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

                             Lundi 13 mai, 10h30

                               ---------------
                               Gabriel Scherer
                               ---------------

                                 Inria Saclay

     ====================================================================
     A right-to-left type system for mutually-recursive value definitions
     ====================================================================

In call-by-value languages, some mutually-recursive value definitions
can be safely evaluated to build recursive functions or cyclic data
structures, but some definitions (`let rec x = x + 1`) contain
vicious circles and their evaluation fails at runtime. We propose
a static analysis to check the absence of such runtime failures.

We present a set of declarative inference rules, prove its soundness
with respect to a reference source-level semantics, and show that
it can be (right-to-left) directed into an algorithmic check
in a surprisingly simple way.

Our implementation of this new check replaced the existing check used
by the OCaml programming language, a fragile syntactic/grammatical
criterion which let several subtle bugs slip through as the language
kept evolving.