Towards Proof Automation in Logical Frameworks

Carsten Schürmann (Yale University):
Towards Proof Automation in Logical Frameworks
(joint work with Serge Autexier)

Zusammenfassung:

In many respects reasoning about properties of programming
languages, compilers, types systems, logics, protocol systems,
or safety architectures is a challenging problem. Formulation
of theorems is problematic, finding their proofs is often even
more difficult and so is learning from failure. Can we prove
automatically that a logic used in a proof carrying safety
architecture is sound, that a programming language preserves
types, or that an authentication protocol is safe?

In this talk I will give an introduction to logical frameworks
and describe the results we have achieved by integrating them
with automated theorem proving techniques. One technique that
we consider to be particularly important is the recognition of
none-theorems. To this end we have developed a logically clean
and elegant criterion that prevents our theorem prover from
exploring unnecessary branches in the search state. The theorem
prover is currently being implemented into a proof assistant
based on the logical framework LF.