# Research Seminars

At Group MMM (aka. Hasuo Lab.), Dept. Computer Science, Univ. Tokyo

Get email notices for coming events! (Ask Ichiro)

Thu 9 February 2016, 16:00–17:00

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (School of Science Bldg. No. 7)

Kenta Cho (Radboud U. Nijmegen), An Effectus-Theoretic Perspective on Probabilistic Programming

Modern probabilistic programming languages have the ability to "condition", which is an essential operation in Bayesian statistics to compute conditional (posterior, updated) probabilities given certain data. Probabilistic programming has attracted increasing attention especially for machine learning applications.

Effectuses have recently been introduced as categorical models for quantum logic and computation, with probabilistic and Boolean as special cases. Based on the concepts of states and predicates in an effectus, we formulate "conditioning" as an operation on states and predicates. It then offers a language and semantics for Bayesian probabilistic reasoning. For example, backward and forward inference can be neatly captured by the combination of conditioning and state/predicate transformers. This works uniformly, not only in the discrete and continuous probabilistic setting, but also in the quantum setting.

We are also developing a Python library implementing the effectus language based on states and predicates. It is currently not meant for large scale computation (eg. machine learning), but is useful for modelling and calculating small probabilistic problems. The talk will include the use / demo of the library.

Wed 21 December 2016, 15:00–16:00

Room 214, School of Science Bldg. No. 7

Marc Bagnol (MMM, U-Tokyo), The Resolution Semiring (a unification-based syntax for GoI)

Geometry of Interaction can be presented using many different tools, including include circuits, automata, operator algebras... one of them is based on the theory unification: the Resolution Semiring. The main feature of this GoI model is its finite, syntactic nature. Notions such as term size, height etc. are available, which simplifies complexity-related investigations.

I will present the basic machinery at work in this structure, then show it provides indeed a traced category, hence allowing for GoI constructions. I will also discuss some complexity results one can obtain within this framework.

Wed 30 November 2016, 15:00–18:00

Room 102, School of Science Bldg. No. 7

Sasinee Pruekprasert (Osaka U.), A game theoretical approach to supervisory control of non-terminating discrete event systems

Discrete event system (DES) is a dynamic discrete-state event-driven system where the state changes are triggered by the occurrence of events. A DES spontaneously and asynchronously generates events which are partitioned into controllable and uncontrollable ones. A supervisor is a controller that and controls the DES by disabling or enabling any of the controllable events based on the observed generated sequences. We consider the optimal control of quantitative non-terminating DESs modeled by finite weighted automata, whose behaviors are represented by the generated infinite sequences. An optimal supervisor is a supervisor that satisfies two objectives: 1) to avoid system halts and 2) to maximize the control performance, which is evaluated by the worst-case limit-average weight of the infinite sequences generated by the supervised DES. We propose a game theoretical design method for an optimal supervisor using a two-player turn-based mean-payoff game automaton. As the ﬁrst player, the objective of the supervisor is to maximize the worst-case limit-average weight of the generated sequences; as the second player, the DES aims to minimize it. We can decide the existence of an optimal supervisor using an optimal strategy of the two-player game, and compute it if it exists.

Yoshihiro Kumazawa (MMM, U. Tokyo), A method of MITL specification debugging

Wed 16 November 2016, 15:00–18:00

Room 102, School of Science Bldg. No. 7

Hand written notes : https://honokaa.is.s.u-tokyo.ac.jp/svn/trunk/MMM/oyabu/16111604.PDF

Satoshi Kura (MMM, U. Tokyo), Extending Expected Runtime Transformer

http://dl.acm.org/citation.cfm?doid=2933575.2935317

Ibuki Okamoto (MMM, U. Tokyo), Winning cores

https://arxiv.org/abs/1602.01963

Wed 9 November 2016, 15:00–18:00

Room 102, School of Science Bldg. No. 7

Takamasa Okudono (MMM, U. Tokyo), TBA

https://sway.com/nAriTIM83KDOu7K4 (pw: 10MangokuManjuu)

https://www-mmm.is.s.u-tokyo.ac.jp/~tokudono/qe/calc.jpg

Masaki Waga (MMM, U. Tokyo), Simulation of Two-Way Pushdown Automata Revisited

https://arxiv.org/pdf/1309.5142.pdf

Ichiro Hasuo (MMM, U. Tokyo), Metamathematics for Systems Design: an ERATO Project Overview

（ごめん，最後に回してもらったほうがよいかも）

Wed 2 November 2016, 15:00–18:00

Room 102, School of Science Bldg. No. 7

Shunsuke Shimizu (MMM, U. Tokyo), Parity Automata for Quantitative Linear Time Logics

http://www-mmm.is.s.u-tokyo.ac.jp/~shunsuke/seminar/161102.pdf

http://www-mmm.is.s.u-tokyo.ac.jp/~shunsuke/seminar/fossacs2017.pdf

Ryo Tanaka (MMM, U. Tokyo), Encoding Pi-calculus into Concurrent Interaction Nets

Takumi Akazaki (MMM, U. Tokyo), WIP: Falsification with Bayesian Network Annotations

Handwritten note: FalsificationWithBN 20161101_ _ Evernote Web.pdf

Wed 26 October 2016, 15:00–18:00

Room 102, School of Science Bldg. No. 7

Soichiro Fujii (MMM, U. Tokyo), Generalized Global States and Its Operational Semantics (work in progress)

Handwritten notes: https://dl.dropboxusercontent.com/u/60634646/Fujii_161026.pdf

Toshiki Kataoka (MMM, U. Tokyo), The free cocompletion and three definitions of colimits

For a small category, its free cocompletion is the presheaf category.  Part I: for small categories.  Part II: for locally small categories.

Natsuki Urabe (MMM, U. Tokyo), Categorical Liveness Checking by Corecursieve Algebra

I give a categorical generalization of ranking function and ranking supermartingale.

Slides:

Wed 19 Oct 2016, 15:00–18:00

Room 102, School of Science Bldg. No. 7

Hiroki Kobayashi (MMM, U. Tokyo), An introduction to call-by-push-value calculus

Slides are available on:

Mainly depends on:

A tutorial on call-by-push-value, Levy (slide, 2016) https://www.cs.bham.ac.uk/~pbl/papers/cbpvefftt.pdf

Masaki Hara (MMM, U. Tokyo), Representation of non-distributive lattices

Using Birkhoff’s representation theorem, one can construct a Kripke model from a heyting algebra model of intuitionistic logic. This is convenient for refutation of propositional formulas, because Kripke models are more friendly with SAT (satisfiability) solvers. Similar representation theorem for non-distributive lattices would be useful for substructural logics like linear logic. This can be achieved by introducing two different accessibility relations to Kripke frames.

Based on: Gerard Allwein and J. Michael Dunn, Kripke Models for Linear Logic. The Journal of Symbolic Logic

Vol. 58, No. 2 (Jun., 1993), pp. 514-545. https://www.jstor.org/stable/2275217

Wataru Hino (MMM, U. Tokyo), Varieties of metric and quantitative algebras

References

• R. Mardare, P. Panangaden, and G. Plotkin. Quantitative algebraic reasoning. LICS 2016, pp 700 – 709.
• V. A. Khudyakov. Quasivarieties of metric algebras. Algebra and Logic, 42(6):419–427, 2003.
• N. Weaver. Quasi-varieties of metric algebras. Algebra universalis, 33(1):1–9, 1995.

Tue 2 Aug 2016, 13:00–15:00

Room 102, School of Science Bldg. No. 7

Akira Yoshimizu (MMM, U. Tokyo), TBA

TBA

Wataru Hino (MMM, U. Tokyo), Varieties of Quantitative Algebras

References:

R Mardare, P Panangaden, G Plotkin, Quantitative Algebraic Reasoning

Stephen L. Bloom, Varieties of ordered algebras

Tue 26 July 2016, 13:00–15:00

Room 102, School of Science Bldg. No. 7

Takamasa Okudono (MMM, U. Tokyo), TBA

TBA

https://sway.com/i0pbtUolBp6RcPI3

https://people.mpi-inf.mpg.de/~sofronie/papers/pdf/rybalchenko-sofronie-vmcai07.pdf

http://www.cs.princeton.edu/~zkincaid/pub/ijcai16.pdf

Ryo Tanaka (MMM, U. Tokyo), Token Machines for Multiport Interaction Combinators

TBA

Toshiki Kataoka (MMM, U. Tokyo), Tripos

[Pitts 1981][Pitts 1999]

Tue 19 July 2016, 13:00–15:00

Room 102, School of Science Bldg. No. 7

Liang-Ting Chen (Dept. of Info. and Comp. Sci., University of Hawaii), Schutzenberger Products in a Category

The Sch\"utzenberger product of monoids is a key tool for the algebraic treatment of language concatenation. In this paper we generalize the Sch\"utzenberger product to the level of monoids in an algebraic category 𝒟, leading to a uniform view of the corresponding constructions for monoids (Sch\"utzenberger), ordered monoids (Pin), idempotent semirings (Kl\'ima and Pol\'ak) and algebras over a field (Reutenauer). In addition, assuming that 𝒟 is part of a Stone-type duality, we derive a characterization of the languages recognized by Sch\"utzenberger products.

Tue 12 July 2016, 13:00–15:00

Room 102, School of Science Bldg. No. 7

Masaki Waga (MMM, U. Tokyo), TBA

TBA

Shunsuke Shimizu (MMM, U. Tokyo), TBA

TBA

Takamasa Okudono (MMM, U. Tokyo), TBA

TBA

Tue 28 June 2016, 13:00–15:00

Room 102, School of Science Bldg. No. 7

Akira Yoshimizu (MMM, U. Tokyo), TBA

TBA

Ryo Tanaka (MMM, U. Tokyo), Differential Linear Logic and Resource Calculus

Soichiro Fuji (MMM, U. Tokyo), Theories and dense functors

Handwritten note: https://dl.dropboxusercontent.com/u/60634646/Fujii_160628.pdf

Tue 14 June 2016, 13:00–15:00

Room 102, School of Science Bldg. No. 7

Tetsuya Sato (RIMS, Kyoto University), 差分プライバシーの圏論的特徴づけと、その検証

Bartheによる Approximate Relational Hoare Logic (apRHL) [Barthe et al., POPL 2012]は、クエリーの差分プライバシーを形式的に検証するための枠組みで、差分プライバシーの概念を、圏Set上の確率分布モナドのパラメトリックな二項関係持ち上げによって与えるというアイデアに基づいて構成されている。

Ichiro Hasuo (MMM, U. Tokyo), Coalgebras and Higher-Order Computation: a GoI Approach

(An FSCD invited talk rehearsal, one hour)

Girard's geometry of interaction (GoI) can be seen as a compositional compilation method from functional programs to sequential machines, where tokens move around and express interactions between (parts of) programs. Intrigued by the combination of abstract theory and concrete dynamics in GoI, our line of work (with Naohiko Hoshino, Koko Muroya and Toshiki Kataoka) has aimed at exploiting, in GoI, results from the theory of coalgebra---a categorical abstraction of state-based transition systems that has found its use principally in concurrency theory. Such reinforced connection between higher-order computation and state-based dynamics is made possible thanks to an elegant categorical axiomatization of GoI by Abramsky, Haghverdi and Scott, where traced monoidal categories are identified to be essential in modeling interaction. In the talk I shall lay out these preliminaries and basic ideas, together with some of our results on: GoI semantics for a quantum programming language; and extension of GoI with algebraic effects.

Tue 7 June 2016, 13:00–15:00

Room 214, School of Science Bldg. No. 7

Takumi Akazaki (MMM., U. Tokyo), Gaussian Process Regression and Optimization

I will give you a brief introduction of Gaussian process regression and optimization algorithm (GP-UCB)

Gaussian Process and Machine Learning [Rasmussen & Williams, MIT press 2006]

http://www.gaussianprocess.org/gpml/chapters/RW.pdf

Gaussian Process Optimization in the Bandit Setting: No Regret and Experimental Design [N. Srinivas et al., ICML ’10]

Natsuki Urabe (MMM., U. Tokyo), TBA

Nir Piterman and Amir Pnueli, Faster Solutions of Rabin and Streett Games

http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=1691238

Notions of progress measure are introduced for Rabin and Streett Games

Hiroki Kobayashi (MMM., U. Tokyo), Induction Fibrationally

Indexed Induction and Coinduction, Fibrationally, Ghani, Johann and Fumex (CALCO 2011)

http://arxiv.org/pdf/1307.3263v3.pdf (31 pages)

Structural Induction and Coinduction in a Fibrational Setting, Hermida and Jacobs (Inf. & Comp., 1998)

My talk will largely depend on [Ghani et al., CALCO 2011].

For detail of fibration, see [Hasuo et al., MFPS 2013](https://www.cs.ru.nl/K.Cho/papers/predcoind.pdf ).

Slides are available on http://www-mmm.is.s.u-tokyo.ac.jp/~hkoba/seminar/InductionFibrationally.pdf .

Tue 31 May 2016, 13:00–15:00

Room 102, School of Science Bldg. No. 7

Takamasa Okudono (MMM., U. Tokyo), TBA

Model checking in the modal µ-calculus and generic solutions, Kalorkoti (2011)

http://www.sciencedirect.com/science/article/pii/S074771711000177X

TBA

Wataru Hino (MMM., U. Tokyo),

TBA

Masaki Hara (MMM., U. Tokyo), Memoryless determinacy and a decision procedure of parity games

Memoryless determinacy is a fundamental property of parity games. I will give a proof of it and present a main application: a decision procedure of finite parity games.

Tue 24 May 2016, 13:00–15:00

Room 214, School of Science Bldg. No. 7

Takamasa Okudono (MMM., U. Tokyo), TBA

Model checking in the modal µ-calculus and generic solutions, Kalorkoti (2011)

http://www.sciencedirect.com/science/article/pii/S074771711000177X

TBA

Toshiki Kataoka (MMM., U. Tokyo), (Classical) Nonstandard Analysis

The ultraproduct construction [Robinson] of models, and the axioms by Nelson.

Wataru Hino (MMM., U. Tokyo), TBA

TBA

Tue 17 May 2016, 13:00–15:00

Room 214, School of Science Bldg. No. 7

Masaki Waga (MMM., U. Tokyo), STORMED Hybrid Systems

Kengo Kido (MMM., U. Tokyo), The Domain of Ellipsoids

Shunsuke Shimizu (MMM., U. Tokyo), TBA

TBA

Tue 10 May 2016, 13:00–15:00

Room 214, School of Science Bldg. No. 7

Kenta Cho (Inst. of Comp. & Info. Sci., Radboud University), Von Neumann algebras from a logical / categorical perspective

Many researches at the Nijmegen group involve von Neumann algebras,

which are now important not only in quantum physics but also in the

context of quantum computation and information. I plan to talk about:

1) basics of von Neumann algebras and quantum theory; 2) von Neumann

algebras in effectus theory (a categorical approach to quantum

computation and logic); 3) von Neumann algebras as a (categorical,

denotational) model of the quantum lambda calculus.

Tue 26 Apr 2016, 13:00–15:00

Room 214, School of Science Bldg. No. 7

Natsuki Urabe (MMM., U. Tokyo), Coalgebraic Infinite Traces of Probabilistic Automata

I show the coincidence between automata-theoretic infinite languages of probabilistic automata and coalgebraic infinite traces of them.

Hiroki Kobayashi (MMM., U. Tokyo) Girard’s paradox

• Pure type system (PTS) については
• A simplification of Girard’s paradox (Hurkens, 1995)
• Easier Girard's paradox in a circular pure type system (PTS) (mathoverflow)

• λZ: Zermelo’s Set Theory as a PTS with 4 Sorts (Miquel, 2004)

https://www.fing.edu.uy/~amiquel/publis/types04.pdf

• LE CALCUL DES CONSTRUCTIONS IMPLICITE : SYNTAXE ET SÉMANTIQUE

(Miquel) (フランス語)

https://www.fing.edu.uy/~amiquel/publis/these.pdf

http://www-mmm.is.s.u-tokyo.ac.jp/~hkoba/seminar/girard.pdf

Replay of FoSSaCS

Tue 19 Apr 2016, 13:00–15:00

Room 214, School of Science Bldg. No. 7

Takumi Akazaki (MMM., U. Tokyo), Toward compositional falsification

TBA

Masaki Hara (MMM., U. Tokyo), SAT/SMT Solvers

I describe briefly SAT/SMT solvers and its application.

References:

Ichiro Hasuo (MMM., U. Tokyo), Research Ideas Showcase

Wed 30 Mar 2016, 16:30–18:00

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

(Part I)

Nayuta Yanagisawa (Dept. Math., Kyoto U.), Topological Theory of Distributed Computing

(Part II)

Nayuta Yanagisawa (Dept. Math., Kyoto U.), A Topological Characterization of Wait-Free Solvability in the Infinite Arrival Model

We extend the topological theory of distributed computing for systems with a fixed set

of n processes to that for systems with infinitely many processes. We investigate

a necessary and sufficient condition for the finitely-valued colorless tasks to be

wait-free solvable in such distributed systems. A finitely-valued colorless task is a task

that assumes a finite set of possible input/output values, and specifies input/output

relation without referring to process IDs. Our characterization only resorts to finite

combinatorial structures, called finite simplicial complexes as the topological device.

By restricting our attention to finitely-valued colorless tasks, we can represent possible

protocol states that are innocent of process IDs by a finite simplicial complex,

even if the number of participating processes is infinite.

Mon 18 Jan 2016, 13:00–15:00

Room 214, School of Science Bldg. No. 7

, TBA

TBA

Mon 21 Dec 2015, 13:00–14:30

Room 214, School of Science Bldg. No. 7

John Power (U. Bath), TBA

TBA

Thu 17 Dec 2015, 13:30–15:00

Room 214, School of Science Bldg. No. 7

John Power (U. Bath), TBA

TBA

Tue 15 Dec 2015, 13:00–14:30

Room 214, School of Science Bldg. No. 7

John Power (U. Bath), TBA

TBA

Mon 14 Dec 2015, 13:00–15:00

Room 214, School of Science Bldg. No. 7

Hiroki Kobayashi (MMM., U. Tokyo), Duality and Healthiness

TBA

Masaki Waga (MMM., U. Tokyo), Timed Pattern Matching with Automaton

TBA

Masaki Hara (MMM., U. Tokyo), Characterization of Parameterized Coinduction and Induction

Parameterized coinduction ( http://dblp.uni-trier.de/rec/html/conf/popl/HurNDV13 ) is a technique for proving liveness conditions in a proof assistant like Coq. We define the dual counterpart and give characterization of their power.

Mon 7 Dec 2015, 13:00–15:00

Room 214, School of Science Bldg. No. 7

Yoshiki Nakamura (Kashima Lab., Tokyo Tech), A Derivative for Concurrent Kleene Algebra with Tests

Peter Jipsen introduced Concurrent Kleene Algebra with Tests(CKAT) In

RAMiCS2014. The Language theoretical model of CKAT is called Guarded

Series-Parallel Language. We give a derivative for CKAT to decide word

problems over Guarded Series-Parallel Language.

Thu 26 Nov 2015, 15:00-16:30 (Joint Seminar w/ Kobayashi Lab.)

Taku Terao (Kobayashi Lab., U. Tokyo), Higher-order Model Checking in Direct Style

TBA (Joint work with Tsukada & Kobayashi)

Shunsuke Shimizu (MMM., U. Tokyo), Automata, Nested Fixed Points, and Coalgebraic Model Checking

TBA

Mon 16 Nov 2015, 13:00–15:00

Room 214, School of Science Bldg. No. 7

Ryo Tanaka (MMM., U. Tokyo), Embedding from “Particle-style” to “Wave-style”

http://www.mscs.dal.ca/~selinger/papers/bainbridge.ps [Selinger, 1998]

Takumi Akazaki (MMM., U. Tokyo), Yoneda lemma & adjoint

TBA

Ryo Hirafuji (MMM., U. Tokyo), Units-of-Measure types

TBA

Mon 9 Nov 2015, 13:00–15:00

Room 214, School of Science Bldg. No. 7

Natsuki Urabe (MMM., U. Tokyo), Coalgebraic simulation for Buechi automata

TBA

Toshiki Kataoka (MMM., U. Tokyo), Lambek extensions of finite groups

Isbell in 1968 showed that there does not exist a finitely complete Lambek extension of the cyclic group Z/4.  Why Z/4?  We will simplify Isbell’s proof and give general result for arbitrary finite groups.

(To appear in extended version of http://arxiv.org/abs/1505.01098)

(The result will be submitted soon, possibly with Dusko.)

Akira Yoshimizu (MMM., U. Tokyo), Interaction nets and its non-deterministic extensions

Interaction net introduced by Lafont is a graph rewriting scheme subsuming multiplicative linear logic proof net. While keeping nice locality of MLL proof net, it is much more expressive; there exists a system that is Turing complete. We will look at the basic definition of interaction net with several examples, a Geometry of Interaction-like semantics of a universal system called interaction combinator, and extension to non-deterministic ones.

Mon 2 Nov 2015, 16:30–18:00

Room 214, School of Science Bldg. No. 7

Bart Jacobs (Radboud U.), Introduction to Effectus Theory

Effectus theory provides a novel categorical approach to models of probabilistic and quantum computation and logic. The talk will introduce the main aspects and examples of effectuses.

http://lmcs-online.org/ojs/viewarticle.php?id=1766&layout=abstract

Mon 26 Oct 2015, 13:00–15:00

Room 214, School of Science Bldg. No. 7

Wataru Hino (MMM., U. Tokyo), ω-regular language and ω-semigroup

http://www.liafa.jussieu.fr/~jep/Resumes/InfiniteWords.html [D. Perrin, J. É. Pin 2004]

Kengo Kido (MMM., U. Tokyo), [Cohen et al., IEEE Trans. on Software Eng. ‘97] [Nadi et al., IESE ‘14]

[Nadi et al, ICSE 14] Mining Configuration Constraints: Static Analyses and Empirical Results

http://dl.acm.org/citation.cfm?id=2568283

Akihiko Tozawa (MMM., U. Tokyo), TBA

TBA

Mon 19 Oct 2015, 13:00–15:00

Room 214, School of Science Bldg. No. 7

Koko Muroya (MMM., U. Tokyo), Memoization in memoryful GoI

TBA

Ichiro Hasuo (MMM., U. Tokyo), State-of-art of coalgebraic trace & simulation

TBA

Shota Nakagawa (MMM., U. Tokyo), Finite automata and monadic second-order logic

TBA

Thu 8 Oct 2015, 16:00-17:30 (Joint Seminar w/ Kobayashi Lab.)

Takumi Akazaki (MMM., U. Tokyo), TBA

TBA

Takeshi Tsukada (Kobayashi Lab., U. Tokyo), Negations in Refinement Intersection Type Systems

TBA

Mon 3 Aug 2015, 16:30-18:00

Room 415, 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/ (see bottom)

Research Topics Showcase

Mon 27 July 2015, 16:00-17:30

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Ichiro Hasuo (MMM., U. Tokyo), TBA

… and then Research Problems Session

Mon 13 July 2015, 16:00-17:30

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Kengo Kido (MMM., U. Tokyo), SNR rehearsal

To appear in SNR 2015.

Takumi Akazaki (MMM., U. Tokyo), CAV rehearsal

To appear in CAV 2015.

Mon 15 June 2015, 16:00-17:30

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Toshiki Kataoka (MMM., U. Tokyo), CALCO rehearsal

To appear in CALCO 2015.

Natsuki Urabe (MMM., U. Tokyo), CALCO rehearsal

Coalgebraic Infinite Traces and Kleisli Simulations

Wataru Hino (MMM., U. Tokyo), CALCO EI rehearsal

TBA

Mon 8 June 2015, 16:00-17:30

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Toshiki Kataoka (MMM., U. Tokyo), Towards concept analysis in categories: limit inferior as algebra, limit superior as coalgebra (part II)

To appear in CALCO 2015.

Kentaro Honda (Hagiya Lab, U. Tokyo), TBA

TBA

Ryo Tanaka (MMM., U. Tokyo), Initial Solutions of Domain Equations

Roberto M. Amadio & Pierre-Louis Curien: Domains and Lambda-Calculi, 7.1

Wed 3 June 2015, 16:30-18:00

アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access:
http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)

Alexandre Rocca (Verimag),

Application of Formal Methods to Biological Systems Modelling

The modelling of complex biological systems as differential equations often results in non-linear, high-dimensional, stiff models with uncertain parameters. The validation of those models with respect to some experimental results is often done with simulations. However, these validations are not guaranteed. Formal verification techniques allow proving properties, with set-based computation techniques, by replacing the simulation runs with a conservative set of trajectories. However, biological models are challenging by their size and complex dynamics: we need automatic, and formal, model reduction methods to reduce the dimension and complexity of biological models. We are currently investigating a  reduction technique based on a separation of the different time-scales, and singular perturbation theory. After reduction, the model is smaller and less stiff and then reachability analysis can be applied more efficiently. In addition, we are working on a reachability tool (based on Bernstein polynomials) for polynomial systems with uncertain parameters, which often arise in biochemical reaction networks.

Mon 1 June 2015, 16:00-17:30

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Shota Nakagawa (MMM., U. Tokyo), TBA

C. Baier, et al., Model-Checking Algorithms for Continuous-Time Markov Chains

Hiroshi Ogawa (MMM., U. Tokyo), Approximation Metrics for Discrete and Continuous Systems (Antoine Girard, George J. Pappas)

IEEE transactions and automatic control 2007

Toshiki Kataoka (MMM., U. Tokyo), Towards concept analysis in categories: limit inferior as algebra, limit superior as coalgebra

To appear in CALCO 2015.

Thu 28 May 2015, 10:45-12:00

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Shunsuke Shimizu (MMM., U. Tokyo), TBA

Parity Progress Measure in Coalgebraic Model Checking

Mon 18 May 2015, 16:00-17:30

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Kenta Cho (Radboud U. Nijmegen), Effectus Theory

An effectus is a category with a final object and finite coproducts

satisfying certain assumptions, which was introduced by Jacobs [1]

(the term "effectus" was later given) for the study of quantum/effect

logic and computation. Effectuses are now actively studied by Jacobs'

group in Nijmegen. Our long-term aim is to define a quantum-analogue

of a topos, which shall be called a "telos".

In this talk, I will give an overview of effectuses, and then recent

developments such as partial computations, quotients and

comprehensions in effectuses.

[1] Bart Jacobs. New Directions in Categorical Logic, for Classical,

Probabilistic and Quantum Logic. http://arxiv.org/abs/1205.3940v3

Mon 11 May 2015, 16:00-17:30

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Takumi Akazaki (MMM., U. Tokyo), Semidefinite Programming for Kengo

Pablo. A. Parrilo: Semidefinite programming relaxations for semialgebraic problems (Math. Program. ‘02)

Natsuki Urabe (MMM., U. Tokyo), TBA

K. Chatterjee, L. Doyen & T. A. Henzinger, Quantitative Languages (TOCL ‘10)

Shunsuke Shimizu (MMM., U. Tokyo), TBA

http://users.dcc.uchile.cl/~gaelle/icalp2010.pdf

Mon 27 Apr 2014, 16:00-17:30

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Kengo Kido (MMM., U. Tokyo), TBA

TBA

Koko Muroya (MMM., U. Tokyo), TBA

D. Ghica: Geometry of Synthesis: a structured approach to VLSI design (POPL ‘07).

Takumi Akazaki (MMM., U. Tokyo), TBA

Pablo. A. Parrilo: Semidefinite programming relaxations for semialgebraic problems (Math. Program. ‘02)

Mon 20 Apr 2014, 16:00-17:30

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Ryo Tanaka (MMM., U. Tokyo), TBA

Coeffects: Unified static analysis of context-dependence (2013)

Akihiko Tozawa (MMM., U. Tokyo), TBA

Bounded Linear Types in a Resource Semiring (ESOP, '14)

Wataru Hino (MMM., U. Tokyo), Observational-induced algebra

We will introduce the notion of observational-induced algebra by Battenfeld et al.

Tue 30 Mar 2014, 15:30-17:00

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Soichiro Fujii (MMM., U. Tokyo), Games as Syntax

We give an overview of the paper “Game semantics in string diagrams” by Paul-Andre Mellies.

Ryo Tanaka (MMM., U. Tokyo), TBA

TBA

Tue 10 Mar 2014, 15:00-16:30

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Hiroshi Ogawa (MMM., U. Tokyo), TBA

TBA

Wataru Hino (MMM., U. Tokyo), TBA

TBA

Koko Muroya (MMM., U. Tokyo), TBA

TBA

Mon 9 Mar 2014, 15:30-17:00

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Ryo Tanaka (MMM., U. Tokyo), TBA

TBA

Shunsuke Shimizu (MMM., U. Tokyo), TBA

TBA

Natsuki Urabe (MMM., U. Tokyo), TBA

TBA

Mon 2 Mar 2014, 15:30-17:00

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Shunsuke Shimizu (MMM., U. Tokyo), TBA

TBA

Ichiro Hasuo (MMM., U. Tokyo), TBA

TBA

Kentaro Honda (Hagiya Lab., U. Tokyo), TBA

TBA

Mon 23 Feb 2014, 16:45-17:30

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Takumi Akazaki (MMM., U. Tokyo), TBA

TBA

Mon 5 Jan 2014, 15:30-17:00

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Kazutaka Matsuda (Kobayashi Lab., Dept. CS, U. Tokyo),

Bidirectional Programming in a More Applicative Style

A bidirectional transformation is a pair of mappings between source

and view data objects, one in each direction. When the view is

modified, the source is updated accordingly with respect to some

laws. One way to reduce the development and maintenance effort of

bidirectional transformations is to have specialized languages in

which the resulting programs are bidirectional by construction---

giving rise to the paradigm of bidirectional programming.

In this talk, we will propose a new bidirectional programming framework

in which we can write and combine bidirectional transformations in

the applicative style, with usual higher-order functions. As a result,

we can program bidirectional transformations almost as easy as usual

unidirectional programming in a usual higher-order language.

Toshiki Kataoka (MMM., U. Tokyo), On Innocent Strategies and Sheaves

TBA

Shota Nakagawa (MMM., U. Tokyo), Safra’s Algorithm

TBA

Mon 22 Dec 2014, 14:00-15:30

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

John Power (U. Bath), Coalgebraic Logic Programming: from Semantics to Implementation; embracing the laxness (joint with Ekaterina Komendantskaya), Part II

Coinductive definitions, such as that of an infinite stream, may often be described by elegant logic programs, but ones for which SLD-refutation is of no value as SLD-derivations fall into infinite loops.  Such definitions give rise to questions of lazy corecursive derivations and parallelism, as execution of such logic programs can have both recursive and corecursive features at once. Observational and coalgebraic semantics have been used to study them abstractly. However, the programming developments have often occurred separately and have usually been implementation-led.

Here, we start to give a coherent semantics-led account of the issues, proceeding from abstract category theoretic semantics and developing coalgebra to try to characterise naturally arising trees. As part of the project but not presented in this talk, the work is proceeding towards implementation of a new dialect, CoALP, of logic programming, characterised by guarded lazy corecursion and parallelism.

Mon 15 Dec 2014, 14:00-15:30

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

John Power (U. Bath), Coalgebraic Logic Programming: from Semantics to Implementation; embracing the laxness (joint with Ekaterina Komendantskaya)

Coinductive definitions, such as that of an infinite stream, may often be described by elegant logic programs, but ones for which SLD-refutation is of no value as SLD-derivations fall into infinite loops.  Such definitions give rise to questions of lazy corecursive derivations and parallelism, as execution of such logic programs can have both recursive and corecursive features at once. Observational and coalgebraic semantics have been used to study them abstractly. However, the programming developments have often occurred separately and have usually been implementation-led.

Here, we start to give a coherent semantics-led account of the issues, proceeding from abstract category theoretic semantics and developing coalgebra to try to characterise naturally arising trees. As part of the project but not presented in this talk, the work is proceeding towards implementation of a new dialect, CoALP, of logic programming, characterised by guarded lazy corecursion and parallelism.

Mon 8 Dec 2014, 15:30-17:00

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Akihiko Tozawa (MMM., U. Tokyo), Map-Reduce

http://dl.acm.org/citation.cfm?id=1989310

http://infolab.stanford.edu/~ullman/pub/join-mr.pdf

Norihiro Tsumagari (MMM., U. Tokyo), On Upper-Expectation Bisimilarity and Lukasiewicz mu-calculus

Hiroshi Ogawa (MMM., U. Tokyo), the characterization of pointwise enrichment in the Kleisli category

Mon 1 Dec 2014, 15:30-17:00

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Kengo Kido (MMM., U. Tokyo), The domain of convex polyhedra (in our nonstandard setting)

Takumi Akazaki (MMM., U. Tokyo), Robustness of temporal logic specifications

[TCS09, Fainekos and Pappas] http://www.public.asu.edu/~gfaineko/pub/tcs09.pdf

[FORMATS10, A. Donze et al.] http://link.springer.com/chapter/10.1007/978-3-642-15297-9_9

Mon 17 Nov 2014, 15:30-17:00

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Wataru Hino (Math Dept., U. Tokyo), Difference between Free Monads and Algebraically Free Monads

Reference: Kelly, G. (1980). A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on. Bulletin of the Australian Mathematical Society, Vol. 22. (esp. pp.63-66)

Koko Muroya (MMM., U. Tokyo), Introduction to Bayesian networks

Chap. 1 from R. Neapolitan (2004), Learning Bayesian networks.

Soichiro Fujii (MMM., U. Tokyo), Completions in Mathematics

TBA

Mon 10 Nov 2014, 15:30-17:00

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Tomohiro Katayama (Imai Lab., U. Tokyo), TBA

TBA

Natsuki Urabe (MMM, U. Tokyo), Kleisli Simulation for Infinite Trace

Ryo Tanaka (MMM., U. Tokyo), TBA

TBA

Tue 28 Oct 2014, 9:00-10:30

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Shunsuke Shimizu (MMM, U. Tokyo), TBA

TBA

Kentaro Honda (Hagiya Lab., U. Tokyo), TBA

TBA

Mon 27 Oct 2014, 15:30-17:00

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Toshiki Kataoka (MMM, U. Tokyo), Introduction to Topos

By examples: presheaves, sheaves over topological spaces.

Mon 20 Oct 2014, 15:30-17:00

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Hiroshi Ogawa (MMM, U. Tokyo), On the Construction of Final Coalgebra.

Akira Yoshimizu (MMM, U. Tokyo), On Multi-Agent Justification Logic

Shota Nakagawa (MMM, U. Tokyo), Visibly Pushdown Automata

Wed 15 Oct 2014, 15:30-17:00

アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access:
http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)

Akihiko Tozawa (MMM, U. Tokyo), Review of Previous Research

TBA

Norihiro Tsumagari (MMM, U. Tokyo), On Multirelations

Ichiro Hasuo (MMM, U. Tokyo), Coinductive Predicates and Final Sequences in a Fibration

Replay of [MFPS, 2013]

Wed 17 Sep 2014, 11:00-12:00

Kengo Kido (MMM, U. Tokyo), Abstract Interpretation (Survey, ctn’d)

アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access:
http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)

