Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
From MaRDI portal
Publication:2938044
DOI10.1007/978-3-319-03545-1_9zbMath1426.68284OpenAlexW101424827MaRDI QIDQ2938044
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
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
Cites Work
