Inclusions and subtypes II: higher-order case

DOI10.1093/LOGCOM/6.4.541MaRDI QIDQ4895548zbMATH OpenOpenAlexFDO

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

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)

Recommendations

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

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)