Explicit Contexts in LF (Extended Abstract)

DOI10.1016/j.entcs.2008.12.116zbMath1337.68237OpenAlexW2000861240MaRDI QIDQ2804940

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)

Related Items (1)

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

Uses Software

• Twelf
• PoplMark

Cites Work

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

This page was built for publication: Explicit Contexts in LF (Extended Abstract)