Proof pearl: de Bruijn terms really do work

By Michael Norrish and Rene Vestergaard, from TPHOLs 2007, available from Michael Norrish’s website:

Placing our result in a web of related mechanised results, we give a direct proof that the de Bruijn λ-calculus (a la Huet, Nipkow and Shankar) is isomorphic to an α-quotiented λ-calculus. In order to establish the link, we introduce an “index-carrying” abstraction mechanism over de Bruijn terms, and consider it alongside a simplified substitution mechanism. Relating the new notions to those of the α-quotiented and the proper
de Bruijn formalisms draws on techniques from the theory of nominal sets.

Slides from a related presentation are available here.

0 Responses to “Proof pearl: de Bruijn terms really do work”



  1. Leave a Comment

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s





%d bloggers like this: