Nominal Isabelle

General bindings and alpha-equivalence in Nominal Isabelle. 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 α-equivalence and establishes automatically the reasoning infrastructure for α-equated terms. We also prove strong induction principles that have the usual variable convention already built in


References in zbMATH (referenced in 72 articles , 2 standard articles )

Showing results 41 to 60 of 72.
Sorted by year (citations)
  1. Nipkow, Tobias: Teaching semantics with a proof assistant: no more LSD trip proofs (2012)
  2. Pollack, Randy; Sato, Masahiko; Ricciotti, Wilmer: A canonical locally named representation of binding (2012)
  3. Rose, Kristoffer H.; Bloo, Roel; Lang, Frédéric: On explicit substitution with names (2012)
  4. Urban, Christian; Kaliszyk, Cezary: General bindings and alpha-equivalence in Nominal Isabelle (2012)
  5. Vouillon, Jérôme: A solution to the PoplMark challenge based on de Bruijn indices (2012)
  6. Bengtson, Jesper; Johansson, Magnus; Parrow, Joachim; Victor, Björn: Psi-calculi: a framework for mobile processes with nominal data and logic (2011)
  7. Borgström, Johannes; Huang, Shuqin; Johansson, Magnus; Raabjerg, Palle; Victor, Björn; Åman Pohjola, Johannes; Parrow, Joachim: Broadcast psi-calculi with an application to wireless protocols (2011)
  8. Cheney, James; Urban, Christian: Mechanizing the metatheory of mini-XQuery (2011)
  9. Gacek, Andrew; Miller, Dale; Nadathur, Gopalan: Nominal abstraction (2011)
  10. Kaliszyk, Cezary; Barendregt, Henk: Reasoning about constants in Nominal Isabelle or how to formalize the second fixed point theorem (2011)
  11. Urban, Christian; Cheney, James; Berghofer, Stefan: Mechanizing the metatheory of LF (2011)
  12. Urban, Christian; Kaliszyk, Cezary: General bindings and alpha-equivalence in Nominal Isabelle (2011)
  13. Cheney, James: Equivariant unification (2010)
  14. Huffman, Brian; Urban, Christian: A new foundation for Nominal Isabelle (2010)
  15. Krauss, Alexander: Partial and nested recursive function definitions in higher-order logic (2010)
  16. Sato, Masahiko; Pollack, Randy: External and internal syntax of the (\lambda)-calculus (2010)
  17. Bengtson, Jesper; Parrow, Joachim: Psi-calculi in Isabelle (2009)
  18. Cheney, James: A simple nominal type theory (2009)
  19. Gabbay, Murdoch J.: Two-level lambda-calculus (2009)
  20. Gacek, Andrew; Miller, Dale; Nadathur, Gopalan: Reasoning in Abella about structural operational semantics specifications (2009)