BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:From certified languages to their certified implementations - Pier
 re-Yves Strub
DTSTART:20120402T100000Z
DTEND:20120402T110000Z
UID:TALK37070@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION: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.\n\nThe technique will be exemplified on 
 F*.F* is a full-fledged design and implementation of a new dependently typ
 ed language for secure distributed programming.  It's designed to be enabl
 e the construction and communication of proofs of program properties and o
 f properties of a program's environment in a secure way.\n\nIn the F* sett
 ings\, 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\, lib
 raries). This typechecker is given a specification (in F*) strong enough t
 o ensure that it computes valid typing derivations.  We obtain a typing de
 rivation for the core typechecker by running it on itself\, and we export 
 it to Coq as a type-derivation certificate.  By typechecking this derivati
 on (in Coq) and applying the F* metatheory (also mechanized in Coq)\, we c
 onclude that our type checker is correct.\n\nSelf-certification leads to a
 n efficient certification scheme---we no longer depend on verifying certif
 icates 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 mobi
 le code.\n
LOCATION:Small lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR