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

Showing results 1 to 20 of 53.
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. Ayala-Rincón, Mauricio; de Carvalho-Segundo, Washington; Fernández, Maribel; Nantes-Sobrinho, Daniele: A formalisation of nominal $\alpha$-equivalence with A and AC function symbols (2017)
  3. Cheney, James; Momigliano, Alberto: $\alpha\mathrmCheck$: a mechanized metatheory model checker (2017)
  4. Copello, Ernesto; Szasz, Nora; Tasistro, Álvaro: Formal metatheory of the lambda calculus using Stoughton’s substitution (2017)
  5. Azevedo de Amorim, Arthur: Binding operators for nominal sets (2016)
  6. Bengtson, Jesper; Parrow, Joachim; Weber, Tjark: Psi-calculi in Isabelle (2016)
  7. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  8. Stansifer, Paul; Wand, Mitchell: Romeo: a system for more flexible binding-safe programming (2016)
  9. Parrow, Joachim; Borgström, Johannes; Eriksson, Lars-Henrik; Gutkovas, Ramunas; Weber, Tjark: Modal logics for nominal transition systems (2015)
  10. Paulson, Lawrence C.: A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle (2015)
  11. Popescu, Andrei; Roşu, Grigore: Term-generic logic (2015)
  12. Park, Jonghyun; Seo, Jeongbong; Park, Sungwoo; Lee, Gyesik: Mechanizing metatheory without typing contexts (2014)
  13. Sato, Masahiko; Pollack, Randy; Schwichtenberg, Helmut; Sakurai, Takafumi: Viewing $\lambda$-terms through maps (2013)
  14. Smetsers, Sjaak; Barendsen, Erik: Verifying functional formalizations -- a type-theoretical case study in PVS (2013)
  15. Berghofer, Stefan: A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL (2012)
  16. Charguéraud, Arthur: The locally nameless representation (2012)
  17. Cheney, James; Norrish, Michael; Vestergaard, René: Formalizing adequacy: a case study for higher-order abstract syntax (2012)
  18. Felty, Amy; Momigliano, Alberto: Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (2012)
  19. Gabbay, Murdoch; Ghica, Dan: Game semantics in the nominal model (2012)
  20. Gacek, Andrew; Miller, Dale; Nadathur, Gopalan: A two-level logic approach to reasoning about computations (2012)

1 2 3 next