Carsten Schüermann

Automating the Meta Theory of Deductive Systems Degree Type: Ph.D. in Pure and Applied Logic
Advisor(s): Frank Pfenning
Graduated: August 2000

Abstract:

This thesis describes the design of a meta-logical framework that supports the representation and verification of deductive systems, its implementation as an automated theorem prover, and experimental results related to the areas of programming languages, type theory, and logics.

Design: The meta-logical framework extends the logical framework LF [Harper et al. 1993] by a meta-logic M2+. This design is novel and unique since it allows higher-order encodings of deductive systems and induction principles to coexist. On the one hand, higher-order representation techniques lead to concise and direct encodings of programming languages and logic calculi. Inductive definitions on the other hand allow the formalization of properties about deductive systems, such as the proof that an operational semantics preserves types or the proof that a logic is consistent. M2+ is a proof calculus whose proof terms are recursive functions that may be defined by cases and range over dependent higher-order types. The soundness of M2+ follows from a realizability interpretation of proof terms as total recursive functions.

Implementation: A proof search algorithm for proof terms in M2+ is implemented in the meta-theorem prover that is part of the Twelf system. Its takes full advantage of higher-order encodings while using inductive reasoning.

Experiments: Twelf has been used for many experiments. Among others, it proved automatically the Church-Rosser theorem for the simply-typed lambda-calculus and the cut-elimination theorem for intuitionistic first-order logic. In programming languages, it proved various type preservation theorems for different operational semantics and compiler correctness theorems. In logics, it was able to derive the equivalence of various logic calculi, such as the natural deduction calculus, the sequent calculus, and the Hilbert calculus. Twelf also proved that Cartesian closed categories can be embedded into the simply-typed lambda-calculus. In the special domains of programming languages, type theory, and logics, Twelf's reasoning power far exceeds that of any other theorem prover.

Thesis Committee:
Frank Pfenning (Chair)
Robert Harper
Peter Lee
Dana Scott
Natarajan Shankar (SRI International)

Randy Bryant, Head, Computer Science Department
James Morris, Dean, School of Computer Science

Keywords:
Meta logic, LF, induction, regular world assumption, realizability, higher-order abstract syntax, Twelf