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

DOI10.1007/3-540-54415-1_72zbMath1493.68103MaRDI 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

03B25: Decidability of theories and sets of sentences

68Q42: Grammars and rewriting systems

18D15: Closed categories (closed monoidal and Cartesian closed categories, etc.)

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

03B40: Combinatory logic and lambda calculus

Related Items

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