1 July - 31 December 1995
Organisers: S Abramsky (Imperial College, London), G Kahn (INRIA, Sophia-Antipolis), J C Mitchell (Stanford), A M Pitts (Cambridge)
Friday 13 October, 2.15pm
R. Constable (Cornell)
The talk will explore the very simple idea that when we define classes of functions inductively in type theory, we gain access to codes for the functions that allow us to define computational complexity measures. Moreover there is an elegant way to directly define the Cook & Bellantoni definition of PTIME. From this simple observation we can see an elegant way to define resourse bounded logics in type theory.