[Prev][Next][Index][Thread]
Announcement: Ph.D. thesis
I would like to announce that my Ph.D. thesis
Automating the Meta-Theory of Deductive Systems
written under the guidance of Prof. Frank Pfenning is available online
from my homepage:
http://www.cs.yale.edu/~carsten/papers/S00b.ps.gz
The abstract follows below.
Best regards,
-- Carsten Schuermann
============================================================
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.