Contributions in Programming Languages Theory: Logical Relations and Type Theory
Author:
Abstract:
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 the
theory 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.