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 21 to 40 of 72.
Sorted by year (citations)
  1. Azevedo de Amorim, Arthur: Binding operators for nominal sets (2016)
  2. Bengtson, Jesper; Parrow, Joachim; Weber, Tjark: Psi-calculi in Isabelle (2016)
  3. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  4. Copello, Ernesto; Tasistro, Álvaro; Szasz, Nora; Bove, Ana; Fernández, Maribel: Alpha-structural induction and recursion for the lambda calculus in constructive type theory (2016)
  5. Stansifer, Paul; Wand, Mitchell: Romeo: a system for more flexible binding-safe programming (2016)
  6. Dyckhoff, Roy: Cut elimination, substitution and normalisation (2015)
  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) ioport
  13. Tews, Hendrik: Formalizing cut elimination of coalgebraic logics in Coq (2013)
  14. Berghofer, Stefan: A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL (2012)
  15. Charguéraud, Arthur: The locally nameless representation (2012)
  16. Cheney, James; Norrish, Michael; Vestergaard, René: Formalizing adequacy: a case study for higher-order abstract syntax (2012)
  17. Felty, Amy; Momigliano, Alberto: Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (2012)
  18. Gabbay, Murdoch; Ghica, Dan: Game semantics in the nominal model (2012)
  19. Gacek, Andrew; Miller, Dale; Nadathur, Gopalan: A two-level logic approach to reasoning about computations (2012)
  20. Lakin, Matthew R.; Pitts, Andrew M.: Encoding abstract syntax without fresh names (2012)