ACL2
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Formalization of real analysis: a survey of proof assistants and libraries
- Integrating external deduction tools with ACL2
- Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
- HOL Light QE
- scientific article; zbMATH DE number 1765707 (Why is no real title available?)
- scientific article; zbMATH DE number 1798183 (Why is no real title available?)
- Mechanizing Mathematical Reasoning
- On the fine-structure of regular algebra
- ACE
- Matrix Operations
- FloPoCo
- Cyclist
- STeP
- Graphsc
- Pirate
- QuickSpec
- CLAM
- Openproof
- HOL90
- InKa
- Oyster
- Speedith
- VS3
- RADA
- JKind
- Lifting
- HOL2P
- Commons Math
- MoCHi
- LRAT
- Horus
- Transfer
- XASM
- GRATchk
- Kit
- GCminor
- foetus
- HimML
- reFLect
- VeriFun
- mural
- ANaConDA
- ASMKeY
- FRIDGE
- QuodLibet
- Tarski
- RDL
- AVL trees
- Cayley-Hamilton
- RealCertify
- Archive Formal Proofs
- Berlekamp Zassenhaus
- Dijkstra Shortest Path
- Depth First Search
- Echelon Form
- Guardol
- FELIX
- ComLisp
- HOL Light QE
- NASA PVS
- QR Decomposition
- Haskell Show Class
- SAEPTUM
- Piton
- RRL
- Light-weight Containers
- Centaur
- Splay Tree
- Decreasing Diagrams II
- petBoss
- Well Quasi Orders
- DrACuLa
- Treaps
- TAME
- Proof Pad
- Regexp
- MSVL
- DefunT
- Java+ITP
- K Prover
- Regular_Algebras
- TXDT
- aaflib
- PyInterval
- CakeML_Codegen
- Nominal2
- GenMul
- PolyCleaner
- RevSCA
- multgen
- Probabilistic_Prime_Tests
- XPlain
- ASM Workbench
- TSL
- ProverX
- Operational Reasoning for Concurrent Caml Programs and Weak Memory Models
- Reasoning About Incompletely Defined Programs
- Hammer for Coq: automation for dependent type theory
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
This page was built for software: ACL2
