Lifting
Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL. Quotients, subtypes, and other forms of type abstraction are ubiquitous in formal reasoning with higher-order logic. Typically, users want to build a library of operations and theorems about an abstract type, but they want to write definitions and proofs in terms of a more concrete representation type, or “raw” type. Earlier work on the Isabelle Quotient package has yielded great progress in automation, but it still has many technical limitations. We present an improved, modular design centered around two new packages: the Transfer package for proving theorems, and the Lifting package for defining constants. Our new design is simpler, applicable in more situations, and has more user-friendly automation.
Keywords for this software
References in zbMATH (referenced in 26 articles )
Showing results 1 to 20 of 26.
Sorted by year (- Basin, David A.; Lochbihler, Andreas; Sefidgar, S. Reza: CryptHOL: game-based proofs in higher-order logic (2020)
- Divasón, Jose; Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa: A verified implementation of the Berlekamp-Zassenhaus factorization algorithm (2020)
- Foster, Simon; Cavalcanti, Ana; Canham, Samuel; Woodcock, Jim; Zeyda, Frank: Unifying theories of reactive design contracts (2020)
- Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa: A verified implementation of algebraic numbers in Isabelle/HOL (2020)
- Immler, Fabian; Traut, Christoph: The flow of ODEs: formalization of variational equation and Poincaré map (2019)
- Kunčar, Ondřej; Popescu, Andrei: From types to sets by local type definition in higher-order logic (2019)
- Lammich, Peter; Lochbihler, Andreas: Automatic refinement to efficient data structures: a comparison of two approaches (2019)
- Lochbihler, Andreas: Effect polymorphism in higher-order logic (proof pearl) (2019)
- Immler, Fabian: A verified ODE solver and the Lorenz attractor (2018)
- Aransay, Jesús; Divasón, Jose: A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem (2017)
- Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy: Friends with benefits. Implementing corecursion in foundational proof assistants (2017)
- Blanchette, Jasmin Christian; Fleury, Mathias; Traytel, Dmitriy: Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL (2017)
- Foster, Simon; Thiele, Bernhard; Cavalcanti, Ana; Woodcock, Jim: Towards a UTP semantics for Modelica (2017)
- Hölzl, Johannes: Markov chains and Markov decision processes in Isabelle/HOL (2017)
- Aransay, Jesús; Divasón, Jose: Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL (2016)
- Foster, Simon; Zeyda, Frank; Woodcock, Jim: Unifying heterogeneous state-spaces with lenses (2016)
- Immler, Fabian; Traut, Christoph: The flow of ODEs (2016)
- Kunčar, Ondřej; Popescu, Andrei: From types to sets by local type definitions in higher-order logic (2016)
- Lochbihler, Andreas: Probabilistic functions and cryptographic oracles in higher order logic (2016)
- Lochbihler, Andreas; Schneider, Joshua: Equational reasoning with applicative functors (2016)