[logic-ml] Talk by Kazushige Terui, next Thursday

[Ichiro Hasuo]

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.