Christian Urban
Mathematisches
Institut der LMU
Nominal
Techniques in Isabelle/HOL
Abstract:
In this talk, I
will start with a brief
motivation of the nominal logic work and then describe an inductive
definition
for alpha-equated lambda-terms. Building on that, I will illustrate how
informal proofs about the lambda-calculus can be formalized with ease
using
strong induction principles that have Barendregt's variable convention
already
built-in.
Principles
of Programming Seminars