Advertisement
Published in:
2011 | OriginalPaper | Chapter
Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem
Authors : Cezary Kaliszyk, Henk Barendregt
Published in: Certified Programs and Proofs
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Nominal Isabelle is a framework for reasoning about programming languages with named bound variables (as opposed to de Bruijn indices). It is a definitional extension of the HOL object logic of the Isabelle theorem prover. Nominal Isabelle supports the definition of term languages of calculi with bindings, functions on the terms of these calculi and provides mechanisms that automatically rename binders. Functions defined in Nominal Isabelle can be defined with assumptions: The binders can be assumed fresh for any arguments of the functions. Defining functions is often one of the more complicated part of reasoning with Nominal Isabelle, and together with analysing freshness is the part that differs most from paper proofs. In this paper we show how to define terms from
λ
-calculus and reason about them without having to carry around the freshness conditions. As a case study we formalize the second fixed point theorem of the
λ
-calculus.