scientific article; zbMATH DE number 1301737

MaRDI QIDQ4246950zbMATH OpenFDO

Authors Paul-André Melliès, Benjamin Werner

Publication date 13 December 1999

zbMATH Keywords

lambda calculusstrong normalisationpure type systems

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Recommendations

• scientific article; zbMATH DE number 1499107
• scientific article; zbMATH DE number 2163051
• The structural theory of pure type systems
• Strong normalisation in two Pure Pattern Type Systems
• A schematic proof of strong normalization for the system of the \(\lambda\)-cube

Cited in

(17)

• Expansion postponement for normalising pure type systems
• scientific article; zbMATH DE number 1231477 (Why is no real title available?)
• A schematic proof of strong normalization for the system of the \(\lambda\)-cube
• The structural theory of pure type systems
• scientific article; zbMATH DE number 2163051 (Why is no real title available?)
• Pure type systems with more liberal rules
• Strong normalisation in two Pure Pattern Type Systems
• (Head-)normalization of typeable rewrite systems
• Sharing proofs with predicative theories through universe-polymorphic elaboration
• scientific article; zbMATH DE number 683355 (Why is no real title available?)
• Remarks on the equational theory of non-normalizing pure type systems
• Remarks on the equational theory of non-normalizing pure type systems
• scientific article; zbMATH DE number 2185650 (Why is no real title available?)
• Strong normalization with non-structural subtyping
• Weak normalization implies strong normalization in a class of non-dependent pure type systems
• scientific article; zbMATH DE number 1555189 (Why is no real title available?)
• Normalization results for typeable rewrite systems

This page was built for publication:

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