Archive Formal Proofs
From MaRDI portal
swMATH28613MaRDI QIDQ40327FDOQ40327
Author name not available (Why is that?)
Official website: https://www.isa-afp.org
Cited In (only showing first 100 items - show all)
- Formalizing the Logic-Automaton Connection
- Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
- Conflict Analysis of Programs with Procedures, Dynamic Thread Creation, and Monitors
- Grail
- ACE
- KBCV
- DISCOUNT
- AmiCo
- RADA
- Lifting
- ltl2dstar
- Isabelle/UTP
- Fiat
- Circus
- Transfer
- GRAT
- GRATchk
- Kit
- WorkflowFM
- VACID-0
- cubicaltt
- CSimpl
- UTPCalc
- EROS
- Jordan
- kepler98
- MathOverflow
- GitLab
- HOLCF
- OpenCourseWare
- conauto
- Camelot
- DPT
- embed_modal
- sTeX
- Abstract Completeness
- Akra Bazzi
- AVL trees
- Applicative Lifting
- Algebraic Numbers
- Coinductive
- Amortized Complexity
- Cayley-Hamilton
- CAVA Automata Library
- CAVA
- BicolanoMT
- Berlekamp Zassenhaus
- Completeness theorem
- Naproche
- Decreasing Diagrams
- TiML
- Calife
- Dijkstra Shortest Path
- Depth First Search
- Ergodic theory
- CryptHOL
- Edmonds-Karp
- Echelon Form
- Datatype Order Generator
- FinFuns
- Deriving class
- Efficient Mergesort
- Flow Networks
- Gauss-Jordan
- Graph Theory
- Jinja Threads
- Gauss Jordan Elimination
- Hall Marriage
- Lp spaces
- Jordan Normal Forms
- KBPs
- Liouville numbers
- Knuth Bendix Orders
- Markov Models
- Logic2CNF
- Myhill-Nerode
- Meta Model Isabelle
- PairingHeap
- Monomorphic Monad
- Paraconsistency
- Perron Frobenius
- Psi-calculi
- QR Decomposition
- Refinement Monadic
- POSIX Lexing
- Presburger Automata
- Skew Heap
- Separation Logic
- VST-Floyd
- Splay Tree
- Stern-Brocot Tree
- Superposition Calculus
- Stuttering Equivalence
- Tame Graphs
- Timed Automata
- Stone Kleene
- Stone Algebras
- Zoo Probabilistic Systems
- Well Quasi Orders
- Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
This page was built for software: Archive Formal Proofs
