A proof-irrelevant model of Martin-Löf's logical framework

DOI10.1017/S0960129502003766zbMath1029.03049MaRDI QIDQ4405694

Daniel Fridlender

Publication date: 8 February 2004

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

zbMATH Keywords

independenceconsistencyMartin-Löf's type theoryChurch numeralsuntyped lambda calculusMartin-Löf's logical frameworkPeano's fourth axiomproof-irrelevant model

Mathematics Subject Classification ID

Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Combinatory logic and lambda calculus (03B40)

Related Items (2)

Constructing a small category of setoids ⋮ Setoids and universes

This page was built for publication: A proof-irrelevant model of Martin-Löf's logical framework