Transfer
From MaRDI portal
swMATH21009MaRDI QIDQ32822FDOQ32822
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)
- 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
- Poincare_Disc
- 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
- CryptHOL: game-based proofs in higher-order logic
- 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
- Lifting
- Isabelle/UTP
- 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
- 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
- Real_Impl
- Zoo Probabilistic Systems
- Vector Spaces
- Tree Automata
- ProofPeer
- Count Complex Roots
- GeoCoq
- Linear Recurrences
- Program-Conflict-Analysis
- Regex_Equivalence
- Sqrt_Babylonian
- Equational Reasoning with Applicative Functors
- Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
- Boolean_Expression_Checkers
- Game_Based_Crypto
- MFMC_Countable
- Probabilistic_While
- 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
- Title not available (Why is that?)
- The flow of ODEs
- Probabilistic functions and cryptographic oracles in higher order logic
- Markov chains and Markov decision processes in Isabelle/HOL
- Ornaments for Proof Reuse in Coq
- Cubical Agda
- Friends with benefits. Implementing corecursion in foundational proof assistants
- Unifying heterogeneous state-spaces with lenses
- Towards a UTP semantics for Modelica
- 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
- Title not available (Why is that?)
This page was built for software: Transfer
