Polarised subtyping for sized types

DOI10.1017/S0960129508006853zbMath1156.68014MaRDI QIDQ3535676

Andreas Abel

Publication date: 13 November 2008

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

zbMATH Keywords

subtyping calculus

Mathematics Subject Classification ID

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

Related Items (2)

Well-founded recursion with copatterns and sized types ⋮ Unnamed Item

Cites Work

• Perpetual reductions in \(\lambda\)-calculus
• Higher-order subtyping
• Typed operational semantics for higher-order subtyping.
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• Iteration and coiteration schemes for higher-order and nested datatypes
• de Bruijn notation as a nested datatype
• Type-based termination of recursive definitions
• Generalizing generalized tries
• On equivalence and canonical forms in the LF type theory
• Anti-symmetry of higher-order subtyping and equality by subtyping

This page was built for publication: Polarised subtyping for sized types