TBA

Tue 16 Sep 2014, 11:00-12:00

Kengo Kido (MMM, U. Tokyo), Abstract Interpretation (Survey)

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

TBA

Thu 24 Jul 2014, 12:00-12:30

Shota Nakagawa (MMM, U. Tokyo), TBA

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

TBA

Tue 8 Jul 2014, 12:00-12:30

Koko Muroya (MMM, U. Tokyo), TBA

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

TBA

Mon 23 Jun 2014, 15:30-17:00

Toshiki Kataoka (MMM, U. Tokyo), Topos Theoretical Łoś Theorem

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

TBA

Wed 18 Jun 2014, 16:30-18:00

On a Categorical Framework for Coalgebraic Modal Logic

アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access:
http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)

Two syntax-oriented approaches to coalgebraic modal logic — Moss’ cover modality and Pattinson’s predicate liftings — are successful in producing a wide range of modal logics parametric in a Set functor, including modal logics for Kripke frames, Markov chains, Markov processes, and their variants. Both of them can be presented abstractly in a form similar to mathematical SOS by Turi and Plokin, but this line of research was not well-understood yet.

In this talk I will treat the abstract formation seriously, and introduce a category of abstract semantics parametric in a contravariant functor that assigns to the state space its collection of predicates with propositional connectives. Various classical notions are formulated categorically. For example, modular constructions are identified as colimits, limits, and compositions of one-step semantics. The compositions and the colimits of (one-step) expressiveness semantics remain (one-step) expressive. In addition, we investigate a canonically-defined logic by its fibres, and show that it is a terminal object for every fibre.

By its very formulation, it is straightforward to show above results in this level of generality. In fact, I would like to suggest that it is the right level of abstraction for understanding coalgebraic modal logic. For further details, please see my MFPS paper, available in

http://www.cs.cornell.edu/Conferences/MFPS30/MFPS30-prelim.pdf

Tue 17 Jun 2014, 13:00-14:00

Georgios Fainekos (Arizona State University),

Temporal Logic Testing and Verification for Cyber-Physical Systems

アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access:
http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)

