BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The CH2O project: making sense of the C standard - Freek Wiedijk
DTSTART:20150304T130000Z
DTEND:20150304T140000Z
UID:TALK57023@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:CH2O is the PhD project of Robbert Krebbers and has as its goa
 l a formal version of the ISO standard of the C programming language.  A p
 roblem with this is that the C standard is fundamentally inconsistent.\n\n
 There are three versions of the CH2O semantics: a (small step) operational
  semantics\, an executable semantics\, and an axiomatic semantics (a separ
 ation logic for C).  The most important properties - soundness and complet
 eness results\, subject reduction and progress\, correctness of the type c
 hecker - have all been proved.  All definitions and proofs have been fully
  formalized in Coq\, without any axioms and on top of a non-trivial suppor
 t library.\n\nThe CH2O project has two abstract C-like languages.  A signi
 ficant subset of C called "CH2O abstract C" is translated into a simplifie
 d language called "CH2O core C".  This translation is written in Coq and i
 mplicitly gives a semantics to CH2O abstract C.  The rest of the formaliza
 tion is all about CH2O core C.\n\nThe executable CH2O semantics has been e
 xtracted to OCaml and combined with the CIL parser to a standalone "interp
 reter".  This tool can be used to explore all behaviors of a program accor
 ding to the C standard.  Although the CH2O semantics does not yet support 
 I/O (nor the exit function)\, a small hack allows the CH2O interpreter to 
 still explore programs that call printf.\n\nThe CH2O semantics has been sp
 ecifically designed to be compatible with the CompCert semantics for C.  S
 ignificant differences between CompCert and CH2O are that the CH2O semanti
 cs has explicit typing judgments for everything\, and that CH2O applies to
  any ISO compliant compiler.
LOCATION:FW11
END:VEVENT
END:VCALENDAR