Jonas Oberhauser: Bachelor Thesis

Saarland University Computer Science

Formalizations of Metatheoretic Properties of Type Theories

Author: Jonas Oberhauser
Advisor: Chad E. Brown
Supervisor: Gert Smolka


Confluence and termination are powerful properties of type theories that together prove that for every well-formed term of that type theory, all reduction paths are finite and ultimately lead to the same normal form. In conjunction with subject reduction, they can be used to prove the consistency of powerful type thoeries such as ECC. In this thesis, we studied various proofs for confluence and termination and formalized many of them. We started by formalizing two proofs of confluence for a simply typed lambda calculus: one similar to that by Takahashi, and the canonical proof by Tait and Martin-Lof. Then we considered a formalization by Barras of a termination proof for CC. The proof closely follows a proof of termination presented by Geuvers, who also gave proof sketches on how to extend his approach to some extensions of CC, e.g., small sigma types. We extended Barras' formalization to incorporate small sigma types, following the proof sketch of Geuvers.

Thesis Document

In the thesis we give a mathematical presentation of the extended proof, and use it to describe and explain the intricacies of the formal development. We also give a short discussion on what decisions we faced and how other choices could have made our life easier. Finally, we render our thoughts on to whether this approach can be extended to stronger type theories or not.




Jonas Oberhauser, Fri May 3 13:20:50 2013