One of the important challenges in the Model Based Development (MBD) of Cyber-Physical Systems (CPS) is the problem of verifying functional system properties. In its general form, the verification problem is undecidable due to the interplay between continuous and discrete system dynamics. In this talk, we present the bounded-time temporal logic testing and verification problem for CPS. Temporal logics can formally capture both state-space and real-time system requirements. For example, temporal logics can mathematically state requirements like "whenever the system switches to first gear, then it should not switch back to second gear within 2.5sec".  Our approach in tackling this challenging problem is to convert the verification problem into an optimization problem through a notion of robustness for temporal logics. The robust interpretation of a temporal logic specification over a CPS trajectory quantifies "how much" the system trajectory satisfies or does not satisfy the specification. In general, the resulting optimization problem is non-convex and non-linear, the utility function is not known is closed-form and the search space is uncountable. Thus, stochastic search techniques are employed in order to solve the resulting optimization problem. We have implemented our testing and verification framework into a Matlab (TM) toolbox called S-TaLiRo (System's TemporAl LogIc Robustness). In this talk, we demonstrate that S-TaLiRo can provide answers to challenge problems from the automotive and medical device industries.

Georgios Fainekos is an Assistant Professor at the School of Computing, Informatics and Decision Systems (SCIDSE) Engineering at Arizona State University (ASU). He is director of the Cyber-Physical Systems Lab and he is currently affiliated with the Center for Embedded Systems at ASU. He received his Ph.D. in Computer and Information Science from the University of Pennsylvania in 2008 where he was affiliated with the GRASP laboratory. He holds a Diploma degree (B.Sc. & M.Sc.) in Mechanical Engineering from the National Technical University of Athens and an M.Sc. degree in Computer and Information Science from the University of Pennsylvania. Before joining ASU he held a Postdoctoral Researcher position at NEC Laboratories America in the System Analysis & Verification Group. He is currently working in the area of Cyber-Physical Systems (CPS) with focus on formal methods, logic, optimization and control theory with applications to automotive systems, autonomous (ground and aerial) robots and human-robot interaction (HRI). In 2014, Dr. Fainekos received the NSF CAREER award. He was recipient of the 2008 Frank Anger Memorial ACM SIGBED/SIGSOFT Student Award, and the 2013 Best Researcher Junior Faculty award from SCIDSE.

Mon 2 Jun 2014, 15:30-17:00

Bart Jacobs (Radboud U. Njimegen), Axiomatising categorical quantum logic

アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access:
http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)

This talk describes several assumptions on a category that together yield a proposal for a categorical structure for quantum logic. The assumptions and consequences describe the differences and similarities between classical, probabilistic, and quantum logic. The leading examples are the category Sets, the Kleisli category of the distribution monad, and the opposite of the category of C*-algebras and (completely) positive unital maps.

Thu 29 May 2014, 16:30-18:00

Georg Struth (U. Sheffield), Build Your Own Program Analysis Tool

アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access:
http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)

We present a principled way of designing program analysis tools within interactive proof assistants such as Coq or Isabelle; inparticular tools for the construction and verification of sequential and concurrent programs. We use algebras of programs to capture the control flow of programs and to derive Hoare-style inference rules, verification conditions, or transformation and refinement laws. We model their data flow by linking these algebras with denotational models of programs, including relations, predicate transformers, or sets of traces and by enriching these with notions of store and state, with data types, assignment and process interference.

This separation of concern makes the approach open, modular and highly automatic. Its implementation in Isabelle/HOL is particularly simple. It yields lightweight tools which are themselves correct by construction and can be combined with various programming languages and integrated into different formal methods.

We illustrate the approach through three examples: a verification tool for while programs based on Kleene algebra with tests, its extension to a Morgan-style program refinement tool, and a prototype for verifying and constructing shared variable concurrent programs based on a new variant of concurrent Kleene algebra. Time permitting, we

will outline how more powerful program analysis tools can be obtained from more expressive algebras.

Thu 22 May 2014, 16:40-18:00

TBA

Thu 22 May 2014, 10:30-12:00

Hiroshi Hirai (Dept. Math. Inform., U. Tokyo),
Median Algebra, Optimization and Concurrency (Tentative)

アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access:
http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)

TBA

Mon 19 May 2014, 13:00-14:30

Norihiro Tsumagari (MMM, U. Tokyo),

Relational models of Kleene algebras along with Non-determinism and Probability

Room 102, 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/ (see bottom)

Kleene algebra is sound and complete for the equational theory of regular expressions. After Kozen introduced the notion of Kleene algebra, various extensions of the algebra were so appeared as to be suitable for each purpose.

Complete idempotent semiring, aka quantale, is an algebraic structure strongly related with Kleene algebra. In this talk, we study on a relaxation of complete idempotent semiring, called a complete IL-semiring which gives up the one side of distributivity of multiplication over the join.

We give some relational models of complete IL-semirings by multirelations and convex-relations. Multirelations are appeared in the study of predicate transformer, game logic, and concurrent propositional dynamic logic. Convex relations is a relational generalisation of a semantic domain of probabilistic systems introduced by McIver et al.

In the first part, we study the relationship of complete IL-semirings and weaker variants of Kleene algebras. In the second part, we study various relational models of complete IL-semirings (or weak Kleene algebras).

Mon 12 May 2014, 15:30-17:00

Shota Nakagawa (MMM, U. Tokyo), Stationary Distributions in Markov Chains and their Applications

アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access:
http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)

On: stationary distributions, their application to reachability probability, and its quantum version

Mon 28 April 2014, 15:30-17:00

Takumi Akazaki (MMM, U. Tokyo), TBA

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

We introduce the following paper:

Mon 31 March 2014, 15:30-17:00

Akira Yoshimizu (MMM, U. Tokyo), ESOP 2014 Talk Rehearsal

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

TBA

Takumi Akazaki (MMM, U. Tokyo), HAS 2014 Talk Rehearsal

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

TBA

Mon 10 March 2014, 16:40-18:10

Corina Cirstea (U. Southampton),
TBA

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

TBA

Mon 3 March 2014, 16:40-18:10

Ichiro Hasuo (MMM, U. Tokyo),
Generic Weakest Precondition Semantics from Monads Enriched with Order

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

We devise a generic framework where a weakest precondition semantics, in the form of indexed posets, is derived from a monad whose Kleisli category is enriched by posets. It is inspired by Jacobs' recent identication of a categorical structure that is common in various predicate transformers, but adds generality in the following aspects: 1) different notions of modality (such as \may" vs. \must") are captured by Eilenberg-Moore algebras; 2) nested branching--like in games and in probabilistic systems with nondeterministic environments--is modularly modeled by a monad on the Eilenberg-Moore category of another.

The work is to appear in Proc. CMCS 2014.

Fri 7 February 2014, 16:30-18:00

Mingsheng Ying (University of Technology Sydney & Tsinghua University)
Reachability Analysis of Quantum Markov Chains

アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access:
http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)

The talk will be based on our Concur'12 and Concur'13 papers, which study verification of quantum systems, including quantum programs, modelled by quantum Markov chains (qMCs). We consider three kinds of long-term behaviour, namely reachability, repeated reachability and persistence, of qMCs. As a stepping-stone, we introduce the notion of bottom strongly connected component (BSCC) of a qMC and develop an algorithm for finding BSCC decompositions of the state space of a qMC. As the major contribution, several (classical) algorithms for computing the reachability, repeated reachability and persistence probabilities of a qMC are presented, and their complexities are analysed.

Mon 6 January 2014, 15:30-17:00

Hiroshi Ogawa (MMM, U. Tokyo), TBA

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

TBA

Akira Yoshimizu (MMM, U. Tokyo), TBA

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

TBA

Mon 16 December 2013, 15:30-17:00

Shota Nakagawa (MMM, U. Tokyo), TBA

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Fairness of DTMCs, and more

Takumi Akazaki (MMM, U. Tokyo), TBA

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

TBA

Mon 9 December 2013, 15:30-17:00

Kengo Kido (MMM, U. Tokyo), TBA

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

TBA

Mon 25 November 2013, 15:30-17:00

Ichiro Hasuo (MMM, U. Tokyo), Intro. to Coalgebraic Trace Semantics (Part I)

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Mon 18 November 2013, 15:30-17:00

Natsuki Urabe (MMM, U. Tokyo), TBA

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

1-hour talk

Naohiko Hoshino (RIMS, Kyoto U.), SK-Algebras from Geometry of Interaction

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

Ichiro Hasuo (MMM, U. Tokyo), Generic Trace Semantics by Coinduction

I’ll use the slides http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/talks/acg2006.pdf and explain generic trace semantics for transition systems by coinduction in a Kleisli category.

Mon 11 November 2013, 15:30-17:00

Soichiro Fujii (Dept. Mathematical Engineering and Information Physics, U. Tokyo), TBA

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

TBA

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

Paul-Andre Mellies (U. Paris VII),

What a geometry of reasoning would look like?

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 (U. Bologna),
Applicative Bisimulation for Probabilistic Lambda-Calculus

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.

Fri 1 November 2013, 10:30-12:00

An excursion from computable to automatic structures

In this talk we introduce two classes of structures: computable structures and

automatic structures. We present several examples, theorems, research topics

in the areas, and discuss their motivations, proofs and importance.  The goal will

be to make a transition from computable to automatic structures with an eye

towards decidability. We also give some historical perspective.

Mon 21 October 2013, 15:30-17:00

Akira Yoshimizu (MMM, U. Tokyo), TBA

Room 236, Chemistry Building East (“Kagaku-Higashikan”). Next to our building (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/ (see bottom)

TBA

Thu 17 October 2013, 17:00-18:00

Venanzio Capretta (U. Nottingham), THE CONSTRUCTION OF INFINITY

This talk is about the implementation and use of infinite data structures in computer science, specifically in constructive type theory.

In the first part, I give some history and philosophy of the mathematical theories of infinity, illustrated with some puzzles.

The second part is about solving equations on infinite streams: under what conditions does a recursive definition produce a unique function on streams?

The third part is about a new kind data type, which I call "Wander Types". It allows the definition of non-well-founded structures with fine control on branching behaviour.

Fri 4 October 2013, 17:00-18:00

Tarmo Uustalu (Institute of Cybernetics, Tallinn),

We introduce update monads as a generalization of state monads. Update monads are compatible compositions of reader and writer monads given by a set and a monoid. Distributive laws between such monads are given by monoid actions.

We also discuss a dependently typed generalization of update monads. Unlike simple update monads, those cannot be factored into a reader and writer monad.

Dependently typed update monads arise from cointerpreting directed containers, by which we mean interpreting the opposite of the category directed containers into the category of set functors.

(Joint work with Danel Ahman, University of Edinburgh.)

Tue 30 July 2013, 16:00-17:30

Hiroyoshi Sekine (MMM, U. Tokyo), Nakano’s Modal Type System for Guarded Recursion (Tentative)

アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access:
http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)

