scientific article; zbMATH DE number 1086659

MaRDI QIDQ4362909zbMATH OpenFDO

Authors Gilles Barthe, Paul-André Melliès

Publication date 13 November 1997

zbMATH Keywords

confluencestrong normalizationtyped \(\lambda\)-calculialgebraic type systemslabelled syntaxSubject Reductiontyped rewriting systems

Mathematics Subject Classification ID

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

Recommendations

• ON THE REDUCTION OF TYPE THEORY
• scientific article; zbMATH DE number 1722651
• 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

(7)

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

Describes a project that uses

Uses Software

• Automath

This page was built for publication:

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