OpenTheory
From MaRDI portal
Software:44336
No author found.
Related Items (19)
Classification of alignments between concepts of formal mathematical systems ⋮ The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ On definitions of constants and types in HOL ⋮ Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation ⋮ JEFL: joint embedding of formal proof libraries ⋮ Programming and Proving with Classical Types ⋮ Aligning concepts across proof assistant libraries ⋮ Standalone Tactics Using OpenTheory ⋮ Unnamed Item ⋮ A semantic framework for proof evidence ⋮ Proof-producing synthesis of CakeML from monadic HOL functions ⋮ A verified proof checker for higher-order logic ⋮ TacticToe: learning to prove with tactics ⋮ System Description: GAPT 2.0 ⋮ Matching Concepts across HOL Libraries ⋮ Towards Knowledge Management for HOL Light ⋮ Conversion of HOL Light proofs into Metamath ⋮ Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC ⋮ A formalization and proof checker for Isabelle's metalogic
This page was built for software: OpenTheory
