John Hughes
ABSTRACT
We present a functional language with a type system such that well typed programs run within stated space-bounds. The language is a strict, first-order variant of ML with constructs for explicit storage management. The type system is a variant of Tofte and Talpin's region inference system to which the notion of sized types, of Hughes, Pareto and Sabry, has been added.
- AVW93.Joe Armstrong, Robert Virding, and Mike Williams, Concurrent programming in erlang, Prentice Hall, 1993. Google Scholar
Digital Library
- HCRP91.N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, The synchronous dataflow programming language Lustre, Proc. IEEE 79 (1991), no. 9, 1305-1320.Google ScholarCross Ref
- HPS96.John Hughes, Lars Pareto, m~d Amr Sabry, Proving the correctness of reactive systems using sized types, POPL '96, Janu;~ry 1996. Google ScholarDigital Library
- Lan64.P.J. Landin, The Mechanical Evaluation of Expressions, Computer Journal ~ (1964), no. 4, 308-320.Google Scholar
- Par98.Laxs Pareto, Sized types, Licentiate thesis, Chalmers University of Technology, 1998, (http: // www. cs. chalmers.se/-~ p aret o/lic, ps).Google Scholar
- Pug92.William Pugh, A practical algorithm for exact array dependence analysis, Communications of the ACM 35 (1992), no. 8, 102-114. Google ScholarDigital Library
- TBE+.Mads Torte, Lars Birkedal, Martin Elsman, Niels Hallenberg, Tommy Hojfeld Olcsen, Peter Sestort, and Peter Bertelsen, Programming wi~h regions in the ML Kit, Tech. Report DIKU-TR- 97/12, University' of Copenhagen.Google Scholar
- TT97.Mads Torte and Jean-Pierre Talpin, Regionbased memory management, Information and Computation 132 (1997), no. 2, 109-176. Google ScholarDigital Library
Index Terms
- Recursion and dynamic data-structures in bounded space: towards embedded ML programming
Recommendations
Recursion and dynamic data-structures in bounded space: towards embedded ML programming
We present a functional language with a type system such that well typed programs run within stated space-bounds. The language is a strict, first-order variant of ML with constructs for explicit storage management. The type system is a variant of Tofte ...
Programming Examples Needing Polymorphic Recursion
Inferring types for polymorphic recursive function definitions (abbreviated to polymorphic recursion) is a recurring topic on the mailing lists of popular typed programming languages. This is despite the fact that type inference for polymorphic ...
Comments