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

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

1 2 3 next

  1. Ebrahimi, M.M.; Keshvardoost, Kh.; Mahmoudi, M.: Simple and subdirectly irreducible finitely supported $Cb$-sets (2018)
  2. Cheney, James; Momigliano, Alberto: $\alpha\mathrmCheck$: a mechanized metatheory model checker (2017)
  3. Copello, Ernesto; Szasz, Nora; Tasistro, Álvaro: Formal metatheory of the lambda calculus using Stoughton’s substitution (2017)
  4. Bengtson, Jesper; Parrow, Joachim; Weber, Tjark: Psi-calculi in Isabelle (2016)
  5. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  6. Stansifer, Paul; Wand, Mitchell: Romeo: a system for more flexible binding-safe programming (2016)
  7. Parrow, Joachim; Borgström, Johannes; Eriksson, Lars-Henrik; Gutkovas, Ramunas; Weber, Tjark: Modal logics for nominal transition systems (2015)
  8. Paulson, Lawrence C.: A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle (2015)
  9. Popescu, Andrei; Roşu, Grigore: Term-generic logic (2015)
  10. Park, Jonghyun; Seo, Jeongbong; Park, Sungwoo; Lee, Gyesik: Mechanizing metatheory without typing contexts (2014)
  11. Sato, Masahiko; Pollack, Randy; Schwichtenberg, Helmut; Sakurai, Takafumi: Viewing $\lambda$-terms through maps (2013)
  12. Smetsers, Sjaak; Barendsen, Erik: Verifying functional formalizations -- a type-theoretical case study in PVS (2013)
  13. Berghofer, Stefan: A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL (2012)
  14. Charguéraud, Arthur: The locally nameless representation (2012)
  15. Cheney, James; Norrish, Michael; Vestergaard, René: Formalizing adequacy: a case study for higher-order abstract syntax (2012)
  16. Felty, Amy; Momigliano, Alberto: Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (2012)
  17. Gacek, Andrew; Miller, Dale; Nadathur, Gopalan: A two-level logic approach to reasoning about computations (2012)
  18. Lakin, Matthew R.; Pitts, Andrew M.: Encoding abstract syntax without fresh names (2012)
  19. Nipkow, Tobias: Teaching semantics with a proof assistant: no more LSD trip proofs (2012)
  20. Pollack, Randy; Sato, Masahiko; Ricciotti, Wilmer: A canonical locally named representation of binding (2012)

1 2 3 next