Strong normalisation in two Pure Pattern Type Systems

DOI10.1017/S0960129508006749zbMath1153.68027MaRDI QIDQ3520143

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)

Uses Software

• Automath

Cites Work

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

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