Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted Metatheory
No abstract available.
DOI 10.1007/978-3-319-03545-1_8
Related papers
- Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk) CPP 2019
- Adding Sorts to an Isabelle Formalization of Superposition CPP 2026
- A fully adequate shallow embedding of the [pi]-calculus in Isabelle/HOL with mechanized syntax analysis JFP 2003
- HOLCF=HOL+LCF JFP 1999
- Admissible Types-to-PERs Relativization in Higher-Order Logic POPL 2023
- Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem CPP 2019
- A Verified Compiler from Isabelle/HOL to CakeML ESOP 2018
- Formally verified differential dynamic logic CPP 2017