Cited in
(37)- Proof-producing synthesis of CakeML from monadic HOL functions
- Programming and Proving with Classical Types
- JEFL: joint embedding of formal proof libraries
- Towards Knowledge Management for HOL Light
- scientific article; zbMATH DE number 7649970 (Why is no real title available?)
- Aligning concepts across proof assistant libraries
- On definitions of constants and types in HOL
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
- Matching concepts across HOL libraries
- A verified proof checker for higher-order logic
- Conversion of HOL Light proofs into Metamath
- TacticToe: learning to prove with tactics
- Classification of alignments between concepts of formal mathematical systems
- Proviola
- ProofPower
- MMT
- QMT
- Polar
- CakeML
- CERES
- Milawa
- Jitawa
- HOL Zero
- Tactician
- Menhir
- OEuf
- Light-weight Containers
- XIsabelle
- CoqInE
- Logipedia
- Jape
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
- Standalone Tactics Using OpenTheory
- A formalization and proof checker for Isabelle's metalogic
- Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
- A semantic framework for proof evidence
- System description: GAPT 2.0
This page was built for software: OpenTheory
