Remarks on the equational theory of non-normalizing pure type systems

DOI10.1017/S0956796803004726zbMath1088.68033OpenAlexW2168328957MaRDI QIDQ3377459

Thierry Coquand, Gilles Barthe

Publication date: 22 March 2006

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

Full work available at URL: https://doi.org/10.1017/s0956796803004726

Mathematics Subject Classification ID

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

Related Items (2)

Pure type systems with explicit substitutions ⋮ A Partial Type Checking Algorithm for Type:Type

Uses Software

• Automath

This page was built for publication: Remarks on the equational theory of non-normalizing pure type systems