Paper Info
Title
Subtyping over a Lattice (Abstract)
Abstract
This talk, in the first part, will overview the main advances in the area of subtyping for the simply typed lambda calculus. In the second part of the talk we will propose a new system of notations for types, which we call alternating direct acyclic graphs, and show that for a system of sybtype inequalities over a lattice, if it has a solution then there is a solution whose alternating dag is of polynomial size in the size of the original system. There are examples showing that the well known dag representation of types is not good enough for this purpose, already for the two-element lattice.
Year
DOI
Venue
1997
10.1007/3-540-63385-5_34
Kurt Gödel Colloquium
Keywords
Field
DocType
directed acyclic graph,typed lambda calculus
Discrete mathematics,Algebra,Polynomial,Simply typed lambda calculus,Typed lambda calculus,Lambda cube,Fixed-point combinator,System F,Subtyping,Dependent type,Mathematics
Conference
ISBN
Citations 
PageRank 
3-540-63385-5
2
0.41
References 
Authors
5
1
Name
Order
Citations
PageRank
Jerzy Tiuryn11210126.00