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 19 articles )
Showing results 1 to 19 of 19.
Sorted by year (- 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)
- 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)
- 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)
- Raggi, Daniel; Bundy, Alan; Grov, Gudmund; Pease, Alison: Automating change of representation for proofs in discrete mathematics (extended version) (2016)
- Thiemann, René; Yamada, Akihisa: Algebraic numbers in Isabelle/HOL (2016)
- Foster, Simon; Struth, Georg: On the fine-structure of regular algebra (2015)
- Marić, Filip; Petrović, Danijela: Formalizing complex plane geometry (2015)
- Raggi, Daniel; Bundy, Alan; Grov, Gudmund; Pease, Alison: Automating change of representation for proofs in discrete mathematics (2015)
- Huffman, Brian; Kunčar, Ondřej: Lifting and transfer: a modular design for quotients in Isabelle/HOL (2013)