×

Nominal Isabelle

swMATH ID: 12055
Software Authors: Urban, Christian; Kaliszyk, Cezary
Description: 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
Homepage: https://isabelle.in.tum.de/nominal/
Dependencies: Isabelle
Related Software: Isabelle/HOL; PoplMark; Isabelle; Coq; Twelf; Abella; HOL; Ott; ML; Isar; Archive Formal Proofs; Psi-calculi; HYBRID; Bedwyr; Freshml; Sledgehammer; HOL Light; Agda; GitHub; Locales
Cited in: 77 Publications

Standard Articles

2 Publications describing the Software, including 2 Publications in zbMATH Year
General bindings and alpha-equivalence in Nominal Isabelle. Zbl 1326.68265
Urban, Christian; Kaliszyk, Cezary
2011
Nominal techniques in Isabelle/HOL. Zbl 1140.68061
Urban, Christian
2008
all top 5

Cited by 102 Authors

12 Urban, Christian
7 Cheney, James
5 Parrow, Joachim
5 Schmidt-Schauß, Manfred
4 Berghofer, Stefan
4 Fernández, Maribel
4 Gabbay, Murdoch James
4 Kaliszyk, Cezary
4 Kutz, Yunus D. K.
4 Miller, Dale Allen
4 Szasz, Nora
4 Tasistro, Alvaro
3 Ayala-Rincón, Mauricio
3 Bengtson, Jesper
3 Copello, Ernesto
3 Gacek, Andrew
3 Momigliano, Alberto
3 Nadathur, Gopalan
3 Nipkow, Tobias
3 Pollack, Randy
3 Popescu, Andrei
3 Sato, Masahiko
2 Borgström, Johannes
2 de Carvalho-Segundo, Washington
2 Johansson, Magnus M.
2 Keshvardoost, Khadijeh
2 Mahmoudi, Mojgan
2 Narboux, Julien
2 Norrish, Michael
2 Paulson, Lawrence Charles
2 Pientka, Brigitte
2 Rocha-Oliveira, Ana Cristina
2 Sabel, David
2 Sobrinho, Daniele Nantes
2 Victor, Björn
2 Weber, Tjark
1 Abel, Andreas M.
1 Aehlig, Klaus
1 Allais, Guillaume
1 Åman Pohjola, Johannes
1 Ambal, Guillaume
1 Azevedo de Amorim, Arthur
1 Barendregt, Hendrik Pieter
1 Berger, Martin J.
1 Blanchette, Jasmin Christian
1 Bloo, Roel
1 Bove, Ana
1 Breitner, Joachim
1 Cave, Andrew
1 Chapman, Peter
1 Charguéraud, Arthur
1 Dyckhoff, Roy
1 Ebrahimi, Mohammad Mehdi
1 Eliott, Harold Pancho
1 Eriksson, Lars-Henrik
1 Felty, Amy P.
1 Gheri, Lorenzo
1 Ghica, Dan R.
1 Greenaway, David
1 Gutkovas, Ramūnas
1 Haftmann, Florian
1 Hameer, Aliya
1 Henrio, Ludovic
1 Huang, Shuqin
1 Huffman, Brian
1 Kammüller, Florian
1 Krauss, Alexander
1 Kühlwein, Daniel
1 Kunčar, Ondřej
1 Kutsia, Temur
1 Lakin, Matthew R.
1 Lang, Frédéric
1 Lee, Gyesik
1 Lenglet, Sergueï
1 Levy, Jordi
1 Lochbihler, Andreas
1 McKinna, James
1 Park, Jonghyun
1 Park, Sungwoo
1 Perera, Roly
1 Pitts, Andrew M.
1 Raabjerg, Palle
1 Ricciotti, Wilmer
1 Rose, Kristoffer Høgsbro
1 Roşu, Grigore
1 Sakurai, Takafumi
1 Schäfer, Steven
1 Schmitt, Alan
1 Schwichtenberg, Helmut
1 Seo, Jeongbong
1 Stansifer, Paul
1 Stark, Kathrin
1 Tasson, Christine
1 Tews, Hendrik
1 Traytel, Dmitry
1 Urban, Josef
1 Urciuoli, Sebastián
1 Vestergaard, René
1 Villaret, Mateu
1 Vouillon, Jérôme
...and 2 more Authors
all top 5

Cited in 13 Serials

21 Journal of Automated Reasoning
5 MSCS. Mathematical Structures in Computer Science
4 Theoretical Computer Science
3 Journal of Functional Programming
3 Logical Methods in Computer Science
2 Journal of Symbolic Computation
1 Information and Computation
1 Indagationes Mathematicae. New Series
1 Soft Computing
1 Higher-Order and Symbolic Computation
1 Fundamenta Informaticae
1 Theory and Practice of Logic Programming
1 ACM Transactions on Computational Logic
all top 5

Cited in 6 Fields

70 Computer science (68-XX)
41 Mathematical logic and foundations (03-XX)
3 Category theory; homological algebra (18-XX)
1 Game theory, economics, finance, and other social and behavioral sciences (91-XX)
1 Information and communication theory, circuits (94-XX)
1 Mathematics education (97-XX)

Citations by Year