University of Cambridge > Talks.cam > 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 http://research.microsoft.com. 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 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity