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 27 mars, 10h30

                               ---------------
                               Thomas Williams
                               ---------------

                                 Inria Paris

                   =======================================
                   Refactoring ML programs using ornaments
                   =======================================

Ornaments are a way to describe changes in datatype definitions
that preserve their recursive structure, reorganizing, adding, or
dropping some pieces of data. The relation between two types
given by an ornament can be used to define a lifting relation
between functions operating on a bare definition and functions
operating on the ornamented structures. Thus, ornaments provide a
way to specify the desired behaviour of a program refactored to
work on an ornamented datatype.

In this talk, I will explain how ornaments can be used to partially
(and sometimes totally) lift a function. I will present a
prototype implementation of lifting along ornaments for a subset
of OCaml and describe some use cases. I will explain how the
lifting is carried out, and how we can prove the correctness of
the process.