Subtyping dependent types

DOI10.1016/S0304-3975(00)00175-4zbMath0989.68020MaRDI QIDQ5958760

Adriana Compagnoni, David Aspinall

Publication date: 3 March 2002

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

zbMATH Keywords

type theorydependent typessubtyping

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (15)

A Delta for Hybrid Type Checking ⋮ Automath Type Inclusion in Barendregt’s Cube ⋮ Higher-order subtyping and its decidability ⋮ Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters ⋮ Realist Consequence, Epistemic Inference, Computational Correctness ⋮ Typed operational semantics for higher-order subtyping. ⋮ Structural subtyping for inductive types with functorial equality rules ⋮ Polymorphic Contracts ⋮ Implicit coercions in type systems ⋮ Roles, stacks, histories: A triple for Hoare ⋮ Subtyping dependent types ⋮ Coherence of subsumption for monadic types ⋮ Dependent type system with subtyping I: Type level transitivity elimination ⋮ Order-sorted inductive types ⋮ Dependent types with subtyping and late-bound overloading

Uses Software

• Automath

Cites Work

• Using typed lambda calculus to implement formal systems on a machine
• The calculus of constructions
• Inheritance as implicit coercion
• Toward formal development of programs from algebraic specifications: Parameterisation revisited
• Typed operational semantics for higher-order subtyping.
• Coherence of subsumption, minimum typing and type-checking in F ≤
• A framework for defining logics
• Coercive subtyping
• Simple type-theoretic foundations for object-oriented programming
• Anti-symmetry of higher-order subtyping and equality by subtyping
• Subtyping dependent types
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Subtyping dependent types