Explicit contexts in LF (extended abstract)

DOI10.1016/J.ENTCS.2008.12.116MaRDI QIDQ2804940zbMATH OpenOpenAlexFDO

Authors Karl Crary

Publication date 6 May 2016

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2008.12.116

zbMATH Keywords

dependent typesLFTwelf

Mathematics Subject Classification ID

Logic in computer science (03B70)

Recommendations

• Mechanizing metatheory in a logical framework
• Mechanizing the metatheory of LF
• scientific article; zbMATH DE number 1348473
• Canonical HybridLF: extending Hybrid with dependent types
• scientific article; zbMATH DE number 4180831

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)

• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey

Describes a project that uses

Uses Software

• Twelf
• PoplMark

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)