Lifting

swMATH21010MaRDI QIDQ32823FDOQ32823

Author name not available (Why is that?)

Cited In (39)

• Probabilistic Functions and Cryptographic Oracles in Higher Order Logic
• The Flow of ODEs
• From types to sets by local type definition in higher-order logic
• A formalization of the Smith normal form in higher-order logic
• 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
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Friends with Benefits
• Unifying theories of reactive design contracts
• Towards a UTP Semantics for Modelica
• Formalization of the Poincaré disc model of hyperbolic geometry
• Unifying Heterogeneous State-Spaces with Lenses
• Generating custom set theories with non-set structured objects
• Algebraic Numbers in Isabelle/HOL
• From Types to Sets by Local Type Definitions in Higher-Order Logic
• 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?)
• 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

This page was built for software: Lifting