Abstract
We study an annotated type and effect system that integrates let-polymorphism, effects, and subtyping into an annotated type and effect system for a fragment of Concurrent ML. First we define a type inference algorithm and then construct procedures for constraint normalisation and simplification. Next these algorithms are proved syntactically sound with respect to the annotated type and effect system.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
T. Amtoft, F. Nielson, H.R. Nielson, J. Ammann: Polymorphic subtypes for effect analysis: the dynamic semantics. This volume of SLNCS, 1997.
Y.-C. Fuh and P. Mishra: Polymorphic subtype inference: closing the theory-practice gap. In Proc. TAPSOFT '89. SLNCS 352, 1989.
Y.-C. Fuh and P. Mishra: Type inference with subtypes. Theoretical Computer Science, 73, 1990.
F. Henglein and C. Mossin: Polymorphic binding-time analysis. In Proc. ESOP '94, pages 287–301. SLNCS 788, 1994.
M.P. Jones: A theory of qualified types. In Proc. ESOP '92, pages 287–306. SLNCS 582, 1992.
P. Jouvelot and D.K. Gifford: Algebraic reconstruction of types and effects. In Proc. POPL'91, pages 303–310. ACM Press, 1991.
R. Milner: A theory of type polymorphism in programming. Journal of Computer Systems, 17:348–375, 1978.
J.C. Mitchell: Type inference with simple subtypes. Journal of Functional Programming, 1(3), 1991.
F. Nielson and H.R. Nielson: Constraints for polymorphic behaviours for Concurrent ML. In Proc. CCL'94. SLNCS 845, 1994.
H.R. Nielson and F. Nielson: Higher-order concurrent programs with finite communication topology. In Proc. POPL'94, pages 84–97. ACM Press, 1994.
H.R. Nielson, F. Nielson, T. Amtoft: Polymorphic subtypes for effect analysis: the static semantics. This volume of SLNCS, 1997.
P. Panangaden and J.H. Reppy: The essence of Concurrent ML. In ML with Concurrency: Design, Analysis, Implementation and Application (editor: Flemming Nielson), Springer-Verlag, 1996.
J.H. Siekmann: Unification theory. J. Symbolic Computation, 7:207–274, 1989.
G.S. Smith: Polymorphic type inference for languages with overloading and subtyping. Ph.D thesis from Cornell, 1991.
G.S. Smith: Polymorphic inference with overloading and subtyping. In SLNCS 668, Proc. TAPSOFT '93, 1993. Also see: Principal type schemes for functional programs with overloading and subtyping: Science of Computer Programming 23, pp. 197–226, 1994.
J.P. Talpin and P. Jouvelot: Polymorphic type, region and effect inference. Journal of Functional Programming, 2(3), pages 245–271, 1992.
J.P. Talpin and P. Jouvelot: The type and effect discipline. Information and Computation, 111, 1994.
Y.-M. Tang: Control flow analysis by effect systems and abstract interpretation. PhD thesis, Ecoles des Mines de Paris, 1994.
M. Tofte. Type inference for polymorphic references. Information and Computation, 89:1–34, 1990.
M. Tofte and L. Birkedal: Region-annotated types and type schemes, 1996. Submitted for publication.
A.K. Wright: Typing references by effect inference. In Proc. ESOP '92, pages 473–491. SLNCS 582, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nielson, F., Riis Nielson, H., Amtoft, T. (1997). Polymorphic subtyping for effect analysis: The algorithm. In: Dam, M. (eds) Analysis and Verification of Multiple-Agent Languages. LOMAPS 1996. Lecture Notes in Computer Science, vol 1192. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-62503-8_10
Download citation
DOI: https://doi.org/10.1007/3-540-62503-8_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62503-2
Online ISBN: 978-3-540-68052-9
eBook Packages: Springer Book Archive