Subtyping + extensionality: Confluence of βηtop reduction in F≤

DOI10.1007/3-540-54415-1_72zbMath1493.68103OpenAlexW27254708MaRDI QIDQ5096246

Pierre-Louis Curien, Giorgio Ghelli

Publication date: 16 August 2022

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

Full work available at URL: https://doi.org/10.1007/3-540-54415-1_72

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Grammars and rewriting systems (68Q42) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40)

Related Items

Higher-order subtyping, Unification in an extensional lambda calculus with ordered function sorts and constant overloading

Cites Work

• A modest model of records, inheritance, and bounded quantification
• An extension of system \(F\) with subtyping
• A semantic basis for Quest
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item