Christian Urban ; Cezary Kaliszyk - General Bindings and Alpha-Equivalence in Nominal Isabelle

lmcs:813 - Logical Methods in Computer Science, June 20, 2012, Volume 8, Issue 2 - https://doi.org/10.2168/LMCS-8(2:14)2012
General Bindings and Alpha-Equivalence in Nominal IsabelleArticle

Authors: Christian Urban ; Cezary Kaliszyk ORCID

    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.


    Volume: Volume 8, Issue 2
    Published on: June 20, 2012
    Imported on: September 23, 2011
    Keywords: Computer Science - Logic in Computer Science,F.3.1

    21 Documents citing this article

    Consultation statistics

    This page has been seen 1519 times.
    This article's PDF has been downloaded 387 times.