I believe that this submission was the paper mentioned by Andrew Pitts in the comments after Jordi Levy’s talk on efficient nominal unification at RTA 2010.

By Thorsten Altenkirch, unpublished Functional Pearl, available from the Haskell wiki:

We present a new and simple account of α-conversion suitable for formal reasoning. Our main tool is to define α-conversion as a a structural congruence parametrized by a partial bijection on free variables. We show a number of basic properties of substitution. e.g. that substitution is monadic which entails all the usual substitution laws. Finally, we relate α-equivalence classes to de Bruijn terms.

### Like this:

Like Loading...

*Related*

## 0 Responses to “Alpha-conversion is easy”