×

zbMATH — the first resource for mathematics

Polymorphic type, region and effect inference. (English) Zbl 0817.68099
Summary: We present a new static system which reconstructs the types, regions and effects of expressions in an implicitly typed functional language that supports imperative operations on reference values. Just as types structurally abstract collections of concrete values, regions represent sets of possibly aliased reference values and effects represent approximations of the imperative behaviour on regions. We introduce a static semantics for inferring types, regions and effects, and prove that it is consistent with respect to the dynamic semantics of the language. We present a reconstruction algorithm that computes the types and effects of expressions, and assigns regions to reference values. We prove the correctness of the reconstruction algorithm with respect to the static semantics. Finally, we discuss potential applications of our system to automatic stack allocation and parallel code generation.

MSC:
68Q55 Semantics in the theory of computing
68N15 Theory of programming languages
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Rees, Fourth Report on the Algorithmic Language Scheme (1988)
[2] DOI: 10.1145/321250.321253 · Zbl 0139.12303 · doi:10.1145/321250.321253
[3] DOI: 10.1007/BF01409744 · doi:10.1007/BF01409744
[4] Harrison, Lisp and Symbolic Computation, an Internal J. 2 (1989)
[5] Gordon, Lecture Notes in Computer Science 78 (1979)
[6] Deutsch, Proc. ACM Conference on Principles of Programming Languages (1990)
[7] Cousot, Proc. ACM Conference on Principles of Programming Languages (1977)
[8] Appel, Standard ML Reference Manual (Preliminary) (1990)
[9] Mitchell, Proc. ACM Conference on Principles of Programming Languages (1988)
[10] DOI: 10.1016/0022-0000(78)90014-4 · Zbl 0388.68003 · doi:10.1016/0022-0000(78)90014-4
[11] Leroy, Proc. ACM Conference on Principles of Programming Languages (1991)
[12] Larus, Proc. ACM Conference on Programming Language Design and Implementation (1988)
[13] Jouvelot, Proc. ACM Conference on Principles of Programming Languages (1991)
[14] Hughes, Proc. Workshop on Partial Evaluation and Mixed Computation (1987)
[15] Hudak, Proc. ACM Conference on Programming Language Design and Implementation (1986)
[16] Hillis, The Connection Machine (1985)
[17] Sheldon, Proc. ACM Conference on Lisp and Functional Programming (1990)
[18] DOI: 10.1145/322123.322135 · Zbl 0395.68031 · doi:10.1145/322123.322135
[19] Plotkin, Technical report DAIMI-FN-19 (1981)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.