Software Search - zbMATH Open

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

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

9	Lochbihler, Andreas
5	Divasón, Jose
4	Foster, Simon
4	Immler, Fabian
4	Thiemann, René
4	Traytel, Dmitry
3	Aransay, Jesús
3	Kunčar, Ondřej
3	Popescu, Andrei
3	Schneider, Joshua P.
3	Woodcock, James C. P.
3	Yamada, Akihisa
2	Blanchette, Jasmin Christian
2	Bundy, Alan
2	Cavalcanti, Ana
2	Dunne, Ciarán
2	Fürer, Basil
2	Grov, Gudmund
2	Joosten, Sebastiaan J. C.
2	Kaliszyk, Cezary
2	Marić, Filip
2	Pąk, Karol
2	Pease, Alison
2	Raggi, Daniel
2	Traut, Christoph
2	Wells, Joe B.
2	Zeyda, Frank
1	Basin, David A.
1	Boutry, Pierre
1	Bouzy, Aymeric
1	Brown, Chad Edward
1	Brunner, Julian
1	Canham, Samuel
1	Fleuriot, Jacques D.
1	Fleury, Mathias
1	Grossman, Dan
1	Guttmann, Walter
1	Hirata, Michikazu
1	Hölzl, Johannes
1	Kamareddine, Fairouz D.
1	Lammich, Peter
1	Leo, John W.
1	Minamide, Yasuhiko
1	Nipkow, Tobias
1	Petrović, Danijela
1	Rädle, Jonas
1	Ringer, Talia
1	Roßkopf, Simon
1	Sato, Tetsuya
1	Sefidgar, S. Reza
1	Seidl, Benedikt
1	Sickert, Salomon
1	Simić, Danijela
1	Smola, Filip
1	Struth, Georg
1	Thiele, Bernhard
1	Torstensson, Olle
1	Weber, Tjark
1	Wenzel, Makarius
1	Yazdani, Nathaniel

all top 5

16	Journal of Automated Reasoning
1	Theoretical Computer Science
1	Journal of Cryptology
1	Formal Aspects of Computing
1	Annals of Mathematics and Artificial Intelligence
1	Mathematics in Computer Science
1	Logical Methods in Computer Science

all top 5

43	Computer science (68-XX)
10	Mathematical logic and foundations (03-XX)
4	Commutative algebra (13-XX)
4	Linear and multilinear algebra; matrix theory (15-XX)
3	Ordinary differential equations (34-XX)
3	Dynamical systems and ergodic theory (37-XX)
3	Numerical analysis (65-XX)
2	Number theory (11-XX)
2	Geometry (51-XX)
2	Probability theory and stochastic processes (60-XX)
2	Information and communication theory, circuits (94-XX)
1	Combinatorics (05-XX)
1	Field theory and polynomials (12-XX)
1	Algebraic geometry (14-XX)
1	Category theory; homological algebra (18-XX)
1	Operations research, mathematical programming (90-XX)
1	Game theory, economics, finance, and other social and behavioral sciences (91-XX)
1	Systems theory; control (93-XX)