A New Version of Nominal Isabelle
Add to your list(s)
Download to your calendar using vCal
If you have a question about this talk, please contact Thomas Tuerk.
Nominal Isabelle is a definitional extension of Isabelle/HOL for reasoning conveniently about languages involving binders. In this talk, I will describe a new formalisation of the most basic concepts in the nominal logic work. This new formalisation is a much better fit with the reasoning infrastructure provided by Isabelle/HOL. A result is that we can make Nominal Isabelle
easier to use and can also reduce drastically the amount of
custom ML-code in our implementation of Nominal Isabelle.
This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.
This talk is included in these lists:
Note that ex-directory lists are not shown.
|