Author name cluster

Mads Tofte

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

5 papers

2 author rows

TCS Journal 2001 Journal Article

A constraint-based region inference algorithm

Lars Birkedal
Mads Tofte

Region inference is a type-based technique for determining run time memory management at compile time. It is targeted at a runtime model in which the store consists of a stack of regions and memory management predominantly consists of pushing and popping regions. Region inference has previously been specified by a set of inference rules, which formalize when regions may be allocated and deallocated. We present a constraint-based algorithm which implements the specification. It consists of a constraint-based formulation of region inference and a rewriting algorithm for solving a set of constraints. We prove that the constraint-based formulation of region inference is sound with respect to the region inference rules. Moreover we prove “restricted completeness” of the constraint-based formulation, that is, we define an “implementation-oriented” formulation of region inference and show that every derivation in the implementation-oriented formulation can be obtained by a solution to a corresponding constraint problem. We show that rewriting of a constraint problem always terminates with a solution to the original system.

Details DOI

MFCS Conference 1999 Conference Paper

A Type Discipline for Solving Year 2000 Problems in COBOL Programs

Mads Tofte

Abstract Without comparison, the most pressing problem for the industry of computing is the Year 2000 problem. In this talk we explain what the Year 2000 problem is and show its close connection to type theory. We present a new type discipline which allows users to find and correct Year 2000 problems in COBOL programs. The type discipline is implemented in a tool called AnnoDomini, which is sold as a commercial product for remediation of IBM OS/VS COBOL programs (www. hafnium. com). Although developed specifically for business applications, AnnoDomini borrows heavily from research in programming languages. AnnoDomini is written in Standard ML, it provides users with abstract (year) types, it is implemented using unification-based type inference, it was specified using operational semantics, and the core of its design was guided by formulating and proving theorems. The talk presents the basic ideas of AnnoDomini and ends with a demo.

Details

I&C Journal 1997 Journal Article

Region-Based Memory Management

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 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.

Details DOI

TCS Journal 1991 Journal Article

Co-induction in relational semantics

Robin Milner
Mads Tofte

An application of the mathematical theory of maximum fixed points of monotonic set operators to relational semantics is presented. It is shown how an important proof method which we call co-induction, a variant of Park's (1969) principle of fixpoint induction, can be used to prove the consistency of the static and the dynamic relational semantics of a small functional programming language with recursive functions.

Details DOI

I&C Journal 1990 Journal Article

Type inference for polymorphic references

Mads Tofte

The Hindley/Milner discipline for polymorphic type inference in functional programming languages is not sound if used on functions that can create and update references (pointers). We have found that the reason is a simple technical point concerning the capture of free type variables in store typings. We present a modified type inference system and prove its soundness using operational semantics. It is decidable whether, given an expression e, any type can be inferred for e. If some type can be inferred for e then a principal type can be inferred. Principal types are found using unification. The ideas extend to polymorphic exceptions and have been adopted in the definition of the programming language Standard ML.

Details DOI