Nakano’s λ●μ-calculus and modal type system enable us to assert convergence of some kind of self-referencing programs. His framework is applicable to stream-processing programs. In this talk, first I explain about Nakano’s framework, and then I introduce its application, the ultrametric semantics of stream-processing programs by Krishnaswami and Benton.

Tue 16 July 2013, 16:00-17:00

Toshiki Kataoka (MMM, U. Tokyo), Introduction to Homotopy Type Theory (HoTT), Part II

アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access:
http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)

Tue 9 July 2013, 16:00-17:00

Toshiki Kataoka (MMM, U. Tokyo), Introduction to Homotopy Type Theory (HoTT)

アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access:
http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)

At the beginning of this talk, we introduce two theories: Martin-Löf type theory and homotopy theory.  Then, we discuss analogy between them, which bring us Homotopy type theory with a new axiom (Univalent Axiom), new (higher) inductive types, and so on.

Tue 2 July 2013, 15:30-17:00

Takumi Akazaki (MMM, U. Tokyo), TBA

アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access:
http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)

TBA

Kengo Kido (MMM, U. Tokyo), TBA

TBA

Tue 18 June 2013, 15:30-17:00

Kentaro Honda (Hagiya Lab., U. Tokyo), Quantum Nonlocal Game Semantics

アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access:
http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)

TBA

Ichiro Hasuo (MMM, U. Tokyo), TBA

TBA

Tue 11 June 2013, 15:30-17:00

Kenta Cho (MMM, U. Tokyo), Towards Coalgebraic Fixed Point Logics in a Fibration

アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access:
http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)

TBA

Tue 4 June 2013, 15:30-17:00

Akira Yoshimizu (MMM, U. Tokyo), An attempt to give token machine semantics to proof nets with quantum nodes

アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access:
http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)

TBA

Tue 28 May 2013, 15:30-17:00

Toshiki Kataoka (MMM, U. Tokyo), Topoi, Higher-order logic, and Non-standard analysis

アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access:
http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)

The Łoś Theorem is a fundamental theorem for ultrafilters, which justifies arguments with almost-everywhere''.  The condition to be an ultrafilter in the theorem seemed to be essential, since its classical proof used a law of excluded middle.  However, the Łoś Theorem can be stated with filters, not necessarily ultrafilters.

We introduce (elementary) topoi and their internal language, which is simply-typed higher-order logic.  And then, we state the intuitionistic version'' of the Łoś Theorem for a topos E by constructing a topos F which is called the topos of filters of E.

Tue 21 May 2013, 15:30-17:30

Irek Ulidowski (University of Leicester)

Modelling of bonding with processes ad events

アクセス：
https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access:
http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)

We introduce two forms of modelling of systems that consist of objects that are combined together by the means of bonds. In reaction systems for bonding we define how bonds are created and dissolved via reduction-style semantics. The usefulness of reaction systems is illustrated with examples taken from software engineering and biochemistry. We also introduce reversible event structures and define the notion of configuration. We then discuss how to give semantics of reaction systems for bonding in terms of reversible event structures.

Tue 14 May 2013, 15:30-17:00

Hiroyoshi Sekine (MMM, U. Tokyo), TBA

TBA

Tue 30 April 2013, 15:30-17:30

Takeo Uramoto (Dept. Mathematics, Kyoto University)
Tannaka-style reconstruction theorem for profinite monoids with an application to Eilenberg-Reiterman's variety theory

アクセス：
https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access:
http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)

Eilenberg-Reiterman's variety theory is one of the central theories in algebraic studies of finite automata and regular languages. In its recent development, Rhodes and Steinberg pointed out that the Boolean algebra of regular languages admits a bialgebra structure and revealed its important role in the duality-theoretic formulation of the variety theory. In this talk, we study the structure of the bialgebra of regular languages using a traditional idea from the linear representation theory of groups. In particular, we aim at clarifying a close connection between algebraic structures on the bialgebra of regular languages and geometric structures of finite automata. Our main result claims that there exists a bijective correspondence between bilinear multiplications of regular languages that are compatible with respect to word decompositions and binary products on finite automata that are stable with respect to simulations. This is proved as a corollary of the Tannaka-style reconstruction theorem for profinite monoids, which is an analogue of the classical Tannaka duality theorem for compact groups and indicates a categorical universality of the Boolean algebra of regular languages with respect to finite automata and simulations.

Tue 23 April 2013, 15:30-17:30

Kenshi Miyabe (JSPS Research Fellow, Dept. Math. Inform., Univ. Tokyo),

アクセス：
https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access:
http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)

Tue 16 April 2013, 15:30-17:30

Keisuke Nakano (Univ. Electro-Communications), 2 Talks

Talk 1: Juggling meets coinduction

In this talk, I will present an application of coinduction, juggling.  Buhler et al. presented a mathematical theory of toss juggling by regarding a toss pattern as an arithmetic function, where the function must satisfy a condition for the pattern to be valid.  In this talk, I will formalize their theory in terms of coinduction, reflecting the fact that the validity of toss juggling is related to a property of infinite phenomena.  A tactic is implemented for proving the validity of toss patterns in Coq.  Additionally, the completeness and soundness of a well-known algorithm for checking the validity is certified.  The result exposes a practical aspect of coinductive proofs.  Most part of this talk has been presented in CPP 2012.  Some open problems also will be introduced.

Talk 2: Metamorphism in jigsaw

In this talk, I will present a new computation model for metamorphism.  A metamorphism is an unfold after a fold, consuming an input by the fold then generating an output by the unfold.  It is typically useful for converting data representations, e.g., radix conversion of numbers.  Bird and Gibbons have shown that metamorphisms can be incrementally processed in streaming style when a certain condition holds because part of the output can be determined before the whole input is given.  However, whereas radix conversion of fractions is amenable to streaming, radix conversion of natural numbers cannot satisfy the condition because it is impossible to determine part of the output before the whole input is completed. In this talk, I present a jigsaw model in which metamorphisms can be partially processed for outputs even when the streaming condition does not hold.  The jigsaw model allows us to process metamorphisms in a flexible way that includes parallel computation.  We also apply our model to other examples of metamorphisms.  Most part of this talk is recently published in Journal of Functional Programming.  Additionally, I will present some further work on this work.

Tue 9 April 2013, 15:30-17:00

Tetsuri Moriya (MMM, U. Tokyo), TBA

TBA

Tue 2 April 2013, 16:00-18:00

Ichiro Hasuo (MMM, U. Tokyo), Research Ideas Showcase

Let’s have an informal session with people presenting their research topics. I’ll present (probably more than) several research ideas that I ran into recently.

Tue 18 December 2012, 16:00-17:30

Keiko Nakata (Tallinn University of Technology), 2 Talks

*** 場所・時間が変わりました ***   *** The time and venue have been changed ***

Prior to Dr. Nakata’s talk there will be a “ToPS seminar” at the same location. The talks will be of similar research interests. http://takeichi.ipl-lab.org/~tops/upcoming_seminar.html

Talk 1: Proving open induction using delimited control operators

Open Induction (OI) is a principle classically equivalent to Dependent

Choice, which is, unlike the later, closed under double-negation

translation and A-translation. In the context of Constructive Reverse

Mathematics, Wim Veldman has shown that, in presence of Markov's

Principle, OI on Cantor space is equivalent to Double-negation Shift

(DNS). With Danko Ilik, we have reworked Veldman's proof to give a

constructive proof of OI, where DNS is interpreted using delimited

control operators.

Joint work with Danko Ilik.

Talk 2: Walking through infinite trees with mixed induction and coinduction: A Proof Pearl with the Fan Theorem and Bar Induction.

We study temporal properties over infinite binary red-blue trees in

the setting of constructive type theory. We consider several familiar

path-based properties, typical to linear-time and branching-time

temporal logics like LTL and CTL*, and the corresponding tree-based

properties, in the spirit of the modal mu-calculus. We conduct a

systematic study of the relationships of the path-based and tree-based

versions of eventually always blueness '' and mixed

inductive-coinductive almost always blueness'' and arrive at a

diagram relating these properties to each other in terms of

implications that hold either unconditionally or under specific

assumptions (Weak Continuity for Numbers, the Fan Theorem, Lesser

Principle of Omniscience, Bar Induction).

Joint work with Marc Bezem and Tarmo Uustalu.

Mon 17 December 2012, 16:40-18:10

Tetsuri Moriya (MMM, U. Tokyo), lambda-calculus in pi-calculus

Akira Yoshimizu (MMM, U. Tokyo), An attempt to interpret a quantum language as proof nets

Mon 10 December 2012, 16:40-18:10

Hiroyoshi Sekine (MMM, U. Tokyo), SProcdt: Stream Processing with Infinitesimals

Kenta Cho (MMM, U. Tokyo), Bialgebraic Structural Operational Semantics and Coalgebraic Modal Logic

Mon 3 December 2012, 16:40-18:10

Kentaro Honda (Hagiya Lab., U. Tokyo), Topos Perspective on Quantum Theory II : “Neo-realistic” View of Quantum Physics

