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

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

1 2 3 4 next

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

1 2 3 4 next