Some logical and syntactical observations concerning the first-order dependent type system λP

DOI10.1017/S0960129599002856zbMath0939.03016MaRDI QIDQ4704760

Herman Geuvers, Erik Barendsen

Publication date: 29 June 2000

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

zbMATH Keywords

completenessformulas as typesgeneralized type theoryminimal predicate logic

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40)

Related Items (2)

Introduction to Type Theory ⋮ \texttt{slepice}: towards a verified implementation of type theory in type theory

Uses Software

• Automath

This page was built for publication: Some logical and syntactical observations concerning the first-order dependent type system λP