HKU PL Group

We are a group of programming language researchers who study topics about functional language design, type theory, compilers and program analysis.
The University of Hong Kong

Mechanisation of Higher-order Terms

In this problem session I present a simple-looking problem of implementing formalisation involving higher-order terms (or more simply, terms with binders). Our existing tools and techniques are usually good enough to handle most of the practical cases for a simpler (in terms of implementation) system, but there are always exceptions…