University of Birmingham > Talks@bham > Theoretical computer science seminar > Forcing, effects and continuity

## Forcing, effects and continuityAdd to your list(s) Download to your calendar using vCal - Martin Escardo, University of Birmingham
- Friday 03 August 2012, 16:00-17:00
- CS 217.
If you have a question about this talk, please contact Paul Levy. A natural model of GĂ¶del’s system T (simply typed lambda calculus with natural numbers and primitive recursion) is the full type hierarchy. The type of natural numbers is interpreted as the set N of natural numbers, function types are interpreted as sets of all functions. Every T-definable function f:(N->N)->N is continuous. Moreover, from any T-definition of f, one can algorithmically extract a T-definable function m:(N->N)->N such that the value of f at a sequence x:N->N depends only on the first m(x) positions of x. Such a function m is a so-called modulus of continuity of f. One way of proving this is to use constructive “forcing” with a “generic” sequence N->N. I will develop this from the point of view of denotational semantics. With a Moggi-style semantics of system T for a suitable “dialogue” monad, the generic sequence amounts to a so-called generic effect. A logical relation between the “intended” set-theoretical model and the auxiliary monadic model gives the continuity result. I also implemented the construction and short proof in Agda. This talk is part of the Theoretical computer science seminar series. ## This talk is included in these lists:- CS 217
- Computer Science Departmental Series
- Computer Science Distinguished Seminars
- Theoretical computer science seminar
- computer sience
Note that ex-directory lists are not shown. |
## Other listsSeminars on Advanced Materials School of Mathematics Events Computer Science Lunch Time Talk Series## Other talksTBC |