swMATH32625MaRDI QIDQ44336FDOQ44336
Author name not available (Why is that?)
Official website: http://www.gilith.com/opentheory/
Cited In (36)
- 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
- Title not available (Why is that?)
- 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
- Conversion of HOL Light proofs into Metamath
- A verified proof checker for higher-order logic
- TacticToe: learning to prove with tactics
- Classification of alignments between concepts of formal mathematical systems
- ProofPower
- MMT
- QMT
- Polar
- CakeML
- CERES
- Milawa
- Jitawa
- HOL Zero
- Tactician
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
- Menhir
- OEuf
- Light-weight Containers
- XIsabelle
- CoqInE
- Logipedia
- Jape
- 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
