Contributions offered by Martin Hofmann for topic
H (semantics-based optimisation)

I have developed a typed lambda calculus with inductive datatypes 
in which all definable first-order functions are polynomial time 
computable. 

The proof of this goes by interpretation in a certain model
based on presheaves and realisability.

I hope that from the proof one can extract a "semantics-based 
compiler" or "partial evaluator" which would yield more efficient 
code for programs typable in the system. 

At the workshop I will present the setting and discuss some of the 
problems involved.

--------------------------------------------------------------
Result of feedback form submitted by
Hofmann (mxh@dcs.ed.ac.uk) on Friday, July 3, 1998 at 18:04:5