Peter Møller Neergaard
Complexity Aspects of Programming Language
Design-From Logspace to Elementary Time via Proofnets and Intersection
Types
PhD thesis, Brandeis University, October 2004
More than being just a tool for expressing algorithms, a
well-designed programming language allows the user to express her
ideas efficiently. The design choices, however, affect the efficiency
of the algorithms written in the languages. It is therefore important
to understand how such choices effect the expressibility of
programming languages. The dissertation approaches this problem from
two different angles.
The dissertation presents what appears to be the first resource
independent characterization of the logspace-computable
functions. This is done in the form of a function
algebra BC-varepsilon that is sound and complete for
logspace. BC-varepsilon provides insights
into restricting recursion that might be useful to provide
compile-time guarantees on resource bounds. Furthermore, by
comparison with work by Bellantoni and Cook, it highlights linearity
as a potential distinction between logspace and
ptime.
The dissertation also formalizes how successful type inference
fundamentally depends on the amnesia of the type system: the
fact that the type system forgets information about the program.
Intersection type systems without idempotency provides
an exact analysis where all information is retained. The dissertation
shows that in such intersection type systems, normalization is
equivalent to type inference in every single case. Time bounds
on type inference and normalization are thus identical and doing
compile-time type inference is useless.
The latter part reveals that expansion variables proposed for
type inference are closely related to the boxes already known from the
linear logic technology of proofnets. This hithertho
unknown connection between the two technologies suggests fruitful
contributions between the two fields. Moreover, it extends and
formalizes a previously known connection between intersection types
and proofnets.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.61
Copyright notice: The documents contained
in these pages are included by the contributing authors as a means to
ensure timely dissemination of scholarly and technical work on a
non-commercial basis. Copyright and all rights therein are maintained
by the authors or by other copyright holders, notwithstanding that
they have offered their works here electronically. It is understood that all persons copying this information will
adhere to the terms and constraints invoked by each author's
copyright. These works
may not be reposted without the explicit permission of the copyright
holder.
If you experience problems downloading any of the files above,
it is most likely because your browser does not handle compressed
files correctly.
In particular, Netscape might save the file in the compressed
gz-format with extension .ps or
.pdf (indicating postscript or PDF, resp.). You can work around this by saving the file,
renaming it to .ps.gz or .pdf.gz, and then
uncrompress it.