Toshiki Kataoka (MMM, U. Tokyo), Dana Scott’s Construction of D_\infty, Categorically

A reflexive domain D_\infty was constructed by D. Scott in 1972.  While the construction was very complicated, some reformulation in a category theory makes it clear.

Mon 19 November 2012, 16:40-18:10

Tetsuri Moriya (MMM, U. Tokyo), HORSs as coalgebras

Akira Yoshimizu (MMM, U. Tokyo), An Overview of Geometry of Interaction

Fri 9 November 2012, 10:30-12:00

Jan Rutten (CWI Amsterdam & Radboud Univ. Nijmegen),
The method of coalgebra--an overview

Since the early nineties, coalgebra has become an active area of research in which one tries to understand all kinds of infinite data types, automata, transition systems and dynamical systems from a unifying perspective. The focus of coalgebra is on observable behaviour and one uses coinduction as a central methodology, both for behavioural specifications and to prove behavioural equivalences. These days, one uses coalgebraic techniques in a wide variety of areas, ranging from automata theory to software engineering to ecology. In this talk, we shall illustrate the coalgebraic approach by discussing a number examples, including streams, automata and circuits.

Mon 5 November 2012, 16:40-18:10

Hiroyoshi Sekine (MMM, U. Tokyo), Differential Equations in Whiledt/SProcdt

Kenta Cho (MMM, U. Tokyo), Introduction to Coalgebraic Modal Logic

Tue 30 October 2012, 16:40-18:10

Ana Sokolova (U. Salzburg),
Quantitative relaxations of concurrent data structures

This talk is about our recent work on relaxing the semantics of concurrent data structures, in a quantitative way, so that they allow better-performing implementations. By their nature, data structures are bottlenecks in the presence of concurrency, e.g.  the top pointer of a stack is a point of contention for which all threads compete. As a consequence, implementations of concurrent data structures often show negative scalability. Recent trends in concurrency show that relaxing the semantics may be the way to better performance. In this work we provide a framework for quantitative relaxations of concurrent data structures, where the allowederror" from the perfect semantics is quantified by a distance. During the talk, we will use a stack as a running example. Also we present new concurrent implementation of a quantitatively relaxed stack that performs well and shows positive scalability.

(joint work with Thomas A. Henzinger, Christoph M. Kirsch, Hannes Payer, and Ali Sezgin)

Mon 22 October 2012, 16:40-18:10

Toshiki Kataoka (MMM, U. Tokyo), Topos Theory for Logic: Elementary Notions and Examples

There are some views on topoi.  Setting aside the applications for algebraic geometry, I will introduce topoi as models for intuitionistic higher-order logic in this talk.  After that, I describe the sheaf topoi on topological spaces as concrete examples, and show how topoi and their internal languages work.

Kentaro Honda (Hagiya Lab., Dept. CS, U. Tokyo), Topos Perspective on Quantum Theory: Presheaf and Kochen-Specker Theorem

Kochen-Specher theorem, which characterize quantum physics, states that there does not exist any valuation satisfying functional composition condition (FUNC). Because of this theorem, we can not assign true or false to quantum propositions. However, this theorem does not assert the impossibility of partial valuations. In this talk, I show that a partial valuation can be extended to a sieve-valued generalized valuation, using a certain presheaf that arises naturally in quantum physics.

Tue 9 October 2012, 16:50-18:10

Akira Yoshimizu (MMM, U. Tokyo), Geometry of Synthesis: Game Semantics and Hardware Compilation

(This is a replay of the talk done at summer seminar with RIMS, 24 Sept.)

Game semantics, developed in the 90s, is an approach to give denotational semantics to various kinds of programming languages, logic, and type systems. Recently it has been studied actively, since it gives us formal semantics with some nice features, such as full abstraction or full completeness. In this talk, first I will introduce basic notions and intuition of what called game semantics (rather informally). Then, as an application of game semantics, we see a game model of SCI (a simple programming language with concurrency). The game model turns out to coincide with a logical circuit representation, event logic -- therefore a compiler that translates an (extension of) SCI program into a VHDL code (i.e. a logical circuit) has been studied and developed by Ghica et al.

References:

[1] J. M. E. Hyland, C.-H. Luke Ong: On Full Abstraction for PCF: I, II, and III. Inf. Comput. 163(2): 285-408 (2000)

[2] Samson Abramsky, Radha Jagadeesan, Pasquale Malacaria: Full Abstraction for PCF. Inf. Comput. 163(2): 409-470 (2000)

[3] Dan R. Ghica, Alex Smith: Geometry of Synthesis II: From Games to Delay-Insensitive Circuits. Electr. Notes Theor. Comput. Sci. 265: 301-324 (2010)

Fri 24 August 2012, 17:30-20:00

Naohiko Hoshino (RIMS, Kyoto U.),

Talk 1: A Representation Theorem for Unique Decomposition Categories

Haghverdi introduced the notion of unique decomposition categories as a foundation for categorical study of Girard’s Geometry of Interaction (GoI). The execution formula in GoI provides a semantics of cut-elimination process, and we can capture the execution formula in every unique decomposition category: each hom-set of a unique decomposition category comes equipped with a partially defined countable summation, which captures the countable summation that appears in the execution formula. The fundamental property of unique decomposition categories is that if the execution formula in a unique decomposition category is always defined, then the unique decomposition category has a trace operator that is given by the execution formula. In this paper, we introduce a subclass of unique decomposition categories, which we call strong unique decomposition categories, and we prove the fundamental property for strong unique decomposition categories as a corollary of a representation theorem for strong unique decomposition categories: we show that for every strong unique decomposition category C, there is a faithful strong symmetric monoidal functor from C to a category with countable biproducts, and the countable biproducts characterize the structure of the strong unique decomposition category via the faithful functor.

Talk 2: Step Indexed Realizability Semantics for a Call-by-Value Language

Based on Basic Combinatorial Objects

We propose a mathematical framework for step indexed realizability semantics of a call-by-value polymorphic lambda calculus with recursion, existential types and recursive types. Our framework subsumes step indexed realizability semantics by untyped call-by-value lambda calculi as well as categorical abstract machines. Starting from an extension of Hofstra’s basic combinatorial objects, we construct a step indexed categorical realizability semantics. Our main result is soundness and adequacy of our step indexed realizability semantics. As an application, we show that a small step operational semantics captures the big step operational semantics of the call-by-value polymorphic lambda calculus. We also give a safe implementation of the call-by-value polymorphic lambda calculus into a categorical abstract machine.

Thu 5 July 2012, 16:40-17:10

Hiroyoshi Sekine (MMM, U. Tokyo),  Simulink Diagrams as Hyperstream Processing Systems

(Joint work with Kohei Suenaga and Ichiro Hasuo. To appear in NSV 2012)

We present StP^dt, an extension of Lustre-like stream-processing language with an infinitesimal value dt. The infinitesimal value enables StP^dt to capture the behavior of hybrid systems modeled in the continuous signal-processing style such as Simulink models. We present by intuition how StPdt deals with continuous signals and signal processing blocks based on nonstandard analysis. The main idea is to convert continuous signals into hyperstreams, streams whose sampling interval is dt, and apply sectionwise execution.

Mon 11 June 2012, 16:40-18:10

本発表では２レベルゲーム意味論という新しいゲーム意味論を導入し、

これを用いることで共通型システムのゲーム的解釈が与えられることを示

す。ゲーム意味論と共通型理論は近年の高階モデル検査（＝高階再帰スキー

ムという文法が生成する木のモデル検査）の理論において重要な役割を果

たしており、これらの間の関係を明らかにすることは高階モデル検査の理

な対応関係は知られていたが、形式的な対応関係は本発表で導入する２レ

ベルゲーム意味論によるものがはじめてである。

２レベルゲームは、その名が示す通り、上層のゲームと下層のゲームの

２つ（とそれらの間の関係）から成る。下層のゲームは項の計算を表し、

しており、その関係は上層のゲームから下層のゲームへの写像として表現

される。

(A) （単純型システムの詳細化であるような）共通型システムにおける

型導出は２レベルゲームの勝利戦略として解釈することができる。

さらに、２レベルゲーム意味論は共通型システムに対して fully

complete である。つまり、すべての（２レベルゲームにおける）

勝利戦略はある（共通型システムの）型導出の解釈となっている。

(B) 共通型システムの重要な性質に主拡張補題というものがある。これ

に対応する性質を、２レベルゲームも満たすことを示す。この証明

は純粋にゲーム意味論的手法で行うことができる。

また最後に、２レベルゲーム意味論の高階モデル検査への応用と今後の

[1] C.-H. Luke Ong and Tsukada Takeshi.  Two-Level Game

Semantics, Intersection Types, and Recursion Schemes.  ICALP

2012 (to appear).

Thu 24 May 2012, 16:40-18:10

Yuto Takei (U. Tokyo),  Formal Proof of Bellman-Ford Algorithm on Why3

The proof works on discrete algorithms are often very complicated.  Without the help of automated theorem provers, it is needed to provide large amount of interactive proof scripts, which requires thorough human involvement.

Why3 is a proving platform developed in Laboratoire de Recherche Informatique (LRI), Université Paris-Sud that allows to combine several theorem provers. By using it, one can purely separate the logical specification and algorithm implementation. As a result, Why3 contributes to make proof tasks more automatized than by using theorem provers individually.

In our work, Bellman-Ford algorithm was chosen as one example to distinguish the major problems in formally proving discrete algorithms. My presentation will consists of four parts. First, I will explain the algorithm behavior. Second, I will introduce Why3 with small examples available from the official gallery. Then I will explain and show the complete proof as a demo. Finally as a conclusion, I will illustrate the roadmap of the work.

