×

A type system for bounded space and functional in-place update. (Extended abstract). (English) Zbl 0964.68027

Smolka, Gerd (ed.), Programming languages and systems. 9th European symposium on programming, ESOP 2000. Held as part of the joint European conferences on theory and practice of software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1782, 165-179 (2000).
Summary: We show how linear typing can be used to obtain functional programs which modify heap-allocated data structures in place. We present this both as a “design pattern” for writing C-code in a functional style and as a compilation process from linearly typed first-order functional programs into malloc ()-free C code.
The main technical result is the correctness of this compilation. The crucial innovation over previous linear typing schemes consists of the introduction of a resource type \(\diamondsuit\) which controls the number of constructor symbols such as cons in recursive definitions and ensures linear space while restricting expressive power surprisingly little.
While the space efficiency brought about by the new typing scheme and the compilation into C can also be realized by with state-of-the-art optimizing compilers for functional languages such as OCAML, the present method provides guaranteed bounds on heap space which will be of use for applications such as languages for embedded systems or ‘proof carrying code’.
For the entire collection see [Zbl 0935.00050].

MSC:

68N20 Theory of compilers and interpreters
68N18 Functional programming and lambda calculus

Software:

OCaml
PDFBibTeX XMLCite