A generic strong normalization argument: Application to the calculus of constructions

DOI10.1007/BFB0049336MaRDI QIDQ4525289zbMATH OpenFDO

Authors Chih-Hao Luke Ong, Eike Ritter

Publication date 22 January 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0049336

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Categorical logic, topoi (03G30) Semantics in the theory of computing (68Q55)

Recommendations

• scientific article; zbMATH DE number 512780
• New Computational Paradigms
• Strong normalization in type systems: A model theoretical approach
• A generic normalisation proof for pure type systems
• On the proof theory of Coquand's calculus of constructions

Cited in

(6)

• Strong normalization for non-structural subtyping via saturated sets
• A direct proof of strong normalization for full constructive second-order logic
• scientific article; zbMATH DE number 512780 (Why is no real title available?)
• A short and flexible proof of strong normalization for the calculus of constructions
• The modified realizability topos
• Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions

Describes a project that uses

Uses Software

• Automath

This page was built for publication: A generic strong normalization argument: Application to the calculus of constructions

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