Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
No abstract available.
DOI 10.1007/978-3-319-03545-1_9
Related papers
- A modular Isabelle framework for verifying saturation provers CPP 2021
- LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL APLAS 2019
- Transport via Partial Galois Connections and Equivalences APLAS 2023
- Towards verifying ethereum smart contract bytecode in Isabelle/HOL CPP 2018
- A modular, efficient formalisation of real algebraic numbers CPP 2016
- Hyper Separation Logic PLDI 2026
- Formally verified lifting of C-compiled x86-64 binaries PLDI 2022
- Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions CPP 2016