Strong normalisation in two Pure Pattern Type Systems

DOI10.1017/S0960129508006749zbMATH Open1153.68027MaRDI QIDQ3520143FDOQ3520143

Authors: Benjamin Wack, Clément Houtmann 

Publication date: 15 August 2008

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

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (4)

• Strong normalization for typed terms with surjective pairing
• Title not available (Why is that?)
• Pure patterns type systems
• Weak normalization implies strong normalization in a class of non-dependent pure type systems

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)