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

DOI10.1017/S0956796803004726zbMATH Open1088.68033OpenAlexW2168328957MaRDI QIDQ3377459FDOQ3377459

Authors Gilles Barthe, Thierry Coquand

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

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

Recommendations

• Remarks on the equational theory of non-normalizing pure type systems
• The structural theory of pure type systems
• scientific article; zbMATH DE number 1499107
• scientific article; zbMATH DE number 1301737
• Pure type systems with explicit substitutions

Cited in

(7)

• A partial type checking algorithm for Type:Type
• Equivalences between pure type systems and systems of illative combinatory logic
• Discussion on: ``On Aizerman's type problem for neutral type systems
• Remarks on the equational theory of non-normalizing pure type systems
• The structural theory of pure type systems
• Erasure and Polymorphism in Pure Type Systems
• Pure type systems with explicit substitutions

Describes a project that uses

Uses Software

• Automath

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3377459)