University of Birmingham > Talks@bham > Theoretical computer science seminar > Analysing PCF and Kleene computability via sequential procedures

Analysing PCF and Kleene computability via sequential procedures

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Paul Levy.

Sequential procedures (a.k.a. PCF Böhm trees) offer a model for PCF -style nested sequential computation in a higher order setting, closely related to the various game models for PCF , although more amenable to interpretation in a wide range of other models such as the Scott model. The ideas behind sequential procedures go back to early work of Sazonov; they also played an incidental role in work on game semantics for PCF , but it is only more recently that we have begun to exploit their potential as a model in their own right has begun to be exploited.

In this talk, I shall do three things:

(1) Give a direct and somewhat novel construction of the sequential procedure model via an untyped lambda-algebra, emphasizing in particular that a surprising amount of the theory works without any reference to the type structure of PCF .

(2) Show how combinatorial reasoning on sequential procedures can be used to obtain expressivity results about (sublanguages of) PCF . In particular, by identifying a certain submodel of the sequential procedure model, we obtain a new result: no bar recursion operator is definable in System T plus minimization.

(3) Use sequential procedures to shed new light on Kleene (S1-S9) computability in the world of total functionals, again offering semantic characterizations of some natural expressivity distinctions.

This talk is part of the Theoretical computer science seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.