Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem
No abstract available.
Related papers
- Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations CPP 2015
- Formal verification of monad transformers ICFP 2012
- An Equational and Graphical Fixed-Point Calculus (Functional Pearl) ICFP 2026
- A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL OOPSLA 2026
- A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs CAV 2025
- Reasoning over Permissions Regions in Concurrent Separation Logic CAV 2020
- Nominal logic programming TOPLAS 2008
- Reasoning About Information Flow Security of Separation Kernels with Channel-Based Communication TACAS 2016