University of Cambridge > > Microsoft Research Cambridge, public talks > From certified languages to their certified implementations

From certified languages to their certified implementations

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

This event may be recorded and made available internally or externally via Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending

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.

This talk is part of the Microsoft Research Cambridge, public talks series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity