Title: Region-Based Memory Management 1 (2008)
Mads Tofte, Jean-pierre Talpin
This 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...
entitled Tips for Danes on Punctuation in (2008)
This document and all examples in it are available from
AnnoDomini in Practice: A Type-Theoretic Approach to the Year 2000 Problem (2007)
Peter Harry Eidorff, Fritz Henglein, Christian Mossin, Peter Harry, Eidorff Fritz, Henglein Christian Mossin, ...
. AnnoDomini is a commercially available source-to-source conversion tool for finding and fixing Year 2000 problems in COBOL programs. AnnoDomini uses type-based specification, analysis, and...
Tips for Computer Scientists (2007)
Standard Ml Mads, Mads Tofte, In English, John Dienhart
Contents 1 Numbers 1 2 Overloaded Arithmetic Operators 1 3 Strings 1 4 Lists 1 5 Expressions 1 6 Declarations 1 7 Function Values 3 8 Constructed Values 3 9 Patterns 4 10 Pattern Matching 5 11...
Tips for Computer Scientists (2007)
Standard Ml, Mads Tofte, In English, John Dienhart
Contents 1 Numbers 1 2 Overloaded Arithmetic Operators 1 3 Strings 1 4 Lists 1 5 Expressions 1 6 Declarations 1 7 Function Values 3 8 Constructed Values 3 9 Patterns 4 10 Pattern Matching 5 11...
Tips for Computer Scientists (2007)
Standard Ml, Mads Tofte, In English, John Dienhart
Contents 1 Numbers 1 2 Overloaded Arithmetic Operators 1 3 Strings 1 4 Lists 1 5 Expressions 1 6 Declarations 1 7 Function Values 3 8 Constructed Values 3 9 Patterns 4 10 Pattern Matching 5 11...
Abstract Principal Signatures for Higher-order (2007)
Under the Damas-Milner type discipline for functional languages, every expression has a principal type, if it elaborates at all. In the type discipline for ML Modules, a signature expression has a...
Niels Hallenberg, Martin Elsman, Mads Tofte
This paper describes a memory discipline that combines region-based memory management and copying garbage collection by extending Cheney's copying garbage collection algorithm to work with...
Title: Region-Based Memory Management 1 (2007)
Mads Tofte, Jean-pierre Talpin
This 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...
2 Values and their Representation (2007)
Mads Tofte, Lars Birkedal, Martin Elsman, Niels Hallenberg, Olesen Peter Sestoft
integer 32 bits, untagged. Unboxed (i.e., not region allocated). One bit is used for tagging when GC is enabled. real 64 bits, untagged. Boxed (i.e., allocated in region) string Unbounded size....
Civil Status Married to Joan Campbell-Tofte. Exams and Degrees (2007)
Curriculum Vitae, Mads Tofte, Kostskole Holbæk
University of Copenhagen (Stipend spent on Ph.D. studies in Edinburgh under the supervision of Professor Robin Milner.) Prizes Won
the Principles of Programming Lnguages (POPL 99), 1999. (2007)
Order Mads Tofte, M. Tofte, L. Birkedal, M. Elsman, Mads Tofte, Gordon Plotkin, ...
Publications and notes in chronological
Programming with Regions in the MLKit Revised for version 4.3.0 (2006)
Mads Tofte, Lars Birkedal, Martin Elsman, Niels Hallenberg, Tommy Højfeld, Olesen Peter Sestoft
Values and their Representation integer 32 bits, untagged. Unboxed (i.e., not region allocated). One bit is used for tagging when GC is enabled. real 64 bits, untagged. Boxed (i.e., allocated in...
A Retrospective on Region-Based Memory Management (2004)
Mads Tofte, Lars Birkedal, Martin Elsman, Niels Hallenberg
We report on our experience with designing, implementing, proving correct, and evaluating a region-based memory management system.
Programming with regions in the ML Kit (for version 4 (2001)
Mads Tofte, Lars Birkedal, Martin Elsman, Niels Hallenberg, Tommy Højfeld, Olesen Peter Sestoft
Values and their Representation integer 32 bits, untagged. Unboxed (i.e., not region allocated). One bit is used for tagging when GC is enabled. real 64 bits, untagged. Boxed (i.e., allocated in...
Programming with regions in the ML Kit (for version 4 (2001)
Mads Tofte, Lars Birkedal, Martin Elsman, Niels Hallenberg, Tommy Højfeld, Olesen Peter Sestoft
Values and their Representation integer 32 bits, untagged. Unboxed (i.e., not region allocated). One bit is used for tagging when GC is enabled. real 64 bits, untagged. Boxed (i.e., allocated in...
A constraint-based region inference algorithm (1999)
Region inference is a type-based technique for determining runtime memory management at compile time. It is targeted at a runtime model in which the store consists of a stack of regions and memory...
AnnoDomini: From Type Theory to Year 2000 Conversion Tool (1999)
Peter Harry Eidorff, Fritz Henglein, Christian Mossin, Peter Harry, Eidorff Fritz, Mads Tofte, ...
AnnoDomini is a source-to-source conversion tool for making COBOL programs Year 2000 compliant. It is technically and conceptually built upon type-theoretic techniques and methods: type-based...
A Region Inference Algorithm (1998)
This article presents an algorithm which implements the specification. We prove that the algorithm is sound with respect to the region inference rules and that it always terminates even though the...
Programming with Regions in the ML Kit (1998)
Mads Tofte, Sortbytime Option, Source File
Machine Kit Abstract Machine, 33, 185 kit.script, 185 kitdemo directory, 37 Lambda, 34, 41, 183 lambda abstraction, 125, 126 Lambda optimiser, 35 L A T E X document including figure in, 28 Layout,...
Consider the following region inference rules: Region-based translation of expressions TE ` e) e 0: � ' TE ` c) c at:(int �) � fput ()g TE ` e1) e 0 1:(int � 1)�'1 TE ` e2) e 0 TE...
Programming with Regions in the ML Kit (1997)
Mads Tofte, Stack Profile, Stat Option
Machine Kit Abstract Machine, 29, 167 kit architecture, 168 kitdemo directory, 42 Lambda, 30, 35, 165 lambda abstraction, 117, 118 Lambda optimiser, 30 Layout, 167 leaving the Kit, 163 length of...
From region inference to von Neumann machines via region representation inference (1996)
Lars Birkedal, Mads Tofte, Magnus Vejlstrup, Nkt Elektronik
Region Inference is a technique for implementing programming languages that are based on typed call-by-value lambda calculus, such as Standard ML. The mathematical runtime model of region inference...
Essentials of Standard ML Modules (1996)
. 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...
From Region Inference to von Neumann Machines via Region Representation Inference (1996)
Lars Birkedal Carnegie, Lars Birkedal, Mads Tofte, Magnus Vejlstrup, Nkt Elektronik
Region Inference is a technique for implementing programming languages that are based on typed call-by-value lambda calculus, such as Standard ML. The mathematical runtime model of region inference...
From Region Inference to von Neumann Machines via Region Representation Inference (1996)
Lars Birkedal, Mads Tofte, Magnus Vejlstrup, Nkt Elektronik
Region Inference is a technique for implementing programming languages that are based on typed call-by-value lambda calculus, such as Standard ML. The mathematical runtime model of region inference...
Unification and Polymorphism in Region Inference (1996)
Region Inference is a technique for inferring lifetimes of values in strict, higher-order programming languages such as Standard ML. The purpose of this paper is to show how ideas from Milner's...
Introduction One of the greatest advances in science in this century has been the realisation that there exists a single kind of molecule, DNA, which all known, living organisms use to store their...
Essentials of Standard ML Modules (1996)
. 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...
Implementation of the typed call-by-value λ-calculus using a stack of regions (1994)
Mads Tofte, Jean-Pierre Talpin
We 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....
Implementation of the typed call-by-value -calculus using a stack of regions (1994)
We 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....
Object-oriented programming and Standard ML (1994)
This paper explores connections between object-oriented programming and Standard ML. In particular we show that F-bounded polymorphism can be expressed using ML's polymorphism and a programming...
A Semantics for Higher-order Functors (1994)
. Standard ML has a module system that allows one to define parametric modules, called functors. Functors are "first-order," meaning that functors themselves cannot be passed as parameters...
Implementation of the typed call-by-value λ-calculus using a stack of regions (1994)
Mads Tofte, Jean-Pierre Talpin
We 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...
Object-Oriented Programming and Standard ML (1994)
This paper explores connections between object-oriented programming and Standard ML. In particular we show that F-bounded polymorphism can be expressed using ML's polymorphism and a programming...
A Semantics for Higher-order Functors (1994)
. Standard ML has a module system that allows one to define parametric modules, called functors. Functors are "first-order," meaning that functors themselves cannot be passed as parameters...
Implementation of the typed call-by-value λ-calculus using a stack of regions (1994)
We 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...
Principal Signatures for Higher-order Program Modules (1993)
In 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...
A Theory of Stack Allocation in Polymorphically Typed Languages (1993)
Mads Tofte, Jean-Pierre Talpin
We present a stack-allocation scheme for the call-by-value lambda calculus typed according to Milner's polymorphic type discipline. All the values a program produces, including function...
Mads Tofte, Lars Birkedal, Nick Rothwell, Mads Tofte
System Sciences, 17:348-375, 1978.
3-540-51471-6
Operational Semantics and Polymorphic Type Inference (1988)
Abstract Three languages with polymorphic type disciplines are discussed, namely the *-calculus with Milner's polymorphic type discipline; a language with imperative features (polymorphic...