Cited in
(only showing first 100 items - show all)- Effect polymorphism in higher-order logic (proof pearl)
- scientific article; zbMATH DE number 7649960 (Why is no real title available?)
- Cubical Agda
- 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
- Complex_Geometry
- Poincare_Disc
- Hermite
- Modular_arithmetic_LLL_and_HNF_algorithms
- Smith_Normal_Form
- Smooth_Manifolds
- Friends with benefits. Implementing corecursion in foundational proof assistants
- Quasi-Borel Spaces
- Towards a UTP semantics for Modelica
- Unifying heterogeneous state-spaces with lenses
- 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
- The flow of ODEs: formalization of variational equation and Poincaré map
- scientific article; zbMATH DE number 7649970 (Why is no real title available?)
- Automating Change of Representation for Proofs in Discrete Mathematics
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Unifying theories of reactive design contracts
- Formalization of the Poincaré disc model of hyperbolic geometry
- Generating custom set theories with non-set structured objects
- scientific article; zbMATH DE number 7204430 (Why is no real title available?)
- Automating change of representation for proofs in discrete mathematics (extended version)
- CryptHOL: game-based proofs in higher-order logic
- Isabelle/Isar
- Isabelle/ZF
- HOL-Omega
- HOCL
- EasyCrypt
- Locales
- Autoref
- pGCL
- Isabelle/Circus
- HOL Zero
- Matrix Operations
- Ghostbuster
- AmiCo
- Isabelle/UTP
- Transfer
- WorkflowFM
- IsarMathLib
- CoSP
- HOLCF
- Tycon
- F*
- Applicative Lifting
- Cayley-Hamilton
- CAVA Automata Library
- Archive Formal Proofs
- CAVA
- Berlekamp Zassenhaus
- Ergodic theory
- CryptHOL
- Edmonds-Karp
- Echelon Form
- Gauss-Jordan
- Density Compiler
- Graph Theory
- Affine Arithmetic
- Lp spaces
- Knuth Bendix Orders
- Markov Models
- CAVA LTL Modelchecker
- Meta Model Isabelle
- Dictionary Construction
- Monomorphic Monad
- QR Decomposition
- Refinement Monadic
- Lambda Free RPOs
- Gabow SCC
- LTL_to_DRA
- Ordinary Differential Equations
- Ordinals Cardinals
- Light-weight Containers
- LTL_to_GBA
- Stern-Brocot Tree
- Rank Nullity
- Stone Algebras
- Real_Impl
- Zoo Probabilistic Systems
- Vector Spaces
- Tree Automata
- ProofPeer
- Count Complex Roots
- GeoCoq
- Linear Recurrences
- Program-Conflict-Analysis
This page was built for software: Lifting
