Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL

DOI10.1007/978-3-319-03545-1_9zbMath1426.68284OpenAlexW101424827MaRDI QIDQ2938044

Ondřej Kunčar, Brian Huffman

Publication date: 13 January 2015

Published in: Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-03545-1_9

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem ⋮ Automating change of representation for proofs in discrete mathematics (extended version) ⋮ Generating custom set theories with non-set structured objects ⋮ Quotients of Bounded Natural Functors ⋮ Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL ⋮ Automating Change of Representation for Proofs in Discrete Mathematics ⋮ Unifying Heterogeneous State-Spaces with Lenses ⋮ Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL ⋮ Program logic for higher-order probabilistic programs in Isabelle/HOL ⋮ A verified ODE solver and the Lorenz attractor ⋮ CryptHOL: game-based proofs in higher-order logic ⋮ A Formalized Hierarchy of Probabilistic System Types ⋮ Automatic refinement to efficient data structures: a comparison of two approaches ⋮ FoCaLiZe and Dedukti to the rescue for proof interoperability ⋮ A Formal Proof of the Computation of Hermite Normal Form in a General Setting ⋮ Isabelle/HOL/GST: a formal proof environment for generalized set theories ⋮ Combining higher-order logic with set theory formalizations ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Markov chains and Markov decision processes in Isabelle/HOL ⋮ Towards a UTP Semantics for Modelica ⋮ The flow of ODEs: formalization of variational equation and Poincaré map ⋮ From types to sets by local type definition in higher-order logic ⋮ Friends with Benefits ⋮ Unnamed Item ⋮ Ornaments for Proof Reuse in Coq ⋮ Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. ⋮ A verified implementation of the Berlekamp-Zassenhaus factorization algorithm ⋮ Unifying theories of reactive design contracts ⋮ Effect polymorphism in higher-order logic (proof pearl) ⋮ Formalization of the Poincaré disc model of hyperbolic geometry ⋮ Effect polymorphism in higher-order logic (proof pearl) ⋮ Probabilistic Functions and Cryptographic Oracles in Higher Order Logic ⋮ Unnamed Item ⋮ Isabelle/UTP: A Mechanised Theory Engineering Framework ⋮ A verified implementation of algebraic numbers in Isabelle/HOL ⋮ Transfer ⋮ The Flow of ODEs ⋮ From Types to Sets by Local Type Definitions in Higher-Order Logic ⋮ Equational Reasoning with Applicative Functors ⋮ Algebraic Numbers in Isabelle/HOL ⋮ A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory ⋮ A formalization of the Smith normal form in higher-order logic ⋮ A formalization and proof checker for Isabelle's metalogic ⋮ On the fine-structure of regular algebra ⋮ Formalizing complex plane geometry

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• HOL
• Autoref
• Lifting

Cites Work

• Unnamed Item
• Unnamed Item
• Changing Data Representation within the Coq System
• Defining functions on equivalence classes
• Automatic Data Refinement
• Data Refinement in Isabelle/HOL
• Theorem Proving in Higher Order Logics
• Types for Proofs and Programs