[TYPES] Types for Open Terms ?

[Nicolas Pouillard]

On Thu, Oct 13, 2011 at 5:23 PM, Jacques Carette <carette at mcmaster.ca> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hello,

> I have been looking to find relevant work on types for open terms, i.e.
> types for terms with free variables which are *not* in an environment.

Our work with François Pottier should be relevant for what you are looking for.

Our approach has been described in a first paper [1], a second paper [2]
presents a nicer system studying the de Bruijn approach more in depth.

My PhD thesis would soon be available as well. It contains the nicer
presentation
of our second paper but unified to various first-order representations:
  nominal, de Bruijn indices, de Bruijn levels and combinations of them.

Best regards,

-- 
Nicolas Pouillard
http://nicolaspouillard.fr

[1]: «A Fresh Look at Programming With Names and Binders» (ICFP 2010)
       http://nicolaspouillard.fr/#fresh-look-paper
[2]: «Nameless, Painless» (ICFP 2011)
       http://nicolaspouillard.fr/#nameless-painless