Contributions in Programming Languages Theory: Logical Relations and Type Theory

Software systems are ubiquitous. Failure in safety- and security-critical systems, e.g., the control system of a passenger plane, can be quite catastrophic. Hence, it is crucial to ensure that safety- and security-critical software systems are correct. Types play an important role in helping us achieve this goal. They help compilers check for (some) programmer's mistakes. They also form the basis of a group of proof assistants. A proof assistant is a software that allows for formalization and mechanization of mathematics, including the theory of types, theory of programming languages, program verification, etc. In this thesis we contribute to the study of programming languages and type theory. In the first part of this thesis we formalize a mathematical theory (closely related to thetheory of types and programming languages) in the proof assistant Coq and contribute to the type theory of this proof assistant. In the second part of this thesis we study a number of programming languages through their type systems. In particular, we develop methods for proving soundness (correctness) of their type systems and to prove equivalence of programs. The first part of this thesis begins with the formal specification of category theory, a mathematical theory closely related to the theory of types and programming languages, in the proof assistant Coq. Coq is a proof assistant based on the predicative calculus of inductive constructions (pCIC). In this formalization we have taken advantage of a feature of Coq known as universe polymorphism to represent (relative) smallness and largeness of categories using Coq's universe hierarchy. The formalization of category theory that is presented in this part reveals a shortcoming of pCIC: the fact that the cumulativity relation of Coq, also known as the subtyping relation, needs to be extended to support subtyping of inductive types. The cumulativity relation for categories (represented using inductive types) would allow a small category to be also considered a large category, i.e., the type of small categories would be a subtype of the type of large categories. The following chapter presents the predicative calculus of cumulative inductive constructions (pCuIC). pCuIC extends pCIC to solve the aforementioned shortcoming of pCIC by introducing a novel subtyping relation for inductive types. The cumulativity relation introduced for inductive types also has interesting consequences for types that do not involve the mathematical concept of smallness and largeness. For instance, it unifies (judgementally equates) the type list A of lists (whose elements are terms of type A) at all universe levels. This novel subtyping relation has been integrated into the proof assistant Coq as of the official release of Coq 8.7. In the second part of this thesis we develop logical relation models, as operationally-based semantic approaches for proving type soundness and establishing equivalence of programs, for a number of programming languages. We develop logical relations models for F_mu_ref_conc, a concurrent ML-like programming language, and use them to prove type soundness and equivalence of programs. We use the latter to establish the equivalence of concurrent counter and stack modules. One of the main results of this thesis is developing a logical relations model which allows us to establish proper encapsulation of state in the programming language STLang. STLang is a programming language featuring a Haskell-style ST monad which is used to encapsulate state. This problem was open for almost two decades. We solve this problem by showing that certain program equivalences hold in the presence of the ST monad that would not hold if the state was not properly encapsulated. Finally, we develop logical relations for an extension of F_mu_ref_conc with continuations, a feature that makes reasoning about programs quite intricate. We develop a reasoning principle for our system which allows us to treat parts of the program that do not involve continuations in a disrupting manner (but can nevertheless interact with other parts which do) as though there are no continuations in the programming language. We use this novel reasoning principle together with our logical relations model to prove that an implementation of a web server that uses continuations (in the style of Racket web servers) is equivalent to one which does not use continuations. It is well-known that developing and working with logical relations models for advanced type systems such as those studied in the second part of this thesis is very intricate. In this thesis we mitigate this issue by working in the Iris program logic. Iris is a state-of-the-art program logic based on separation logic for verification of higher-order concurrent imperative programs. Working in Iris allows us to develop our logical relations models at a higher-level of abstraction and thus avoid the usual intricacies associated with developing and working with such models. Furthermore, we take advantage of the formalization of Iris on top of the Coq proof assistant to mechanize all of the results in this part of the thesis on top of Coq.status: publishe