Syntactic Metatheory of Higher-Order Subtyping

DOI10.1007/978-3-540-87531-4_32zbMath1156.03311OpenAlexW2115318924MaRDI QIDQ3540196

Dulma Rodriguez, Andreas Abel

Publication date: 20 November 2008

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

Full work available at URL: https://doi.org/10.1007/978-3-540-87531-4_32

zbMATH Keywords

bounded quantificationalgorithmic subtypinghereditary substitutionhigher-order subtyping

Mathematics Subject Classification ID

Logic in computer science (03B70) Decidability of theories and sets of sentences (03B25) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An algebraic interpretation of the \(\lambda\beta K\)-calculus; and an application of a labelled \(\lambda\)-calculus
• Higher-order subtyping
• Typed operational semantics for higher-order subtyping.
• Towards a mechanized metatheory of standard ML
• Polarized Subtyping for Sized Types
• Implementing a normalizer using sized heterogeneous types
• Mechanizing metatheory in a logical framework
• Anti-symmetry of higher-order subtyping and equality by subtyping
• Types for Proofs and Programs
• Types for Proofs and Programs

This page was built for publication: Syntactic Metatheory of Higher-Order Subtyping