ACL2
From MaRDI portal
swMATH60WikidataQ4650692 ScholiaQ4650692MaRDI QIDQ12833FDOQ12833
Author name not available (Why is that?)
Official website: https://www.cs.utexas.edu/~moore/acl2/
Source code repository: https://github.com/acl2/acl2
Cited In (only showing first 100 items - show all)
- On the fine-structure of regular algebra
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Automating Induction with an SMT Solver
- A Brief Overview of HOL4
- Theorema
- ML
- Prosper
- MizarMode
- Caduceus
- StateFlow
- MetaPRL
- Mizar
- FALKO
- HAP
- Gappa
- Kenzo
- SPASS+T
- Proof General
- UCLID
- LETOS
- zChaff
- HOL
- AEtnaNova
- OCaml
- PIDE
- CeTA
- HOL Light
- METATEM
- C-CoRN
- Flocq
- ML4PG
- LISP
- QuickCheck
- NQTHM
- MMT
- Title not available (Why is that?)
- ACL2s
- HipSpec
- Zeno
- LCF
- CESAR
- CakeML
- APS
- versat
- EAT
- Coq/SSReflect
- TRX
- Lem
- DESUMA
- GIDDES
- CompCert
- CoLoR
- Minlog
- Amphion
- ITP
- CiME
- Dist-Orc
- Milawa
- Toolchain
- PAF!
- PARTHEO
- PhoX
- MOMENT2
- SicoTHEO
- Flyspeck
- Ivy
- PROSPER
- TSOTool
- Coquelicot
- InVeSt
- MDGs
- Specware
- Manip
- PVSio
- Referee
- ABC
- Jitawa
- EVC
- vlogsl
- QuickChick
- ROSCoq
- TCT
- OpenMath
- seL4
- KIDS
- 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)
- HOL Light QE
- FloPoCo
- Cyclist
- STeP
- Graphsc
- Pirate
- QuickSpec
- Openproof
- Speedith
- Mizar: state-of-the-art and beyond
- Hammer for Coq: automation for dependent type theory
- Coquelicot: a user-friendly library of real analysis for Coq
- Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals
This page was built for software: ACL2
