Inclusions and subtypes II: higher-order case

DOI10.1093/LOGCOM/6.4.541zbMATH Open0931.03049OpenAlexW1967795995MaRDI QIDQ4895548FDOQ4895548

Authors: Narciso Martí-Oliet, José Meseguer 

Publication date: 28 February 2000

Published in: Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/ed79cc45466fa109a8e480669f93d81eed004ce4

Recommendations

• scientific article; zbMATH DE number 4027428
• Type system \(\lambda\omega\times_\leqq\)
• Foundations for the implementation of higher-order subtyping
• Higher-order subtyping

zbMATH Keywords

model categoriesinclusionimplicit conversionstructural subtypinghigher-order categorical semanticshigher-order equational logichomomorphism between modelsinclusive subtypes

Mathematics Subject Classification ID

Logic in computer science (03B70) Categorical logic, topoi (03G30) Semantics in the theory of computing (68Q55)

Cited In (5)

• Strict coherence of conditional rewriting modulo axioms
• Type system \(\lambda\omega\times_\leqq\)
• An abstract formalization of correct schemas for program synthesis
• Specification and proof in membership equational logic
• Inclusions and subtypes I: first-order case

This page was built for publication: Inclusions and subtypes II: higher-order case

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