Cited in
(33)- Proof-producing synthesis of ML from higher-order logic
- A consistent foundation for Isabelle/HOL
- Milestones from the Pure Lisp Theorem Prover to ACL2
- A verified runtime for a verified theorem prover
- Aligning concepts across proof assistant libraries
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
- A verified generational garbage collector for CakeML
- Verifying a concurrent garbage collector with a rely-guarantee methodology
- A verified generational garbage collector for CakeML
- Towards a formally verified proof assistant
- VLISP
- Polar
- CompCertTSO
- CakeML
- IsaFoR
- Jitawa
- HOL Zero
- Proof-producing reflection for HOL. With an application to model polymorphism
- A verified theorem prover backend supported by a monotonic library
- CertiCoq
- GCminor
- Light-weight Containers
- DefunT
- OpenTheory
- TXDT
- Metamath Zero
- PRECiSA
- Formalization of the resolution calculus for first-order logic
- A formalization and proof checker for Isabelle's metalogic
- A verified proof checker for higher-order logic
- Steps towards Verified Implementations of HOL Light
- HOL Zero's solutions for Pollack-inconsistency
- Interactive theorem proving. 5th international conference, ITP 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14--17, 2014. Proceedings
This page was built for software: Milawa
