Lambda the Ultimate

Self Certification: Bootstrapping Certified Typecheckers in F* with Coq by Pierre-Yves Strub, Nikhil Swamy, Cedric Fournet, and Juan Chen. POPL'2012.

Well-established dependently-typed languages like Coq provide a highly reliable way to build and check formal proofs. Researchers have also developed several other dependently-typed programming languages such as Agda, Aura, ATS, Cayenne, Epigram, F*, F7, Fine, Guru, PCML5, Ur, etc., and more are in the works, e.g., Trellys. All these languages shine in their own regard, but they lag behind Coq in the degree of safety provided by their implementations. This paper proposes a general technique called self-certification that allows a typechecker for a suitably expressive language to be certified for correctness. We have implemented this general technique for F*, a dependently typed language on the .NET platform.

Self-certification (for F*) involves implementing a typechecker for F* in F*, while using all the conveniences F* provides for the compiler-writer (e.g., partiality, effects, implicit conversions, proof automation, libraries). This type checker is given a specification (in F*) strong enough to ensure that it computes valid typing derivations. We obtain a typing derivation for the core typechecker by running it on itself, and we export it to Coq as a type-derivation certificate. By typechecking this derivation (in Coq) and applying the F* metatheory (also mechanized in Coq), we conclude that our type checker is correct. Once certified in this manner, the F* typechecker is emancipated from Coq.

Self-certification leads to an efficient certification scheme - we no longer depend on verifying certificates in Coq - as well as a more broadly applicable one. For instance, the self-certified F* checker is suitable for use in adversarial settings where Coq is not intended for use, such as run-time certification of mobile code.

F* (Fstar) was mentioned on LtU last year. I find it exciting; F* not only certifies the program but generates efficient proof-carrying bytecode for distribution and thus has much potential for certified programs in open systems where we neither trust the provider of code nor can accept the denial-of-service vulnerabilities and resource costs for validating richly typed code locally.

The self-certification of F*, and the general methods and lessons learned, open a path for incrementally modifying the language, offering much greater freedom to language developers who might pursue languages with similarly expressive type systems.

Between self-certification, generating proof-carrying code for distribution, and interop with the .NET family, F* is seducing me onto the certified programming bandwagon.

Twitter has become a hotbed for PLT humor.

Currently known accounts are:

• PLT Borat
• PLT HULK
• popltarts
• Smug Lisp Borat
• PLT Zizek
• PLT Alain de Botton
• PLT Molyneux
• PLT Ryan Gosling (new!)

If you know of any others let us know in the comments. Or create one your own! It's fun. :-)