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

                           Lundi 17 février, 10h30

                               ----------------
                               Guillaume Allais
                               ----------------

                          University of Strathclyde

                    =====================================
                    Generic Generalised de Bruijn indices
                    =====================================

Edward Kmett's bound library defines a Scope monad transformer making
the introduction and manipulation of binders in a user-defined syntax
both safe, simple and more efficient than the more traditional de
Bruijn indices.

We will build up on this idea to construct a universe of syntaxes with
binding thus making it possible to use Scopes and program generically
over all possible syntaxes in the same dependently-typed host language.