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 1 to 20 of 72.
Sorted by year (citations)

1 2 3 4 next

  1. Ambal, Guillaume; Lenglet, Sergueï; Schmitt, Alan: (\mathrmHO\pi) in Coq (2021)
  2. Gheri, Lorenzo; Popescu, Andrei: A formalized general theory of syntax with bindings: extended version (2020)
  3. Kutz, Yunus; Schmidt-Schauß, Manfred: Rewriting with generalized nominal unification (2020)
  4. Urciuoli, Sebastián; Tasistro, Álvaro; Szasz, Nora: Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda (2020)
  5. Abel, Andreas; Allais, Guillaume; Hameer, Aliya; Pientka, Brigitte; Momigliano, Alberto; Schäfer, Steven; Stark, Kathrin: POPLMark reloaded: mechanizing proofs by logical relations (2019)
  6. 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)
  7. Kunčar, Ondřej; Popescu, Andrei: A consistent foundation for Isabelle/HOL (2019)
  8. Miller, Dale: Mechanized metatheory Revisited (2019)
  9. Schmidt-Schauß, Manfred; Sabel, David; Kutz, Yunus D. K.: Nominal unification with atom-variables (2019)
  10. Breitner, Joachim: The adequacy of Launchbury’s natural semantics for lazy evaluation (2018)
  11. Cave, Andrew; Pientka, Brigitte: Mechanizing proofs with logical relations -- Kripke-style (2018)
  12. Ebrahimi, M. M.; Keshvardoost, Kh.; Mahmoudi, M.: Simple and subdirectly irreducible finitely supported (Cb)-sets (2018)
  13. Gabbay, Murdoch J.: The language of stratified sets is confluent and strongly normalising (2018)
  14. Keshvardoost, Khadijeh; Mahmoudi, Mojgan: Free functor from the category of (G)-nominal sets to that of 01-(G)-nominal sets (2018)
  15. Perera, Roly; Cheney, James: Proof-relevant (\pi)-calculus: a constructive account of concurrency and causality (2018)
  16. Schmidt-Schauß, Manfred; Sabel, David: Nominal unification with atom and context variables (2018)
  17. 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)
  18. Cheney, James; Momigliano, Alberto: (\alpha\mathrmCheck): a mechanized metatheory model checker (2017)
  19. Copello, Ernesto; Szasz, Nora; Tasistro, Álvaro: Formal metatheory of the lambda calculus using Stoughton’s substitution (2017)
  20. Ayala-Rincón, Mauricio; Fernández, Maribel; Rocha-Oliveira, Ana Cristina: Completeness in PVS of a nominal unification algorithm (2016)

1 2 3 4 next