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.
Partly supported by NSF grant CCR-9417382 and by Polish KBN Grant 8 T11C 034 10.
Preview
Unable to display preview. Download preview PDF.
References
M. Benke. Efficient type reconstruction in the presence of inheritance. In Eds. A. M. Borzyszkowski, S. Sokolowski, editor, MFCS'93: Mathematical Foundations of Computer Science, Proc. 18th Intern. Symp., volume 711 of Lecture Notes in Computer Science, pages 272–280. Springer Verlag, 1993.
C. Dwork, P. Kanellakis, and J.C. Mitchell. On the sequential nature of unification. J. Logic Programming, 1:35–50, 1984.
A. Frey. Solving subtype inequalities in polynomial space. available from http://www.ensmp.fr/frey/Notes/frey-02-v1.2.ps.gz, 1997.
M. Hoang and J.C. Mitchell. Lower bounds on type inference with subtypes. In Conf. Rec. 22nd ACM Symposium on Principles of Programming Languages, pages 176–185, 1995.
J. Tiuryn. Subtype inequalities. In Proc. IEEE Symp. on Logic in Computer Science, pages 308–315, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tiuryn, J. (1997). Subtyping over a lattice (abstract). In: Gottlob, G., Leitsch, A., Mundici, D. (eds) Computational Logic and Proof Theory. KGC 1997. Lecture Notes in Computer Science, vol 1289. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63385-5_34
Download citation
DOI: https://doi.org/10.1007/3-540-63385-5_34
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63385-3
Online ISBN: 978-3-540-69806-7
eBook Packages: Springer Book Archive