ACL2
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Integrating external deduction tools with ACL2
- Efficiently checking propositional refutations in HOL theorem provers
- A rewriting logic approach to operational semantics
- Certifying properties of an efficient functional program for computing Gröbner bases
- Intelligent computer mathematics. 16th symposium, Calculemus 2009, 8th international conference, MKM 2009, held as part of CICM 2009, Grand Bend, Canada, July 6--12, 2009. Proceedings
- Adapting functional programs to higher order logic
- A verified common lisp implementation of Buchberger's algorithm in ACL2
- Inductive proof search modulo
- Proof assistants: history, ideas and future
- Operating system verification---an overview
- Coq
- Isabelle
- mizar-items
- Ott
- HolPy
- Theorema
- fKenzo
- ML
- DrScheme
- Prosper
- Partial functions in ACL2
- Isabelle/HOL
- JavaFAN
- VoDKA
- MizarMode
- CoqJVM
- VLISP
- ITP/OCL
- ASTRAL
- Structured theory development for a mechanized logic
- PVS
- Proof assistance for real-time systems using an interactive theorem prover
- Verification of FM9801: An out-of-order microprocessor model with speculative execution, exceptions, and program-modifying capability
- CoqEAL
- On the desirability of mechanizing calculational proofs
- Formal proofs about rewriting using ACL2
- StateFlow
- Iterated ultrapowers for the masses
- Hammer for Coq: automation for dependent type theory
- The formalization of discrete Fourier transform in HOL
- An elementary proof of the group law for elliptic curves
- SPASS+T
- MetaPRL
- Caduceus
- UCLID
- Mizar
- Superposition with structural induction
- Efficient, verified checking of propositional proofs
- Using abstract stobjs in ACL2 to compute matrix normal forms
- Gauge integral
- zChaff
- Reasoning about algebraic data types with abstractions
- FALKO
- Kenzo
- HAP
- Gappa
- Proof General
- LETOS
- Incorporating quotation and evaluation into Church's type theory
- HOL
- HOL Light QE
- AEtnaNova
- OCaml
- PIDE
- Verification of Year 2000 conversion rules using the ACL2 theorem prover
- METATEM
- HOL Light
- CeTA
- C-CoRN
- An experiment concerning mathematical proofs on computers with French undergraduate students
- Flocq
- ML4PG
- LISP
- Formalization of a normalization theorem in simplicial topology
- Principles of proof scores in CafeOBJ
- QuickCheck
- NQTHM
- ACL2s
- Zeno
- HipSpec
- Quantitative verification of Kalman filters
- MMT
- A graph library for Isabelle
- Coquelicot: a user-friendly library of real analysis for Coq
- Formalization of Euler-Lagrange equation set based on variational calculus in HOL light
- An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model
- LCF
- Separation logic-based verification atop a binary-compatible filesystem model
- versat
- CESAR
- CakeML
- TRX
- APS
- A formalization of the Smith normal form in higher-order logic
- EAT
- Coq/SSReflect
- Lem
- Deadlock in packet switching networks
- Toolchain
- DESUMA
This page was built for software: ACL2
