On the subject reduction property for algebraic type systems

DOI10.1007/3-540-63172-0_31MaRDI QIDQ4362909zbMATH OpenFDO

Authors Gilles Barthe, Paul-André Melliès

Publication date 13 November 1997

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

Full work available at URL https://ir.cwi.nl/pub/1307

zbMATH Keywords

algebraic type systemsconfluencelabelled syntaxstrong normalizationSubject Reductiontyped \(\lambda\)-calculityped rewriting systems

Mathematics Subject Classification ID

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

Recommendations

• ON THE REDUCTION OF TYPE THEORY
• Reductions, intersection types, and explicit substitutions
• Reductions, intersection types, and explicit substitutions
• Typed Lambda Calculi and Applications
• Modular properties of algebraic type systems
• A type reduction from proof-conditional to dynamic semantics
• Reducibility of types in typed lambda calculus. Comment on a paper by Richard Statman
• Reduction and unification in lambda calculi with a general notion of subtype
• Reducibility: a ubiquitous method in lambda calculus with intersection types
• An algebraic semantics of higher-order types with subtypes

Cited in

(8)

• An algebraic view on recursive types
• A note on subject reduction in (, )-Curry with respect to complete developments
• scientific article; zbMATH DE number 445155 (Why is no real title available?)
• scientific article; zbMATH DE number 1797606 (Why is no real title available?)
• Modular properties of algebraic type systems
• Optimizing optimal reduction
• Typed Lambda Calculi and Applications
• Subject Reduction in Multi-Universe Type Theories

Describes a project that uses

Uses Software

• Automath

This page was built for publication: On the subject reduction property for algebraic type systems

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