some image logo

HOME

SEARCH

CURRENT ISSUE

REGULAR ISSUES

   Volume 1 (2005)

   Volume 2 (2006)

   Volume 3 (2007)

   Volume 4 (2008)

   Volume 5 (2009)

   Volume 6 (2010)

   Volume 7 (2011)

   Volume 8 (2012)

      Issue 1

      Issue 2

      Issue 3

      Issue 4

   Volume 9 (2013)

   Volume 10 (2014)

   Volume 11 (2015)

   Volume 12 (2016)

   Volume 13 (2017)

SPECIAL ISSUES

SURVEY ARTICLES

AUTHORS

ABOUT

SERVICE

LOGIN

FAQ

SUPPORT

CONTACT

VOLUME 8, ISSUE 2, PAPER 14


General Bindings and Alpha-Equivalence in Nominal Isabelle

©Christian Urban, TU Munich
©Cezary Kaliszyk, University of Tsukuba

Abstract
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.

Publication date: June 20, 2012

Full Text: PDF | PostScript
DOI: 10.2168/LMCS-8(2:14)2012

Hit Counts: 5617

Creative Commons