Intersection type assignment systems with higher-order algebraic rewriting

DOI10.1016/S0304-3975(96)80706-7zbMath0874.03016OpenAlexW4234327515MaRDI QIDQ672048

Franco Barbanera, Maribel Fernández

Publication date: 27 February 1997

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(96)80706-7

zbMATH Keywords

completenessintersection typesstrong normalizationtype assignmentextensions of \(\lambda\)-calculi with algebraic rewriting

Mathematics Subject Classification ID

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

Related Items (4)

Nominal rewriting ⋮ On modular properties of higher order extensional lambda calculi ⋮ A metamodel of access control for distributed environments: applications and properties ⋮ Principal Types for Nominal Theories

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The heart of intersection type assignment: Normalisation proofs revisited
• Counterexamples to termination for the direct sum of term rewriting systems
• On termination of the direct sum of term-rewriting systems
• An extension of basic functionality theory for \(\lambda\)-calculus
• Polymorphic rewriting conserves algebraic strong normalization
• Combinatory reduction systems: Introduction and survey
• Edinburgh LCF. A mechanized logic of computation
• Typing and computational properties of lambda expressions
• Comparing curried and uncurried rewriting
• On theories with a combinatorial definition of 'equivalence'
• A filter lambda model and the completeness of type assignment
• COMBINING TERM REWRITING AND TYPE ASSIGNMENT SYSTEMS
• Modularity of strong normalization in the algebraic-λ-cube

This page was built for publication: Intersection type assignment systems with higher-order algebraic rewriting