Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E
			   __
			  / _`  _   /  /  o
			 /   ) __) /  /  / /  / /\/|
			(___/ (_/ (_ (_ / (__/ /   |

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                            MARDI 18 avril, 10h30

                                --------------
                                Armaël Guéneau
                                --------------

                                 Inria Paris

                 ===========================================
                 Verified Characteristic Formulae for CakeML
                 ===========================================

Characteristic Formulae (CF) offer a productive, principled approach
to generating verification conditions for higher-order imperative
programs, but so far the soundness of CF has only been considered with
respect to an informal specification of a programming language
(OCaml).

In this talk, I will explain how we built a fully-fledged CF framework
for the formally specified CakeML programming language. Our framework
extends the existing CF approach to support exceptions and I/O,
thereby covering the full feature set of CakeML, and comes with a
formally verified soundness theorem. I will also show how the CF
framework integrates with existing proof techniques for verifying
CakeML programs. This validates the CF approach, and allows users to
prove end-to-end theorems for higher-order imperative programs.

This is joint work with Magnus Myreen, Ramana Kumar and Michael
Norrish.