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