Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem

DOI10.1007/978-3-642-25379-9_9zbMath1350.68239WikidataQ108482186 ScholiaQ108482186MaRDI QIDQ3100205

Cezary Kaliszyk, H. P. 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

Mathematics Subject Classification ID

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

03B40: Combinatory logic and lambda calculus

Uses Software

• Isabelle/HOL
• Sledgehammer
• Nominal Isabelle