Explicit contexts in LF (extended abstract)
From MaRDI portal
Publication:2804940
Recommendations
Cites work
- A framework for defining logics
- A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
- Contextual modal type theory
- Higher-order superposition for dependent types
- Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF
- Theorem Proving in Higher Order Logics
- Towards a mechanized metatheory of Standard ML
- Types for Proofs and Programs
Cited in
(1)
This page was built for publication: Explicit contexts in LF (extended abstract)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2804940)