Abstract

In this talk, I will present a general technique called self-certification that allows a typechecker for a suitably expressive language to be certified for correctness.

The technique will be exemplified on F.F is a full-fledged design and implementation of a new dependently typed language for secure distributed programming. It’s designed to be enable the construction and communication of proofs of program properties and of properties of a program’s environment in a secure way.

In the F settings, self-certification 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 typechecker 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.

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.