Transfer

swMATH21009MaRDI QIDQ32822FDOQ32822

Author name not available (Why is that?)

Described by source

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

Cited In (38)

• From types to sets by local type definition in higher-order logic
• A formalization of the Smith normal form in higher-order logic
• From types to sets by local type definitions in higher-order logic
• Algebraic numbers in Isabelle/HOL
• On the fine-structure of regular algebra
• A verified implementation of algebraic numbers in Isabelle/HOL
• A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
• A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
• Title not available (Why is that?)
• The flow of ODEs: formalization of variational equation and Poincaré map
• Automating Change of Representation for Proofs in Discrete Mathematics
• Unifying theories of reactive design contracts
• Formalization of the Poincaré disc model of hyperbolic geometry
• Generating custom set theories with non-set structured objects
• Title not available (Why is that?)
• Automating change of representation for proofs in discrete mathematics (extended version)
• CryptHOL: game-based proofs in higher-order logic
• A verified ODE solver and the Lorenz attractor
• Quotients of Bounded Natural Functors
• Program logic for higher-order probabilistic programs in Isabelle/HOL
• Title not available (Why is that?)
• Formalizing complex plane geometry
• Equational Reasoning with Applicative Functors
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory
• A formalization and proof checker for Isabelle's metalogic
• Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL
• Effect polymorphism in higher-order logic (proof pearl)
• Title not available (Why is that?)
• The flow of ODEs
• Probabilistic functions and cryptographic oracles in higher order logic
• Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
• Automatic refinement to efficient data structures: a comparison of two approaches
• Markov chains and Markov decision processes in Isabelle/HOL
• Ornaments for Proof Reuse in Coq
• Friends with benefits. Implementing corecursion in foundational proof assistants
• Unifying heterogeneous state-spaces with lenses
• Towards a UTP semantics for Modelica

This page was built for software: Transfer