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

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

1 2 3 4 next

  1. Gheri, Lorenzo; Popescu, Andrei: A formalized general theory of syntax with bindings: extended version (2020)
  2. Abel, Andreas; Allais, Guillaume; Hameer, Aliya; Pientka, Brigitte; Momigliano, Alberto; Schäfer, Steven; Stark, Kathrin: POPLMark reloaded: mechanizing proofs by logical relations (2019)
  3. Ayala-Rincón, Mauricio; de Carvalho-Segundo, Washington; Fernández, Maribel; Nantes-Sobrinho, Daniele; Rocha-Oliveira, Ana Cristina: A formalisation of nominal (\alpha)-equivalence with A, C, and AC function symbols (2019)
  4. Kunčar, Ondřej; Popescu, Andrei: A consistent foundation for Isabelle/HOL (2019)
  5. Miller, Dale: Mechanized metatheory Revisited (2019)
  6. Schmidt-Schauß, Manfred; Sabel, David; Kutz, Yunus D. K.: Nominal unification with atom-variables (2019)
  7. Breitner, Joachim: The adequacy of Launchbury’s natural semantics for lazy evaluation (2018)
  8. Cave, Andrew; Pientka, Brigitte: Mechanizing proofs with logical relations -- Kripke-style (2018)
  9. Ebrahimi, M. M.; Keshvardoost, Kh.; Mahmoudi, M.: Simple and subdirectly irreducible finitely supported (Cb)-sets (2018)
  10. Gabbay, Murdoch J.: The language of stratified sets is confluent and strongly normalising (2018)
  11. Keshvardoost, Khadijeh; Mahmoudi, Mojgan: Free functor from the category of (G)-nominal sets to that of 01-(G)-nominal sets (2018)
  12. Perera, Roly; Cheney, James: Proof-relevant (\pi)-calculus: a constructive account of concurrency and causality (2018)
  13. 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)
  14. Cheney, James; Momigliano, Alberto: (\alpha\mathrmCheck): a mechanized metatheory model checker (2017)
  15. Copello, Ernesto; Szasz, Nora; Tasistro, Álvaro: Formal metatheory of the lambda calculus using Stoughton’s substitution (2017)
  16. Ayala-Rincón, Mauricio; Fernández, Maribel; Rocha-Oliveira, Ana Cristina: Completeness in PVS of a nominal unification algorithm (2016)
  17. Azevedo de Amorim, Arthur: Binding operators for nominal sets (2016)
  18. Bengtson, Jesper; Parrow, Joachim; Weber, Tjark: Psi-calculi in Isabelle (2016)
  19. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  20. 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)

1 2 3 4 next