< Back to previous page

Project

Dependently typed programming for secure and correct web applications

Dependent type theory is a powerful language for writing functional programs
with very precise types. It is used to write not only programs but also
mathematical proofs that these programs satisfy certain properties. Because of
this, languages based on dependent types – such as Coq, Agda, and Idris – are
used both as programming languages and as interactive proof assistants.
While dependent types give strong guarantees about your programs and proofs,
they also impose equally strong requirements on them. This often makes it
harder to write programs in a dependently typed language compared to one with
a simpler type system. For this reason certain techniques have been developed,
such as dependent pattern matching and specialization by unification. These
techniques provide an intuitive way to write programs and proofs in dependently
typed languages.
Previously, dependent pattern matching had only been shown to work in
a limited setting. In particular, it relied on the K axiom – also known as
the uniqueness of identity proofs – to remove equations of the form x = x.
This axiom is inadmissible in many type theories, particularly in the new and
promising branch known as homotopy type theory (HoTT). As a result, programs
and proofs in these new theories cannot make use of dependent pattern matching
and are as a result much harder to write, modify, and understand. Additionally,
the interaction of dependent pattern matching with small but practical features
such as eta-equality for record types and postponing of unification constraints
was poorly understood, resulting in subtle bugs and inconsistencies.
In this thesis, we develop dependent pattern matching and unification in a
general setting that does not require the K axiom, both from a theoretical
perspective and a practical one. In particular, we present a proof-relevant
unification algorithm, where each unification rule produces evidence of its
correctness. This evidence guarantees that all unification rules are correct by
construction, and also gives a computational characterization to each unification
rule.
To ensure that these techniques are sound and will stay so in face of future
extensions to type theory, we show how to translate them to more basic primitive
constructs, i.e. the standard datatype eliminators. During this translation, wepay special attention to the computational content of all constructions involved.
This guarantees that the intuitions from regular pattern matching carry over to
a dependently typed setting.
Based on our work, we implemented a complete overhaul of the algorithm
for checking definitions by dependent pattern matching in Agda. Our new
implementation fixes a substantial number of issues in the old implementation,
and is at the same time less restrictive than the old ad-hoc restrictions. Thus itputs the whole system back on a strong foundation. In addition, our work has
already been used as the basis for other implementations of dependent pattern
matching, such as the Equations package for Coq and the Lean theorem prover.
The work in this thesis eliminates all implicit assumptions introduced to the
type theory by pattern matching and unification. In the future, we may also
want to integrate new principles with pattern matching, for example the higher
inductive types introduced by HoTT. The framework presented in this thesis
also provides a solid basis for such extensions to be built on.

Date:1 Oct 2013 →  30 Sep 2017
Keywords:Dependently typed programming
Disciplines:Applied mathematics in specific fields, Computer architecture and networks, Distributed computing, Information sciences, Information systems, Programming languages, Scientific computing, Theoretical computer science, Visual computing, Other information and computing sciences
Project type:PhD project