Jonas Oberhauser: Bachelor Thesis
Formalizations of Metatheoretic Properties of Type Theories
Author: Jonas Oberhauser
Advisor: Chad E. Brown
Supervisor: Gert Smolka
Abstract
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.
Talks
-
15.05.2012, 16:15: Proofs for Confluence of Simple Type Theory (Building E1 3, Room 528)
In this talk we will describe two proof techniques for confluence we have formalized already: One is the common argument using parallel reduction due to Tait and Martin-Lof. The second technique is similar to the "complete development" method due to Takahashi.
-
17.08.2012, 14:15: Proofs for Strong Normalization (Building E1 3, Room 528)
We will introduce the notion of termination and explain logical relations, a technique to prove termination of various type theories. We have already formalized such a proof for simply typed lambda calculus, and show the issues richer type theories introduce. Finally we will give an idea of how to address those additional issues within the framework of logical relations.
-
03.05.2013, 14:15: FINAL TALK: Formalizing Termination of CC (Building E1 3, Room 528)
Termination is the property that for any well-formed term of CC, all
reduction paths are finite.
This is an extremely powerful property and is a key theorem in proving
consistency of CC.
Various proofs of Termination have been proposed; we consider that by
Geuvers.
Geuvers proof makes use of the fact called Classification, i.e., that
every well-formed term of CC can be classified into one of three
classes: kinds, constructors, and objects. Key functions are then often
defined on only one or two of these classes and hence are partial on the
set of the terms of CC.
We consider a formalization of one of the key functions by Barras, which
makes use of advanced features of Coq's type theory in order to deal
with the partiality in an elegant way. We also show a proof and
formalization of Classification, which we deem more elegant than the one
presented by Barras.
References
- Robin Adams. "Lambda-free logical frameworks". In: arXiv preprint
arXiv:0804.1879 (2008).
- Brian Aydemir et al. "Engineering formal metatheory". In: ACM SIG-
PLAN Notices 43.1 (2008), pp. 3-15.
- B. Barras. Coq en Coq. Rapport de Recherche 3026. INRIA, Oct. 1996.
- B. Barras. "Coq in Coq". 1997.
- Hendrik Pieter Barendregt. The lambda calculus: Its syntax and semantics.
Vol. 103. North Holland, 1984.
- Henk Barendregt. "Introduction to generalized type systems". In: Journal
of functional programming 1.2 (1991), pp. 125-154.
-
Yves Bertot and Pierre Casteran. Interactive theorem proving and program
development: Coq'Art: the calculus of inductive constructions. springer,
2004.
- Nicolaas Govert de Bruijn. "Reflections on automath". In: Nederpelt et
al.
- (1990), pp. 201-228.
- Alonzo Church. "A formulation of the simple theory of types". In: J. Symb.
Log. 5.2 (1940), pp. 56-68.
- Alonzo Church. "A set of postulates for the foundation of logic". In: Annals
of mathematics 33.2 (1932), pp. 346-366.
- Thierry Coquand, Gerard Huet, et al. "The calculus of constructions". In:
(1986).
- Nicolaas Govert De Bruijn. "Lambda calculus notation with nameless
dummies, a tool for automatic formula manipulation, with application
to the Church-Rosser theorem". In: Indagationes Mathematicae (Proceed-
ings). Vol. 75. 5. Elsevier. 1972, pp. 381-392.
- Herman Geuvers. "A short and flexible proof of Strong Normalization for
the Calculus of Constructions". In: TYPES. 1994, pp. 14-38.
-
Jean-Yves Girard. "Interpretation fonctionelle et elimination des coupures de l'arithmetique d'ordre superieur". PhD thesis. PhD thesis, Universit e
Paris VII, 1972.
- Jean-Yves Girard. "The system F of variable types, fifteen years later".
In: Theoretical computer science 45 (1986), pp. 159-192.
92
BIBLIOGRAPHY
- Jean-Yves Girard, Paul Taylor, and Yves Lafont. Proofs and types. Vol. 7.
Cambridge University Press Cambridge, 1989.
- Andrew Gordon. "A mechanisation of name-carrying syntax up to alpha-
conversion". In: Higher Order Logic Theorem Proving and Its Applications
(1994), pp. 413-425.
- Robert Harper, Furio Honsell, and Gordon Plotkin. "A framework for
defining logics". In: Journal of the ACM (JACM) 40.1 (1993), pp. 143-
184.
- William A Howard. "The formulae-as-types notion of construction". In:
To HB Curry: essays on combinatory logic, lambda calculus and formalism
44 (1980), pp. 479-490.
- S.C. Kleene and J.B. Rosser. "The inconsistency of certain formal logics".
In: Annals of mathematics 36.3 (1935), pp. 630-636.
- GR Renardel de Lavalette. "Strictness analysis for POLYREC, a language
with polymorphic and recursive types". In: Logic Group Preprint Series
33 (1988).
- G Longo and E Moggi. Constructive natural deduction and its modest
interpretation. Tech. rep. 1988.
- Z. Luo. Computation and Reasoning: A Type Theory for Computer Sci-
ence. International Series of Monographs on Computer Science. Claren-
don Press, 1994. isbn: 9780198538356. url: http://books.google.de/
books?id=z3uicYzJR1MC.
- Per Martin-Lof. A theory of types. 1971.
- Michael Norrish. "Mechanising lambda-calculus using a classical first order the-
ory of terms with permutations". In: Higher-Order and Symbolic Compu-
tation 19.2 (2006), pp. 169-195.
- Frank Pfenning and Conal Elliot. "Higher-order abstract syntax". In:
ACM SIGPLAN Notices 23.7 (1988), pp. 199-208.
- John Reynolds. "Towards a theory of type structure". In: Programming
Symposium. Springer. 1974, pp. 408-425.
- Allen Stoughton. "Substitution revisited". In: Theoretical Computer Sci-
ence 59.3 (1988), pp. 317-325.
- Masako Takahashi. "Parallel reductions in lambda-calculus". In: Information
and computation 118.1 (1995), pp. 120-127.
- Christian Urban. "Nominal unification revisited". In: arXiv preprint
arXiv:1012.4890 (2010).
- Freek Wiedijk and Dana S Scott. The seventeen provers of the world.
Springer, 2006.
- G. Smolka, C. E. Brown. Semantics Lecture Notes, 2012
Development
Legal notice, Privacy policy