Strong normalisation in two Pure Pattern Type Systems

DOI10.1017/S0960129508006749MaRDI QIDQ3520143zbMATHFDO

Authors Benjamin Wack, Clément Houtmann

Publication date 15 August 2008

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

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Recommendations

• scientific article; zbMATH DE number 2163051
• Pure patterns type systems
• scientific article; zbMATH DE number 1301737
• Short Proofs of Strong Normalization
• scientific article; zbMATH DE number 1499107

Cites work

• A typed pattern calculus
• Combinatory reduction systems: Introduction and survey
• Inductive-data-type systems
• The calculus of constructions
• Theorem proving modulo

Cited in

(4)

• Pure patterns type systems
• scientific article; zbMATH DE number 2163051 (Why is no real title available?)
• Weak normalization implies strong normalization in a class of non-dependent pure type systems
• Strong normalization for typed terms with surjective pairing

Describes a project that uses

Uses Software

• Automath

This page was built for publication: Strong normalisation in two Pure Pattern Type Systems

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