みなさま
今週木曜日に催されるセミナーのご案内をさせていただきます。 どうぞお気軽にお越しください。
照井 --- RIMS-CS website http://www.kurims.kyoto-u.ac.jp/~cs/
===== Speaker: Michele Basaldella (RIMS, Kyoto University)
Title: A gentle introduction to ludics
Date: 11.00 - 12.00, April 21st (Thu)
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: When one is interested in understanding the duality between syntax (proofs) and semantics (models) in logic, a primary obstacle is that proofs are finite and concrete objects, while models are infinite and abstract structures. Since proofs and models are so different by their nature, they hardly interact together. This lack of interaction between the two worlds prevents a deeper analysis of the relations between syntax and semantics.
Ludics is a research program started by Girard aimed to explain various logical and computational phenomena from an interactive point of view. The universe of ludics consists of designs: partial and infinitary proofs in which the logical type-information has been almost erased. In this vast universe, both proofs and models can be homogeneously represented as designs. Moreover, since designs come from proofs, we can make them interact together via normalization (cut-elimination). This induces an orthogonality relation, based on the termination of the computation of the normal form, which allows to reconstruct the logical types, as bi-orthogonality-closed sets of designs.
In this talk we introduce and discuss the basic concepts of ludics and show some completeness results for proofs.
--------------------------------------------------------- Kazushige TERUI Research Institute for Mathematical Sciences, Kyoto University. Kitashirakawa Oiwakecho, Sakyo-ku, Kyoto 606-8502, JAPAN. Phone: +81-75-753-7235 Fax: +81-75-753-7276 terui@kurims.kyoto-u.ac.jp http://www.kurims.kyoto-u.ac.jp/~terui/