Lifting
From MaRDI portal
Lifting Q32823
Cited in
(only showing first 100 items - show all)- Cubical Agda
- Isabelle/Isar
- A verified ODE solver and the Lorenz attractor
- Markov chains and Markov decision processes in Isabelle/HOL
- Isabelle/ZF
- The flow of ODEs: formalization of variational equation and Poincaré map
- From types to sets by local type definition in higher-order logic
- HOL-Omega
- HOCL
- A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
- Unifying theories of reactive design contracts
- Formalization of the Poincaré disc model of hyperbolic geometry
- 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
- Generating custom set theories with non-set structured objects
- Program logic for higher-order probabilistic programs in Isabelle/HOL
- EasyCrypt
- CryptHOL: game-based proofs in higher-order logic
- A verified implementation of algebraic numbers in Isabelle/HOL
- On the fine-structure of regular algebra
- Formalizing complex plane geometry
- 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)
- Automatic refinement to efficient data structures: a comparison of two approaches
- Locales
- Autoref
- pGCL
- Isabelle/Circus
- Probabilistic functions and cryptographic oracles in higher order logic
- 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
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- HOL Zero
- Towards a UTP semantics for Modelica
- Friends with benefits. Implementing corecursion in foundational proof assistants
- Unifying heterogeneous state-spaces with lenses
- Ghostbuster
- Transfer
- AmiCo
- Isabelle/UTP
- WorkflowFM
- Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
- IsarMathLib
- Automating Change of Representation for Proofs in Discrete Mathematics
- HOLCF
- Tycon
- CoSP
- F*
- Ergodic theory
- Lp spaces
- Zoo Probabilistic Systems
- Edmonds-Karp
- Refinement Monadic
- Echelon Form
- Stern-Brocot Tree
- Cayley-Hamilton
- Gauss-Jordan
- QR Decomposition
- CAVA Automata Library
- CAVA
- Markov Models
- Graph Theory
- CryptHOL
- Monomorphic Monad
- Knuth Bendix Orders
- Applicative Lifting
- Meta Model Isabelle
- Berlekamp Zassenhaus
- Stone Algebras
- Archive Formal Proofs
- Density Compiler
- Vector Spaces
- Matrix Operations
- Lambda Free RPOs
- Dictionary Construction
- Affine Arithmetic
- Ordinary Differential Equations
- LTL_to_DRA
- CAVA LTL Modelchecker
- Tree Automata
- Ordinals Cardinals
- Gabow SCC
- Light-weight Containers
- Rank Nullity
- LTL_to_GBA
- Real_Impl
- ProofPeer
- Linear Recurrences
- Count Complex Roots
- Sqrt_Babylonian
- Program-Conflict-Analysis
- Regex_Equivalence
- GeoCoq
- OpenTheory
- Quotients of bounded natural functors
- Quotients of Bounded Natural Functors
- Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL
This page was built for software: Lifting
