swMATH21010MaRDI QIDQ32823FDOQ32823
Author name not available (Why is that?)
Official website: https://link.springer.com/chapter/10.1007/978-3-319-03545-1_9
Cited In (only showing first 100 items - show all)
- ZFC_in_HOL
- Transition_Systems_and_Automata
- A formalization of the Smith normal form in higher-order logic
- A verified implementation of algebraic numbers in Isabelle/HOL
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- Complex_Geometry
- Poincare_Disc
- Title not available (Why is that?)
- Quasi-Borel Spaces
- 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
- Quotients of Bounded Natural Functors
- Program logic for higher-order probabilistic programs in Isabelle/HOL
- Title not available (Why is that?)
- Equational Reasoning with Applicative Functors
- Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL
- Effect polymorphism in higher-order logic (proof pearl)
- Hermite
- Modular_arithmetic_LLL_and_HNF_algorithms
- Smith_Normal_Form
- Smooth_Manifolds
- Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
- Automatic refinement to efficient data structures: a comparison of two approaches
- From types to sets by local type definition 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 the Berlekamp-Zassenhaus factorization algorithm
- 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
- Unifying theories of reactive design contracts
- A verified ODE solver and the Lorenz attractor
- Isabelle/Isar
- Isabelle/ZF
- HOL-Omega
- HOCL
- EasyCrypt
- Locales
- Autoref
- pGCL
- Isabelle/Circus
- HOL Zero
- Formalizing complex plane geometry
- 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
