King's College London

Research portal

General Bindings and Alpha-Equivalence in Nominal Isabelle

Research output: Contribution to journalArticle

Christian Urban, Cezary Kaliszyk

Original languageEnglish
Article number14
Number of pages35
JournalLogical methods in computer science
Issue number2
Publication statusPublished - 2012

King's Authors


Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem prover. It provides a proving infrastructure for reasoning about programming language calculi involving named bound variables (as opposed to de-Bruijn indices). In this paper we present an extension of Nominal Isabelle for dealing with general bindings, that means term constructors where multiple variables are bound at once. Such general bindings are ubiquitous in programming language research and only very poorly supported with single binders, such as lambda-abstractions. Our extension includes new definitions of alpha-equivalence and establishes automatically the reasoning infrastructure for alpha-equated terms. We also prove strong induction principles that have the usual variable convention already built in.

View graph of relations

© 2018 King's College London | Strand | London WC2R 2LS | England | United Kingdom | Tel +44 (0)20 7836 5454