LFCS Theory Seminar
Room 2511, JCMB, King's Buildings
4pm, Tuesday 29th October 1996

Title: Normalization and the Yoneda Embedding

Speaker: Djordje Cubric (DPMMS, Cambridge)

Abstract: We show how to solve the word problem for simply typed \lambda\beta\eta-calculus by using a few well-known facts about categories of presheaves and the Yoneda embedding. The formal setting for these results is P-category theory, a version of ordinary category theory where each hom-set is equipped with a partial equivalence relation. The part of P-category theory we develop here is constructive and thus permits extraction of programs.

(Joint work with Peter Dybjer, and Philip Scott)