This work was realized by the courtesy of Dr. Jean-Christophe Filliâtre in LRI, who supervised me during the internship in Feburary - March 2012.

References:

[1] François Bobot, Jean-Christophe Filliâtre, Claude Claude Marché, and Andrei Paskevich. Why3: Shepherd your herd of provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages, Wroclaw, Poland, August 2011.

[2] Boris V. Cherkassky and Andrew V. Goldberg. Negative-cycle detection algorithms. Mathematical Programming, 85:277–311, 1999.  10.1007/s101070050058.

[3] Sylvain Conchon, Jean-Christophe Filliâtre, and Julien Signoles.  Designing a Generic Graph Library using ML Functors. In Marco T.  Morazán and Henrik Nilsson, editors, The Eighth Symposium on Trends in Functional Programming, volume TR-SHU-CS-2007-04-1, pages XII/1–13, New York, USA, April 2007. Seton Hall University.

[4] Thomas H. Cormen, Clifford Stein, Ronald L. Rivest, and Charles E.  Leiserson. Introduction to Algorithms. McGraw-Hill Higher Education, 2nd edition, 2001.

Wed 16 May 2012, 14:50-16:20

Kazuyuki Asada (National Institute of Informatics),

Generalization of UnCAL with any algebraic computational effect

UnCAL, which is introduced by Buneman et al., is (can be seen as) a simply typed (lambda) calculus extended with a kind of graph data type and with some functions for the graph.  The graph is multi-rooted edge-labeled nondeternistic graph.  UnCAL is designed as evaluation of any terms terminate as finite graphs, and so does not have non-terminating powerful operator such as fixed point operator; instead, UnCAL has structural recursion.  Technical points of UnCAL consists of definitions of

1) graph (a kind of coalgebra),

2) graph representation (bialgebra and its full-definability), and

3) graph transformation (structural recursion).

(and efficiency, not addressed in my work.)

In this talk I explain how to generalize UnCAL (i.e., the above three points) with any ranked monad, which replace the above "nondeterministic" with any computational effects such as weighted-nondeterminism (multiset monad), probablistic-nondeterminism (distribution monad) and ordered-nondeterminism (list monad).  One main contribution is how to construct free iteration monads.

Tue 15 May 2012, 16:40-18:10

Bart Jacobs (Radboud U. Njimegen),  New directions in quantum logic

• 当研究室のセミナーにはじめておいでになる方は，
• こちら http://www.doodle.com/7zsyhidh2r478xyk に参加表明をいただけると幸いです．（ペンネームでかまいません）

The talk will use categorical techniques to give a new way of representing predicates that is especially suited for "quantitative" predicate logic. The relevant structure is illustrated for classical, probabilistic and quantum logic. These new predicates give rise to fibred/indexed categories. In the quantum case the Born rule appears as a form of substitution. Predicates can also be used to specify measurements in this setting.

Mon 16 Apr 2012, 16:40-18:10

Toshiki Kataoka (U. Tokyo),  Lebesgue integration in 90 minutes.

Lebesgue integration is the standard integration theory at present.  Why?  While it is no more convenient than Riemann’s one for calculating the integrals of usual functions (e.g. x^2, sin x, … ), Lebesgue integration has many formulas (e.g. “limit and integral can be swapped”) with a kind of natural assumption.  I will talk about the definitions, the results, and the key idea for their proofs.

Fri 13 Apr 2012, 16:40-18:10

Paul-Andre Mellies (U. Paris VII),

Tensorial logic: a type-theoretic foundation for game semantics

Tensorial logic is a primitive logic of tensor and negation which refines linear logic by relaxing the hypothesis that negation is involutive. I will explain how the logic provides a type-theoretic foundation to game semantics, and how it may be extended with algebraic effects in order to recover specific categories of games and strategies.

Thu 12 Apr 2012, 16:40-18:10

David Galindo (U. Luxembourg),

Encryption Schemes Secure in the Presence of Key Cycles

Traditionally the security of encryption schemes has relied

on the assumption that the decryption keys are not accessible to the

attacker neither directly (e.g. some parts of the decryption key might

have been leaked) nor indirectly (e.g. never encrypt messages that

depend on the decryption key). However this assumption has been

challenged in different contexts in the last decade. The main sources

have been side-channel attacks and formal cryptography.

In this talk we will give an introduction to the traditional security

notions for encryption schemes as well as the new notion of security

in the presence of key cycles. We will explain why the latter notion

is difficult to achieve using previous techniques. Finally we will

introduce the first practical encryption scheme achieving the latter

security notion (appeared at CRYPTO 2008).

Tue 10 Jan 2012, 16:30-18:00

Kenta Cho (U. Tokyo),  Gelfand Duality

The commutative Gelfand-Naimark theorem states relation between commutative C*-algebras and compact Hausdorff spaces. It itself contains no categorical notion, but from a categorical point of view, the theorem represents the duality, what is called the Gelfand Duality, between the category of commutative C*-algebras and that of compact Hausdorff spaces. In the seminar, first I will give the overview of the proof of the theorem, and then talk the categorical meanings.

Tue 13 Dec 2011, 16:30-18:00

Hiroyoshi Sekine (U. Tokyo),  Flows and Stream Processing

To verify a hybrid system, continuous values need to be represented in discrete form. The idea of nonstandard analysis gives us a solution to the problem how to realize this. In the seminar, I will talk about an introduction to nonstandard analysis, and  how to encode a continuous flow as a sequence and to decode it. This conversion enables us to treat continuous values by using discrete method.

Thu 1 Dec 2011, 13:30-15:00

Toshiki Kataoka (U. Tokyo),  Viro’s patchworking method

I will present a method to construct hypersurfaces on real varieties of given isotopy types.  Roughly speaking, patchworking, the name of this method, means "to stitch some parts of many hypersurfaces together".  Viro discovered that the properly patchworked piece-wise-hypersurface is approximated by a genuine hypersurface!

In the seminar, I will talk about toric varieties first, then, sketch the proof of the theorem and show the examples.

Tue 29 Nov 2011, 16:30-18:00

Akira Yoshimizu (U. Tokyo),  Introduction to Linear Logic

This presentation is based on

Vincent Danos & Roberto Di Cosmo, The Linear Logic Primer.

First I will introduce Linear Logic as “logic of resource” informally,

then take a look at its formal definition by a variant of sequent calculus.

The definition is obtained from usual sequent calculus, forbidding some rules and adding two modalities.

I will also show some important equivalences in Linear Logic.

Preliminary knowledge about sequent calculus is not necessary.

Tue 15 Nov 2011, 16:30-18:00

Tetsuri Moriya (U. Tokyo),  Adequacy for SOS by Category Theory : Bialgebras

I will explain the contents of

Bartek Klin: Bialgebras for structural operational semantics: An introduction

This paper provides us how to guarantee congruences of SOS specifications, which are definitely necessary, at level of category theory. To do so, we use bialgebras, which include both algebraic and coalgebraic structures that respectively correspond to initial and final semantics.

I won’t assume so much knowledge about category theory.......

### Tue 18 Oct 2011, 16:30-18:30

• Kohei Suenaga (Kyoto U.), Programming with Infinitesimals: A While-Language for Hybrid System Modeling

(Joint work with Ichiro Hasuo, U. Tokyo. The paper appeared in ICALP 2011)

We add, to the common combination of a WHILE-language and a Hoare-style program logic, a constant dt that represents an infinitesimal (i.e. infinitely small) value. The outcome is a framework for modeling and verification of hybrid systems: hybrid systems exhibit both continuous and discrete dynamics and getting them right is a pressing challenge. We rigorously define the semantics of programs in the language of nonstandard analysis, on the basis of which the program logic is shown to be sound and relatively complete.

• Tachio Terauchi (Nagoya U.), 関数型プログラムのためのプログラム解析とプログラム検証

### Tue 11 Oct 2011, 16:30-18:00

Ichiro Hasuo (U. Tokyo),  Semantics of Higher-Order Quantum Computation via Geometry of Interaction

(Joint work with Naohiko Hoshino, RIMS, Kyoto University. The paper appeared in LICS 2011)

While much of the current study on quantum computation employs low-level formalisms such as quantum circuits, several high-level languages/calculi have been recently proposed aiming at structured quantum programming. The current work contributes to the semantical study of such languages, by providing interaction-based semantics of a functional quantum programming language; the latter is based on linear lambda calculus and is equipped with features like the ! modality and recursion. The proposed denotational model is the first one that supports the full features of a quantum functional programming language; we also prove adequacy of our semantics. The construction of our model is by a series of existing techniques taken from the semantics of classical computation as well as from process theory. The most notable among them is Girard’s Geometry of Interaction (GoI), categorically formulated by Abramsky, Haghverdi and Scott.  The mathematical genericity of these techniques—largely due to their categorical formulation—is exploited for our move from classical to quantum.

### Tue 4 Oct 2011, 16:30-18:00

Ichiro Hasuo (U. Tokyo), Theory of Coalgebra: Towards Mathematics of Systems

（2010/6/30 の情報科学科講演会のリプレイです）

1990年代の Jacobs と Rutten の諸結果に始まり，状態遷移システム(たとえばオートマトン)の圏論的モデルとして成功を収めつつある coalgebra (余代数)の概念について，概説します．最近盛り上がっているいくつかのトピックについて手短に紹介しますが，ポイントは圏論(「なんでも矢印で書こう！」というフォーマリズムです)の持つ抽象力です．計算機科学における，一見異なるいろいろな現象の共通する本質をとらえて，「同じもの」として記述することができます．