Dear all,

This coming Friday we have Ugo Dal Lago (Bologna) and Paul-Andre Mellies (Paris VII) visiting us in U Tokyo and making talks. Feel free to join us. See you there!

Best regards, Ichiro Hasuo http://www-mmm.is.s.u-tokyo.ac.jp/?plain=false&lang=en&pos=seminar

------------------------------

Fri 8 November 2013, 10:00-12:00

Paul-Andre Mellies http://www.pps.jussieu.fr/~mellies/ (U. Paris VII),

What a geometry of reasoning would look like?

理学部7号館地下 007教室 Room 007 (underground floor), School of Science Bldg. No. 7

アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html

Access: http://www-mmm.is.s.u-tokyo.ac.jp/

If one proceeds by analogy with mathematical physics, it is natural to inquire

the geometric (rather than simply symbolic) nature of logical reasoning.

In this introductory talk, I will describe how this question may be investigated

starting from a series of recent advances at the converging point of proof theory

and of programming language semantics. In particular, I will explain how

a careful study of linear continuations, the most elementary mechanism

common to proofs and to programs, enables one to evacuate the historical divide

between classical and constructive logic, and reveals the existence

of a logical pulsation which regulates reasoning and whose geometry

is related to well-known structures in mathematical physics.

Ugo Dal Lago http://www.cs.unibo.it/~dallago/ (U. Bologna), Applicative Bisimulation for Probabilistic Lambda-Calculus

理学部7号館地下 007教室 Room 007 (underground floor), School of Science Bldg. No. 7

アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html

Access: http://www-mmm.is.s.u-tokyo.ac.jp/

http://www-mmm.is.s.u-tokyo.ac.jp/

We study bisimulation and context equivalence in a probabilistic lambda-calculus. Firstly, we show a technique for proving congruence of probabilistic applicative bisimilarity. While the technique follows Howe's method, some of the technicalities are quite different, relying on non-trivial "disentangling" properties for sets of real numbers. We then analyze the impact the employed notion of reduction has on full-abstraction, giving somewhat surprising results in the call-by-value case. We finally give another unexpected result about the discriminating power of probabilistic contexts on pure lambda-terms.