[Prev][Next][Index][Thread]
Linear types and malloc()-free C
Dear all,
I would like to draw your attention to the following preprint
available under http://www.dcs.ed.ac.uk/home/mxh/malloc.ps.gz
Comments and suggestions are very welcome!
Best wishes, Martin
In place update with linear types or how to compile functional
programs into malloc()-free C.
by Martin Hofmann
We show how linear typing can be used to write C-functions which
modify their heap allocated arguments in a functional way without
explicit ``pointer surgery.'' We present this both as a ``design
pattern'' for writing C-code in a functional style and as a
compilation process from linearly typed first-order functional
programs into malloc()-free C code. The main technical result is the
correctness of this compilation. We discuss various extensions, in
particular an extension with FIFO queues admitting constant time
catenation and enqueuing, and an extension of the type system to
fully-fledged intuitionistic linear logic. While preliminary
comparisons with optimising ML compilers are promising we believe that
the main possible application lies in areas where code should be
equipped with a guarantee that it runs in linearly bounded
space. Embedded systems or active networking might be examples.