118 research outputs found
Region-Based Memory Management
No full textAbstractThis paper describes a memory management discipline for programs that perform dynamic memory allocation and de-allocation. At runtime, all values are put intoregions. The store consists of a stack of regions. All points of region allocation and de-allocation are inferred automatically, using a type and effect based program analysis. The scheme does not assume the presence of a garbage collector. The scheme was first presented in 1994 (M. Tofte and J.-P. Talpin,in“Proceedings of the 21st ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages,” pp. 188–201); subsequently, it has been tested in The ML Kit with Regions, a region-based, garbage-collection free implementation of the Standard ML Core language, which includes recursive datatypes, higher-order functions and updatable references L. Birkedal, M. Tofte, and M. Vejlstrup, (1996),in“Proceedings of the 23 rd ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages,” pp. 171–183. This paper defines a region-based dynamic semantics for a skeletal programming language extracted from Standard ML. We present the inference system which specifies where regions can be allocated and de-allocated and a detailed proof that the system is sound with respect to a standard semantics. We conclude by giving some advice on how to write programs that run well on a stack of regions, based on practical experience with the ML Kit
Title: Region-Based Memory Management 1
No full textThis paper describes a memory management discipline for programs that perform dynamic memory allocation and de-allocation. At runtime, all values are put into regions. The store consists of a stack of regions. All points of region allocation and deallocation are inferred automatically, using a type and e ect based program analysis. The scheme does not assume the presence of a garbage collector. The scheme was rst presented by Tofte and Talpin (1994) � subsequently, it has been tested in The ML Kit with Regions, a region-based, garbage-collection free implementation of the Standard ML Core language, which includes recursive datatypes, higher-order functions and updatable references (Birkedal et al. 96, Elsman and Hallenberg 95). This paper de nes a region-based dynamic semantics for a skeletal programming language extracted from Standard ML. We present the inference system which speci es where regions can be allocated and de-allocated and a detailed proof that the system is sound with respect to a standard semantics. We conclude by giving some advice on how to write programs that run well on a stack of regions, based on practical experience with the ML Kit. 3
Principal Signatures for Higher-order Program Modules
No full textIn this paper we present a language for programming with higher-order modules.y The language, HML, is based on Standard ML in that it provides structures, signatures and functors. In HML, functors can be declared inside structures and specified inside signatures; this is not possible in Standard ML. We present an operational semantics for the static semantics of HML signature expressions with particular emphasis on the handling of sharing. As a justification for the semantics, we prove a theorem about the existence of principal signatures. This result is closely related to the existence of principal type schemes for functional programming languages with polymorphism. 1 Introduction Working on large programs involves manipulating large program units as well as working on the details of individual units. Such program units are sometimes called modules, especially if the programming language in question allows the programmer to name units and combine them in a controlled fashion. Since ..
Essentials of Standard ML Modules
No full text. The following notes give an overview of Standard ML Modules system. 1 Part 1 gives an introduction to ML Modules aimed at the reader who is familiar with a functional programming language but has little or no experience with ML programming. Part 2 is a half-day practical intended to give the reader an opportunity to modify a small, but non-trivial piece of software using functors, signatures and structures. PART 1 1 Introduction It is now more than ten years ago that David MacQueen made his proposal for ML Modules[Mac84]. At the time, there was very little experience with large scale programming in ML. At the time the Modules were formally defined (1987-1989), there was still a certain amount of guesswork involved, still because of the limited practical experience. Today, hundreds of thousands of lines of ML later, ML programmers have a much clearer picture of what the most important aspects of the Standard ML modules are. In the experience of the author, there are certain featur..
Partial Evaluation of Standard ML (Master's Thesis)
No full textinterpretation versus type inference (second revised version). (This article is believed to be unpublished), 1991. [Rom90] Sergei A. Romanenko. Arity raiser and its use in program specialization. In Neil D. Jones, editor, ESOP '90. 3rd European Symposium on Programming, Copenhagen, Denmark, May 1990. (Lecture Notes in Computer Science, vol. 432), pages 341--360. Springer-Verlag, 1990. [Ses86] Peter Sestoft. The structure of a self-applicable partial evaluator. In H. Ganzinger and Neil D. Jones, editors, Programs as Data Objects, Copenhagen, Denmark, 1985. (Lecture Notes in Computer Science, vol. 217), pages 236-- 256. Springer-Verlag, 1986. [Tof88] Mads Tofte. Operational Semantics and Polymorphic Type Inference. PhD thesis, Edinburgh University, Department of Computer Science, Edinburgh University, Mayfield Rd., EH9 3JZ Edinburgh, May 1988. Available as Technical Report CST-52-88. [Tof90] Mads Tofte. Type inference for polymorphic references. Information and Compution, 89(1):1--34, No..
Implementation of the typed call-by-value λ-calculus using a stack of regions
No full textWe present a translation scheme for the polymorphically typed call-by-value λ-calculus. All runtime values, including function closures, are put into regions. The store consists of a stack of regions. Region inference and effect inference are used to infer where regions can be allocated and de-allocated. Recursive functions are handled using a limited form of polymorphic recursion. The translation is proved correct with respect to a store semantics, which models a regionbased run-time system. Experimental results suggest that regions tend to be small, that region allocation is frequent and that overall memory demands are usually modest, even without garbage collection.
- …
