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.