Transfer

swMATH21009MaRDI QIDQ32822

No author found.

Described by source

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

Related Items (38)

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 ⋮ Automatic refinement to efficient data structures: a comparison of two approaches ⋮ 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 ⋮ 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 ⋮ A verified implementation of algebraic numbers in Isabelle/HOL ⋮ 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

This page was built for software: Transfer