Explicit contexts in LF (extended abstract)

DOI10.1016/J.ENTCS.2008.12.116zbMATH Open1337.68237OpenAlexW2000861240MaRDI QIDQ2804940FDOQ2804940

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

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
• Publication:3204067

zbMATH Keywords

dependent typesLFTwelf

Mathematics Subject Classification ID

Logic in computer science (03B70)

Cites Work

• Theorem Proving in Higher Order Logics
• A framework for defining logics
• Contextual modal type theory
• Types for Proofs and Programs
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• Towards a mechanized metatheory of standard ML
• Higher-order superposition for dependent types
• Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF

Cited In (1)

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

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)