When & Where: 12:30pm, Wednesday, Sept 25, 2002, Room 400 AKW
Abstract:
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 proof planning. To this end we have developed a logically clean and elegant criterion that allows a theorem prover to recognize unpromising proof states early in a proof. It is currently being implemented into a theorem for a proof assistant based on the logical framework LF.