首页    期刊浏览 2024年11月24日 星期日
登录注册

文章基本信息

  • 标题:General Bindings and Alpha-Equivalence in Nominal Isabelle
  • 本地全文:下载
  • 作者:Christian Urban ; Cezary Kaliszyk
  • 期刊名称:Logical Methods in Computer Science
  • 印刷版ISSN:1860-5974
  • 电子版ISSN:1860-5974
  • 出版年度:2012
  • 卷号:8
  • 期号:2
  • 页码:1
  • DOI:10.2168/LMCS-8(2:14)2012
  • 出版社:Technical University of Braunschweig
  • 摘要: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.
  • 其他关键词:Nominal Isabelle, variable convention, alpha-equivalence, theorem provers, formal reasoning, lambda-calculus.
国家哲学社会科学文献中心版权所有