Isaac Newton Institute for Mathematical Sciences

Semantics of Computation

1 July - 31 December 1995

Organisers: S Abramsky (Imperial College, London), G Kahn (INRIA, Sophia-Antipolis), J C Mitchell (Stanford), A M Pitts (Cambridge)

Semantics of Computation Seminar

Friday 13 October, 2.15pm

Expressing Computational Complexity in Type Theory

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.

Copyright © Isaac Newton Institute