Dear colleagues,
Next Thursday our colleague Kazushige Terui is speaking on his recent work about implicit complexity. You're all welcome; no registration necessary. See you there!
Best regards, Ichiro Hasuo --- RIMS-CS website http://www.kurims.kyoto-u.ac.jp/~cs/
===== Speaker: Kazushige Terui (RIMS, Kyoto U.)
Title: Church => Scott = Ptime: an application of resource sensitive realizability
Date: 11.00 - 12.00, Thu 25 Nov 2010
Place: Room 478, "Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan)" http://www.kyoto-u.ac.jp/en/access/campus/main.htm (Next to our CS Lab) 総合研究2号館 478号室 (CS室のとなりです) http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm
Abstract:
We introduce a variant of linear logic with second order quantifiers and type fixpoints, both restricted to purely linear formulas. The Church encodings of binary words are typed by a standard non-linear type `Church,' while the Scott encodings (purely linear representations of words) are by a linear type `Scott.'
We then give a characterization of polynomial time functions, which is derived from (Leivant and Marion 93): a function is computable in polynomial time if and only if it can be represented by a term of type Church => Scott.
To prove soundness, we employ a resource sensitive realizability technique developed by Hofmann and Dal Lago.
This is a joint work with Alois Brunel.