General Bindings and Alpha-Equivalence in Nominal Isabelle

Christian Urban; Cezary Kaliszyk

doi:10.2168/LMCS-8(2:14)2012

Christian Urban ; Cezary Kaliszyk - General Bindings and Alpha-Equivalence in Nominal Isabelle

lmcs:813 - Logical Methods in Computer Science, June 20, 2012, Volume 8, Issue 2 - https://doi.org/10.2168/LMCS-8(2:14)2012

General Bindings and Alpha-Equivalence in Nominal IsabelleArticle

Authors: Christian Urban ; Cezary Kaliszyk

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 alpha-equivalence and establishes automatically the reasoning infrastructure for alpha-equated terms. We also prove strong induction principles that have the usual variable convention already built in.

Comment: 35 pages

https://doi.org/10.2168/LMCS-8(2:14)2012

Source: arXiv.org:1206.0136

Volume: Volume 8, Issue 2

Secondary volumes: Selected Papers of the 20th European Symposium on Programming (ESOP 2011)

Published on: June 20, 2012

Imported on: September 23, 2011

Keywords: Computer Science - Logic in Computer Science, F.3.1

Licence: arXiv.org - Non-exclusive license to distribute

Bibliographic References

24 Documents citing this article

Daniele Nantes-Sobrinho;Maribel Fernández;Deivid Vale;Mauricio Ayala-Rincón, 2025, A Nominal Approach to Equational Problems in Languages with Binders, Research Portal (King's College London), 27, 1, pp. 1-46, 10.1145/3767744, https://kclpure.kcl.ac.uk/portal/en/publications/58843418-d812-4fc0-8299-3080a8f904d1.

Jan van Brügge;James McKinna;Andrei Popescu;Dmitriy Traytel, 2025, Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings, Proceedings of the ACM on Programming Languages, 9, POPL, pp. 1687-1718, 10.1145/3704893, https://doi.org/10.1145/3704893.

Andrei Popescu, 2024, Nominal Recursors as Epi-Recursors, Proceedings of the ACM on Programming Languages, 8, POPL, pp. 425-456, 10.1145/3632857, https://doi.org/10.1145/3632857.

Andrei Popescu, 2023, Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version, Journal of Automated Reasoning, 67, 3, 10.1007/s10817-023-09672-4, https://doi.org/10.1007/s10817-023-09672-4.

Andrei Popescu, 2022, Rensets and Renaming-Based Recursion for Syntax with Bindings, Lecture notes in computer science, pp. 618-639, 10.1007/978-3-031-10769-6_36, https://doi.org/10.1007/978-3-031-10769-6_36.

Manfred Schmidt-Schauß;Yunus Kutz, 2021, Nominal Unification with Letrec and Environment-Variables, Lecture notes in computer science, pp. 95-112, 10.1007/978-3-030-68446-4_5.

Benoît Montagu;Thomas Jensen, 2020, Stable relations and abstract interpretation of higher-order programs, Proceedings of the ACM on Programming Languages, 4, ICFP, pp. 1-30, 10.1145/3409001, https://doi.org/10.1145/3409001.

Yunus Kutz;Manfred Schmidt-Schauß, 2020, Rewriting with generalized nominal unification, Mathematical Structures in Computer Science, 30, 6, pp. 710-735, 10.1017/s0960129520000122.

ANDREAS ABEL;GUILLAUME ALLAIS;ALIYA HAMEER;BRIGITTE PIENTKA;ALBERTO MOMIGLIANO;et al., 2019, POPLMark reloaded: Mechanizing proofs by logical relations, Archivio Istituzionale della Ricerca (Universita Degli Studi Di Milano), 29, 10.1017/s0956796819000170, http://hdl.handle.net/2434/695543.

Jasmin Christian Blanchette;Lorenzo Gheri;Andrei Popescu;Dmitriy Traytel, 2019, Bindings as bounded natural functors, Proceedings of the ACM on Programming Languages, 3, POPL, pp. 1-34, 10.1145/3290335, https://doi.org/10.1145/3290335.

JOACHIM BREITNER, 2018, The adequacy of Launchbury's natural semantics for lazy evaluation, Journal of Functional Programming, 28, 10.1017/s0956796817000144.

Manfred Schmidt-Schauß;David Sabel;Yunus D.K. Kutz, 2018, Nominal unification with atom-variables, Journal of Symbolic Computation, 90, pp. 42-64, 10.1016/j.jsc.2018.04.003.

JAMES CHENEY;ALBERTO MOMIGLIANO, 2017, αCheck: A mechanized metatheory model checker, Edinburgh Research Explorer, 17, 3, pp. 311-352, 10.1017/s1471068417000035, https://www.research.ed.ac.uk/en/publications/451cfc9f-8d8f-43a5-8e7a-b7d2bfa331ac.

Arthur Azevedo de Amorim, 2016, Binding Operators for Nominal Sets, Electronic Notes in Theoretical Computer Science, 325, pp. 3-27, 10.1016/j.entcs.2016.09.029, https://doi.org/10.1016/j.entcs.2016.09.029.

James Cheney;Alberto Momigliano;Matteo Pessina, 2016, Advances in Property-Based Testing for $$\alpha $$ Prolog, Archivio Istituzionale della Ricerca (Universita Degli Studi Di Milano), pp. 37-56, 10.1007/978-3-319-41135-4_3, http://hdl.handle.net/2434/411297.

Jasmin Christian Blanchette;David Greenaway;Cezary Kaliszyk;Daniel Kühlwein;Josef Urban, 2016, A Learning-Based Fact Selector for Isabelle/HOL, 57, 3, pp. 219-244, 10.1007/s10817-016-9362-8, https://inria.hal.science/hal-01386986.

Manfred Schmidt-Schauß;David Sabel, 2016, Unification of program expressions with recursive bindings, Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, pp. 160-173, 10.1145/2967973.2968603.

Andrei Popescu;Grigore Roşu, 2015, Term-generic logic, Theoretical Computer Science, 577, pp. 1-24, 10.1016/j.tcs.2015.01.047.

Gergely Buday, 2015, Formalising the SECD machine with nominal Isabelle, Proceedings of the 30th Annual ACM Symposium on Applied Computing, pp. 1823-1824, 10.1145/2695664.2696065.

Jesper Bengtson;Joachim Parrow;Tjark Weber, 2015, Psi-Calculi in Isabelle, IT University Of Copenhagen (IT University of Copenhagen), 56, 1, pp. 1-47, 10.1007/s10817-015-9336-2, https://pure.itu.dk/portal/da/publications/1b8c5c18-acc0-4241-b6f5-1d281f1fffac.

Joachim Breitner, 2015, Formally proving a compiler transformation safe, ACM SIGPLAN Notices, 50, 12, pp. 35-46, 10.1145/2887747.2804312.

Joachim Breitner, 2015, Formally proving a compiler transformation safe, Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell, pp. 35-46, 10.1145/2804302.2804312.

LAWRENCE C. PAULSON, 2014, A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS, arXiv (Cornell University), 7, 3, pp. 484-498, 10.1017/s1755020314000112, http://arxiv.org/abs/2104.14260.

René Thiemann, 2013, Formalizing Bounded Increase, Lecture notes in computer science, pp. 245-260, 10.1007/978-3-642-39634-2_19.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3691 times.

This article's PDF has been downloaded 694 times.