Transfer
swMATH ID: | 21009 |
Software Authors: | Huffman, Brian; Kunčar, Ondřej |
Description: | 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. |
Homepage: | https://link.springer.com/chapter/10.1007/978-3-319-03545-1_9 |
Dependencies: | Isabelle |
Related Software: | Lifting; Isabelle/HOL; Archive Formal Proofs; Isabelle; Coq; HOL; Mizar; Sledgehammer; Locales; Autoref; ML; HOL Light; ACL2; seL4; Zoo Probabilistic Systems; HOL-Omega; Isabelle/ZF; kepler98; CeTA; Isar |
Cited in: | 44 Documents |
Standard Articles
1 Publication describing the Software, including 1 Publication in zbMATH | Year |
---|---|
Lifting and transfer: a modular design for quotients in Isabelle/HOL. Zbl 1426.68284 Huffman, Brian; Kunčar, Ondřej |
2013
|
all
top 5
Cited by 60 Authors
all
top 5
Cited in 7 Serials
all
top 5