OpenTheory
From MaRDI portal
Software:44336
swMATH32625MaRDI QIDQ44336FDOQ44336
Author name not available (Why is that?)
Cited In (19)
- 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?)
- System Description: GAPT 2.0
- 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
- 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
- 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
- Matching Concepts across HOL Libraries
This page was built for software: OpenTheory
