Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem
From MaRDI portal
Publication:3100205
DOI10.1007/978-3-642-25379-9_9zbMath1350.68239OpenAlexW35567622WikidataQ108482186 ScholiaQ108482186MaRDI QIDQ3100205
Cezary Kaliszyk, Hendrik Pieter Barendregt
Publication date: 22 November 2011
Published in: Certified Programs and Proofs (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-25379-9_9
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Uses Software
Cites Work
- Unnamed Item
- Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
- The lambda calculus, its syntax and semantics
- Nominal logic, a first order theory of names and binding
- Mechanizing the metatheory of LF
- Psi-calculi: a framework for mobile processes with nominal data and logic
- Mechanised Computability Theory
- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
- Extending Sledgehammer with SMT Solvers
- Automated Deduction – CADE-20
- A New Foundation for Nominal Isabelle
- Formalising the π-Calculus Using Nominal Logic
- General Bindings and Alpha-Equivalence in Nominal Isabelle
This page was built for publication: Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem
