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 42 articles , 2 standard articles )

Showing results 1 to 20 of 42.
Sorted by year (citations)

1 2 3 next

  1. Bengtson, Jesper; Parrow, Joachim; Weber, Tjark: Psi-calculi in Isabelle (2016)
  2. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  3. Paulson, Lawrence C.: A mechanised proof of Gödel’s incompleteness theorems using nominal Isabelle (2015)
  4. Popescu, Andrei; Roşu, Grigore: Term-generic logic (2015)
  5. Park, Jonghyun; Seo, Jeongbong; Park, Sungwoo; Lee, Gyesik: Mechanizing metatheory without typing contexts (2014)
  6. Sato, Masahiko; Pollack, Randy; Schwichtenberg, Helmut; Sakurai, Takafumi: Viewing $\lambda$-terms through maps (2013)
  7. Berghofer, Stefan: A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL (2012)
  8. Charguéraud, Arthur: The locally nameless representation (2012)
  9. Cheney, James; Norrish, Michael; Vestergaard, René: Formalizing adequacy: a case study for higher-order abstract syntax (2012)
  10. Felty, Amy; Momigliano, Alberto: Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (2012)
  11. Gacek, Andrew; Miller, Dale; Nadathur, Gopalan: A two-level logic approach to reasoning about computations (2012)
  12. Lakin, Matthew R.; Pitts, Andrew M.: Encoding abstract syntax without fresh names (2012)
  13. Pollack, Randy; Sato, Masahiko; Ricciotti, Wilmer: A canonical locally named representation of binding (2012)
  14. Rose, Kristoffer H.; Bloo, Roel; Lang, Frédéric: On explicit substitution with names (2012)
  15. Urban, Christian; Kaliszyk, Cezary: General bindings and alpha-equivalence in Nominal Isabelle (2012)
  16. Vouillon, Jér^ome: A solution to the PoplMark challenge based on de Bruijn indices (2012)
  17. Bengtson, Jesper; Johansson, Magnus; Parrow, Joachim; Victor, Björn: Psi-calculi: a framework for mobile processes with nominal data and logic (2011)
  18. Gacek, Andrew; Miller, Dale; Nadathur, Gopalan: Nominal abstraction (2011)
  19. Urban, Christian; Kaliszyk, Cezary: General bindings and alpha-equivalence in Nominal Isabelle (2011)
  20. Cheney, James: Equivariant unification (2010)

1 2 3 next