Publications of Henning Makholm

Polymorphic types for mobility calculi

The topic and main product of this research is the retargetable type system Poly* for mobility calculi. Retargetability means that the type system works for a wide range of concrete calculi; given the reduction rules for a particular calculi, a type system for it is automatically produced.

An implementation of type inference for Poly* is available here.

J. B. Wells Instant Polymorphic Type Systems for Mobile Process Calculi: Just Add Reduction Rules and Close

In Schmuel Sagiv (ed.), Programming Languages and Systems (14th European Symposium on Programming, ESOP 2005, April 4-8, 2005, Edinburgh, Scotland), volume 3444 of Lecture Notes in Computer Science, pages 389-407. Springer-Verlag. Final version as PDF. Presentation slides as PDF.

Long version: Technical Report HW-MACS-TR-0022, Heriot-Watt University, School of Mathematical & Computing Sciences, November 2004. Download page.

This is the most up-to-date technical report describing Poly*.

Torben Amtoft & J. B. Wells PolyA: True Type Polymorphism for Mobile Ambients

In Exploring New Frontiers of Theoretical Informatics 3rd IFIP International Conference on Theoretical Computer Science, TCS 2004, August 24-26 2004, Toulouse, France), pages 591-504. Kluwer Academic Publishers. PDF.

A conference paper describing PolyA, the predecessor of Poly*. PolyA worked for Mobile Ambients only.

Long version: Technical Report HW-MACS-TR-0015, Heriot-Watt University, School of Mathematical & Computing Sciences, February 2004. Download page.

The appendices of this report contain proofs that are more detailed than what we have written down explicitly for Poly* so far.

J. B. Wells Type Inference for PolyA

Technical Report HW-MACS-TR-0013, Heriot-Watt University, School of Mathematical & Computing Sciences, January 2004. Download page.

Our first shot at doing type inference for PolyA/Poly*. This is somewhat obsolete by now, but still a bit more detailed regarding some internal issues than the Poly* technical report.

Type systems for mixin modules and record concatenation

J. B. Wells Type Inference, Principal Typings, and Let-Polymorphism for First-Class Mixin Modules

To appear at ICFP 2005. Final version as PDF. Talk slides as PDF.

Region inference and region type systems

Fritz Henglein & Henning Niss Effect Types and Region-Based Memory Management

Invited survey chapter. In B.C. Pierce (ed.), Advanced Topics in Types And Programming Languages, pages 87-136. MIT Press, 2005. ISBN 0-262-16228-8.

Ph.D. thesis A language-independent framework for region inference

Thesis submitted to the University of Copenhagen in August 2003; defended in November 2003. PDF.

Fritz Henglein & Henning Niss A direct approach to control-flow sensitive region-based memory management

In Principles and Practice of Declarative Programming (3rd International ACM SIGPLAN Conference, PPDP '01, 5-7 September 2001, Firenze, Italy), pages 175-186. ACM Press. Gzipped PostScript.

The accompanying implementation can be downloaded.

Region-based memory management and logic programming

Kostis Sagonas On Enabling the WAM with Region Support

In P.J. Stuckey (ed.), Logic Programming (18th International Conference, ICLP '02, July 29-August 1 2002, Copenhagen, Denmark), volume 2401 of Lecture Notes in Computer Science, pages 163-178. Springer-Verlag. Gzipped PostScript.

A region-based memory manager for Prolog

In A. Hosking (ed.), International Symposium on Memory Management (ISMM '00, 15-16 October 2000, Minneapolis, MN, USA), special issue of ACM SIGPLAN Notices, 36(3):25-34. ACM Press. Gzipped PostScript.

Presents selected aspects of the M.Sc. thesis below. A preliminary version appeared at the CL2000 workshop on Memory Management in Logic Programming Implementations.

M.Sc. thesis Region-Based Memory Management in Prolog

Thesis defended at the University of Copenhagen in March 2000. Gzipped PostScript.

The accompanying implementation can be downloaded.

Jones-optimal partial evaluation

Walid Taha & John Hughes Tag elimination and Jones-optimality.

In O. Danvy and A. Filinski (ed.), Programs as Data Objects (Second Symposium, PADO-II, 21-23 May 2001, Aarhus, Denmark), volume 2053 of Lecture Notes in Computer Science, pages 257-275. Springer-Verlag. Dvi.

On Jones-optimal specialization for strongly typed languages

In W. Taha (ed.), Semantics, Applications and Implementation of Program Generation (International Workshop, SAIG '00, 20 September 2000, Montréal, Canada), volume 1924 of Lecture Notes in Computer Science, pages 129-148. Springer-Verlag. Gzipped PostScript

This is the Jones-optimality paper I'm most proud of myself. It presents a prototype specializer MiXIMUM which can do optimal specialization for a strongly-typed toy language. The prototype can be downloaded here.

Walid Taha Tag elimination; or, Type specialization is a type-indexed effect.

In Subtyping & Dependent Types in Programming, (APPSEM Workshop, DTP'00, 7 July 2000, Ponte de Lima, Portugal), INRIA technical report. PostScript.

MiXIMUM - a simpler and more liberal type specializer

Technical report. Gzipped PostScript

This is a rather sketchy report which goes into greater details about how MiXIMUM works, but not quite up-to-date with the actual implementation.

Other work related to partial evaluation

Specializing C - an introduction to the principles behind C-Mix

Student project. Gzipped PostScript.

This project introduces the "hand-written cogen" approach to partial evaluation and the binding-time analysis in C-Mix.

Arne J. Glenstrup & Jens Peter Secher C-MIX: Specialization of C Programs.

In J. Hatcliff et al. (eds.), Partial Evaluation (DIKU International Summer School, 29 June-10 July 1998, Copenhagen, Denmark), volume 1706 of Lecture Notes in Computer Science, pages 108-154. Springer-Verlag.

henning@makholm.net Front page > publications