Pages that link to "Item:Q287361"
From MaRDI portal
The following pages link to Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (Q287361):
Displaying 12 items.
- Formalization of the resolution calculus for first-order logic (Q1663242) (← links)
- A verified proof checker for higher-order logic (Q1987736) (← links)
- Isabelle's metalogic: formalization and proof checker (Q2055847) (← links)
- A formalization and proof checker for Isabelle's metalogic (Q2108191) (← links)
- Proof-producing synthesis of CakeML from monadic HOL functions (Q2208292) (← links)
- \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic (Q2305408) (← links)
- Exercising Nuprl’s Open-Endedness (Q2819194) (← links)
- Formalization of the Resolution Calculus for First-Order Logic (Q2829269) (← links)
- Proof-Producing Reflection for HOL (Q2945631) (← links)
- (Q5091146) (← links)
- Programming and verifying a declarative first-order prover in Isabelle/HOL (Q5145439) (← links)
- (Q6060676) (← links)
