Personal tools
You are here: Home Events Lab lunch speakers 2010 Randy Pollack

Randy Pollack

A Canonical Representation of Binding In 1992 McKinna and Pollack formalised a representation of lambda terms using distinct classes of names for global names (parameters) vs local names (variables). This representation is not canonical (terms have more than one representation) but much metatheory of Pure Type Systems was formalised without the need to reason about (or even define) alpha-equivalence. In the present work we give a refinement of McKinna--Pollack representation that is canonical. The central idea that makes this possible is due to S

Document Actions