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 - Rocquencourt
                         Amphi Turing du bâtiment 1

                          MERCREDI 21 janvier, 14h30

                             --------------------
                             Clément Pit-Claudel
                             --------------------

                                     MIT

               ================================================
               Fiat: Deductive Synthesis of Abstract Data Types
                            in a Proof Assistant,
                                  and beyond
               ================================================

                   [PLEASE NOTE THE UNUSUAL DATE AND TIME]

In my talk I'll present Fiat, a Coq library for refining declarative
specs into efficient functional programs. I'll discuss how Fiat
works, and how we used it to produce a small verifying database query
planner, automatically deriving efficient implementations of database
schemas and methods expressed in an SQL-like language. I'll then
outline more recent developments, focusing on ongoing work to compile
Fiat programs to verified assembly.