Arthur Charguéraud's locally nameless solution


This locally nameless formalization is the result towards which I have converged at the end of an internship focused on the POPLMark Challenge. The work took place from March to July 2006 at the University of Pennsylvania, with Benjamin Pierce and Stephanie Weirich as advisors.

This solution benefits from two nice properties:

Main aspects of the solution:

About the implementation:

Possible improvements in the solution: