Univiversity of Darmstadt
Martin Hofmann has finished his Habilitation Thesis where he constructed a
functional programming language all whose first order programs exhibit
polynomial run time behaviour. For this purpose he has developed a language
based on the predicative recursion scheme of Bellantoni and Cook together
with linearity constraints ensuring polynomial run time even when using
a higher type version of Bellantoni and Cook's predicative recursion scheme.
Using logical relation techniques and realisability methods he has proved
that all function expressible in his language are P-time.
Thomas Streicher has worked on realisability models for computable analysis
where morphisms are all computable but types may contain non-computable
elements. This is useful for ensuring compactness of the unit interval
which fails in case all elements are assumed to be computable. On these
question there has been cooperation with Dana Scott's group in Pittsburgh
who independently have come up with the same suggestion.
In joint work with his PhD student Peter Lietz he has worked on the comparison
of various realisability models for computable analysis. It has turned out
that realisability over Scott's graph model for the untyped lambda calculus
supports the axiom of choice for representations of classical spaces whereas
realisability over the second Kleene algebra (Baire space) supports the
vailidity of strong continuity principles for classical spaces. This has to
be seen as part of a wider program of an axiomatisation of computable analysis.
Next: University of Durham
Up: Progress Report
Previous: University of Cambridge