Redundancy Elimination for LF

DOI10.1016/j.entcs.2007.11.014zbMath1278.03064OpenAlexW2126773497MaRDI QIDQ2871840

Jason Reed

Publication date: 10 January 2014

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.2007.11.014

zbMATH Keywords

proof compressiondependent type theorybidirectional type checking

Mathematics Subject Classification ID

Logic in computer science (03B70)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Structural cut elimination. I: Intuitionistic and classical logic
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A framework for defining logics
• On equivalence and canonical forms in the LF type theory
• Types for Proofs and Programs

This page was built for publication: Redundancy Elimination for LF