Pure type systems with judgemental equality

DOI10.1017/S0956796805005770zbMath1088.68030MaRDI QIDQ3377462

Robin Adams

Publication date: 22 March 2006

Published in: Journal of Functional Programming (Search for Journal in Brave)

zbMATH Keywords

Church-Rosser theoremuniqueness of types

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Related Items (7)

Unified Syntax with Iso-types ⋮ I Got Plenty o’ Nuttin’ ⋮ Pure type systems with explicit substitutions ⋮ Unnamed Item ⋮ An adequacy theorem for dependent type theory ⋮ Pure Type System conversion is always typable ⋮ A Logical Framework with Explicit Conversions

Uses Software

• Automath

This page was built for publication: Pure type systems with judgemental equality