Possible forms of evaluation or reduction in Martin-Löf type theory

DOI10.1016/0304-3975(85)90065-9zbMath0612.03007OpenAlexW2082341006MaRDI QIDQ1087865

Martin W. Bunder

Publication date: 1985

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(85)90065-9

zbMATH Keywords

constructive mathematicsjudgementsnoncanonical expressions

Mathematics Subject Classification ID

Logic in computer science (03B70)

Related Items (1)

Equivalences between pure type systems and systems of illative combinatory logic

Cites Work

• Constructive mathematics and computer programming
• Unnamed Item

This page was built for publication: Possible forms of evaluation or reduction in Martin-Löf type theory