Transfer
From MaRDI portal
Cited in
(only showing first 100 items - show all)- 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
- 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
- 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
- Boolean_Expression_Checkers
- Game_Based_Crypto
- MFMC_Countable
- Probabilistic_While
- A verified ODE solver and the Lorenz attractor
- Program logic for higher-order probabilistic programs in Isabelle/HOL
- Quotients of Bounded Natural Functors
- Formalizing complex plane geometry
- scientific article; zbMATH DE number 7471712 (Why is no real title available?)
- 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
- ZFC_in_HOL
- Transition_Systems_and_Automata
- 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)
- scientific article; zbMATH DE number 7649960 (Why is no real title available?)
- Cubical Agda
- The flow of ODEs
This page was built for software: Transfer
