Proofs and Programs about Open Terms

TL;DR

This thesis demonstrates how contextual types facilitate the development and reasoning of formal deductive systems with binders, improving ease of programming, proof construction, and logical framework embedding.

Contribution

It introduces the use of contextual types for implicit parameter reconstruction, embedding formal systems with binders, and integrating LF into dependently typed theories, enhancing formal system manipulation.

Findings

Contextual types simplify proof and program development with dependent types.

Embedding formal systems with binders becomes more straightforward using contextual objects.

Embedding LF in dependently typed theories is feasible and beneficial.

Abstract

Formal deductive systems are very common in computer science. They are used to represent logics, programming languages, and security systems. Moreover, writing programs that manipulate them and that reason about them is important and common. Consider proof assistants, language interpreters, compilers and other software that process input described by formal systems. This thesis shows that contextual types can be used to build tools for convenient implementation and reasoning about deductive systems with binders. We discuss three aspects of this: the reconstruction of implicit parameters that makes writing proofs and programs with dependent types easier, the addition of contextual objects to an existing programming language that make implementing formal systems with binders easier, and finally, we explore the idea of embedding the logical framework LF using contextual types in fully dependently typed theory. These are three aspects of the same message: programming using the right abstraction allows us to solve deeper problems with less effort. In this sense we want: easier to write programs and proofs (with implicit parameters), languages that support binders (by embedding a syntactic framework using contextual types), and the power of the logical framework LF with the expressivity of dependent types.