Proving LF correctness in the Coq Proof Assistant
Formalising logic reasoning on a computer can be achieved using so-called proof assistants.
Among them, the LF logical framework allows to describe logics and prove properties
within these logics as well as meta-properties about these logics.
So far, the reliability of such formal proofs has only been ensured by a informal meta-proof which
states that derived formal proofs really belong to the consequence relation of the encoded logic.
A project such as Sec whose aim is to provide a reliable platform for execution of
untrusted pieces
of code uses the type checker of LF to ensure programs comply with some given security requirements.
As a consequence, the reliability of the whole system depends on the reliability
of the type checking algorithm of LF. That is the reason why we require
a high level of confidence regarding its correctness.
One way of achieving such a level of confidence consists in formalising and proving the correctness
of this algorithm within another proof assistant. We propose to use the Coq proof system,
which is based on a much more powerful type-theoretic framework (the Calculus of Inductive Constructions)
than LF to carry out such a proof.
Expectations
- Core requirements for successful completion:
- Learn how to write specifications and proofs using the Coq proof assistant.
- Understand the existing meta-theoretical proof of type-checking for LF.
- Formalize the various properties required to achieve this proof within Coq.
- Formalize some parts of these proofs
- Extra tasks for the ambitious:
- Complete the formal proof of the whole meta-theory of LF.
- Extract a type-checker for LF from the proofs.
References
- The Coq proof assistant
- Coq'Art: A book about how to develop programs and prove them correct
- Twelf: An implementation of LF logical framework
- Sec: Untrusted Code, Security and Proofs
- Some relevant papers on this topic are:
-
R. Harper, F. Honsell, and G. Plotkin.
A framework for defining logics.
Journal of the ACM, 40(1):143--184, 1993.
- R. Harper and F. Pfenning.
On Equivalence and Canonical Forms in the LF Type Theory.
ACM Transactions on Computational Logic, 2003.
To appear.
- A related work is described in:
J. McKinna and R. Pollack.
Some Lambda Calculus and Type Theory Formalized.
Journal of Automated Reasoning, 23(3-4):373--409, 1999.
Last modified : Mon Feb 16 2004
