Abstract

Bindings are common and critical to language design. We repeat defining the uninteresting functions and relations once and once again for each of the systems, where most of them are related to bindings. Luckily, a proof assistant, named Abella, allows us to reasoning our systems in a high-level approach, such that bindings, freshness and substitution becomes much easier to control. Abella brings us a whole new aspect of fresh variables, and the built-in support of lambda-tree syntax enables us to introduce abstractions(lambda functions) directly. What’s more, the two-level approach helps modeling “standard” systems even easier, where lemmas like weakening are assumed for free. This seminar talk will be in a tutorial form, basic knowledge on Coq and the Locally Nameless (TLC) library will be helpful.