Pages that link to "Item:Q2938044"

The following pages link to Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL (Q2938044):

Displaying 44 items.

• Transfer (Q32822) (← links)
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL (Q333325) (← links)
• A verified ODE solver and the Lorenz attractor (Q1663218) (← links)
• FoCaLiZe and Dedukti to the rescue for proof interoperability (Q1687726) (← links)
• Markov chains and Markov decision processes in Isabelle/HOL (Q1701041) (← links)
• The flow of ODEs: formalization of variational equation and Poincaré map (Q1722644) (← links)
• From types to sets by local type definition in higher-order logic (Q1722645) (← links)
• A verified implementation of the Berlekamp-Zassenhaus factorization algorithm (Q1984794) (← links)
• Unifying theories of reactive design contracts (Q2007732) (← links)
• Formalization of the Poincaré disc model of hyperbolic geometry (Q2031408) (← links)
• A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory (Q2102926) (← links)
• A formalization of the Smith normal form in higher-order logic (Q2102950) (← links)
• A formalization and proof checker for Isabelle's metalogic (Q2108191) (← links)
• Generating custom set theories with non-set structured objects (Q2128829) (← links)
• Program logic for higher-order probabilistic programs in Isabelle/HOL (Q2163157) (← links)
• CryptHOL: game-based proofs in higher-order logic (Q2175214) (← links)
• A verified implementation of algebraic numbers in Isabelle/HOL (Q2303244) (← links)
• On the fine-structure of regular algebra (Q2352506) (← links)
• Formalizing complex plane geometry (Q2354913) (← links)
• A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem (Q2362109) (← links)
• Automating change of representation for proofs in discrete mathematics (extended version) (Q2364883) (← links)
• Automatic refinement to efficient data structures: a comparison of two approaches (Q2417948) (← links)
• Probabilistic Functions and Cryptographic Oracles in Higher Order Logic (Q2802495) (← links)
• Isabelle/UTP: A Mechanised Theory Engineering Framework (Q2814613) (← links)
• The Flow of ODEs (Q2829258) (← links)
• From Types to Sets by Local Type Definitions in Higher-Order Logic (Q2829259) (← links)
• Equational Reasoning with Applicative Functors (Q2829262) (← links)
• Algebraic Numbers in Isabelle/HOL (Q2829274) (← links)
• A Formalized Hierarchy of Probabilistic System Types (Q2945633) (← links)
• Towards a UTP Semantics for Modelica (Q2971175) (← links)
• Friends with Benefits (Q2988636) (← links)
• Unifying Heterogeneous State-Spaces with Lenses (Q3179407) (← links)
• Automating Change of Representation for Proofs in Discrete Mathematics (Q3453117) (← links)
• (Q5028480) (← links)
• Quotients of Bounded Natural Functors (Q5048992) (← links)
• Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL (Q5049005) (← links)
• (Q5111307) (← links)
• Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. (Q5875415) (← links)
• (Q5875419) (← links)
• (Q5875430) (← links)
• Ornaments for Proof Reuse in Coq (Q5875438) (← links)
• Effect polymorphism in higher-order logic (proof pearl) (Q5915785) (← links)
• Effect polymorphism in higher-order logic (proof pearl) (Q5919584) (← links)
• Combining higher-order logic with set theory formalizations (Q6161232) (← links)