The Power of Abstraction
in a Theory, a Project, and an Inspiring Mind
Symposium on the Categorical Unity of the Sciences
Kyoto, Japan. March 22, 2019

Ichiro Hasuo
National Institute of Informatics & SOKENDAI
Research Director, JST ERATO MMSD ProjectWhy Categories?
Why category theory?

“Unity” as Yoshi talked about (?)

My answer: for generalization & abstraction
A plain math. language“Scalability is the end, compositionality
is the means, category theory is the means
to the means.” (Jules Hedges)

Equipped only witha (typed) compositional structure

A nicely extendable base language:accommodates various additional features(monoidal, topos, locally presentable/accessible, eﬀectus, …)

Make theory builders aware of what exactly (s)he is using,and thus extract the essence of a theory
Then, why abstraction??
2

Hasuo (NII, Tokyo)

The Power of Abstraction
in atheoryin aproject

… and
in an
inspiring mind
3

Hasuo (NII, Tokyo)

??

λ-calculus
concurrency

??
??

game
domaintheory semantics
bisimulation

databasequantummechanics

contextuality

Chu spaces

economics
4

Hasuo (NII, Tokyo)

Outline
Abstraction in a Theory I
Categorical GoI (geometry of interaction)[Abramsky, Haghverdi & Scott, MSCS’02] [Hasuo & Hoshino, LICS’11] [Hoshino, Muroya & Hasuo, CSL-LICS’14][Muroya, Hoshino & Hasuo, POPL’16] [Hasuo & Hoshino, APAL’17]

Abstraction in a Theory II
Codensity Bisimulation Games[Katsumata & Sato, CALCO’15] [Sprunger, Katsumata, Dubut & Hasuo, CMCS’18][Komorida, Katsumata, Hu, Klin & Hasuo, submitted (soon on arXiv)]

Abstraction in a ProjectIntroducing ERATO MMSD Project:from categorical foundations to automated driving

Abstraction in an Inspiring Mind
5

Hasuo (NII, Tokyo)

Abstraction in a Theory:“Categorical Transfer”
Defn.

T (e) =✓

theory of coalgebrasin K`(Be )◆, where Be is a monad

Abstract TechniqueThm. Coalgebraic proof methods (such as (bi)simulations) are v
A

T[_]
Identify“mathematicalessense”

Proof.

::=

true | false | A1 ^ A2 | ¬A | a1 < a2 |8x 2 ⇤N. A | 8x 2 ⇤R. A

By the following characterizations in K`(Be ).
FX
O
c
X

F behc /

F OZ
final
/Z

behc
system behavior

Chooseparameter e1

Existing Technique

FX
O
c
X

Chooseparameter e2

T[e2]
6

w

/ FY
O
d
/Y

f
simulation

Novel Technique

T1 = T[e1]FfOutline
Abstraction in a Theory I
Categorical GoI (geometry of interaction)[Abramsky, Haghverdi & Scott, MSCS’02] [Hasuo & Hoshino, LICS’11] [Hoshino, Muroya & Hasuo, CSL-LICS’14][Muroya, Hoshino & Hasuo, POPL’16] [Hasuo & Hoshino, APAL’17]

Abstraction in a Theory II
Codensity Bisimulation Games[Katsumata & Sato, CALCO’15] [Sprunger, Katsumata, Dubut & Hasuo, CMCS’18][Komorida, Katsumata, Hu, Klin & Hasuo, submitted (soon on arXiv)]

Abstraction in a ProjectIntroducing ERATO MMSD Project:from categorical foundations to automated driving

Abstraction in an Inspiring Mind
7

Hasuo (NII, Tokyo)

Abstraction in a Theory I
Categorical GoI

x2X

f

Ï

Ï

f: X ⇥N !
T (X ⇥ N)[Abramsky, Haghverdi & Scott, MSCS’02][Hasuo & Hoshino, LICS’11] [Hoshino, Muroya & Hasuo, CSL-LICS’14][Muroya, Hoshino & Hasuo, POPL’16] [Hasuo & Hoshino, APAL’17]
8

Hasuo (NII, Tokyo)

Abstraction in a Theory:“Categorical Transfer”
Categorical Geometry of Interaction[Abramsky, Haghverdi, Scott]✓Defn.

T (e) =

theory of coalgebrasin K`(Be )◆, where Be is a monad

Abstract TechniqueThm. Coalgebraic proof methods (such as (bi)simulations) are v
A

T[_]
Identify“mathematicalessense”

true | false | A1 ^ A2 | ¬A | a1 < a2 |8x 2 ⇤N. A | 8x 2 ⇤R. A

By the following characterizations in K`(Be ).
FX
O
c
X

F behc /

F OZ
final
/Z

behc
system behavior

Chooseparameter e1

Existing Technique

T1 = T[e1]Geometry of Interaction[Girard]

Proof.

::=

FX
O
c
X

Ff
w

/ FY
O
d
/Y

f
simulation

Chooseparameter e2
Novel TechniqueT[e2]
GoI with nondeterministic, probabilistic,
quantum, and other effects… ➜ Memoryful
Geometry of Interaction [Hoshino, Muroya, Hasuo, …]
9Outline

GoI w/“GoI Animation”

T-branchingÏÏ f : N ! TNf

[IH & Hoshino, LICS’11]

x2X

f

Ï

Ï

f: X ⇥N !
T (X ⇥ N)

Memoryful GoI

Categorical GoI[Hoshino, Muroya & IH,
CSL-LICS’14 & POPL’16][Abramsky, Haghverdi & Scott, MSCS’02]

Coalgebra meets higher-order computationin Geometry of Interaction [Girard, LC’88]

Hasuo (NII, JP)Geometry of Interaction (GoI)
J.-Y. Girard, at Logic Colloquium ’88
Provides “denotational” semantics (w/ operational flavor)
for linear λ-term M
As a compilation technique[Mackie, POPL’95] [Pinto, TLCA’01] [Ghica et al., POPL’07, POPL’11, ICFP’11, ...]

Two presentations:(Operator-) Algebraic [Girard]ax
ax

Token machines/
interaction abstract machines

ax

ax

ax

ax

ax

[Danos & Regnier, TCS’99] [Mackie, POPL’95]

ax

Ï

⌦

`
`
B↵

⌦

`
`
B↵

(a)

(↵1? ` ↵2? )`(↵(b)
3 ⌦ [ ])

Hasuo (NII, JP)

The GoI Animation
JM K = ( NN, a partial function )= “piping”

↓

↓

↓

0

1 token
2 3

✖

↓
...

(countably many)

[|M|]

...
↓

↓

↓

↓

Hasuo (NII, JP)

The GoI Animation
Function application JM N K

by “parallel composition + hiding”

Hasuo (NII, JP)

...

...
[|MN|]...

JM N K
=

...

[|M|]

[|N|]

...

...

...

...
“parallel composition + hiding”(cf. AJM games)...
[|MN|]JM N K
=

...
[|M|]

...
[|N|]

...

...

... ➜ M = x. x + 1 N = 2
N =2➜ M = x. 1
N = x. (x + 1)
➜ M = f. f 1

Outline
Coalgebra meets higher-order computationin Geometry of Interaction [Girard, LC’88]“GoI Animation”

Categorical GoI[Abramsky, Haghverdi & Scott, MSCS’02]

Hasuo (NII, JP)Categorical GoI
Axiomatics of GoI
in the categorical language
Our main reference:[AHS02] S. Abramsky, E. Haghverdi, and P. Scott, Geometry of interaction
and linear combinatory algebras, Math. Str. Comp. Sci, 2002
Especially its technical report version (Oxford CL),
since it’s a bit more detailed
See also:
IH and Naohiko Hoshino. Semantics of Higher-Order Quantum
Computation via Geometry of Interaction. Annals Pure & Applied Logic
2017.
arxiv.org/abs/1605.05079
Hasuo (NII, JP)

The Categorical GoI
Workflow
Traced monoidal category C+ other constructs ➜ “GoI situation” [AHS02]

A

f
B

Categorical GoI [AHS02]

A

C
tr

C

7 !

tr(f )B

Applicative str. + combinators
Model of untyped calculus

Linear combinatory algebra
PER, ω-set, assembly, ...

Realizability

Linear category“Programming in untyped λ”

Model of typed calculus

Hasuo (NII, JP)What we use (ingredient)

GoI situation
Defn. (GoI situation [AHS02])
A GoI situation is a triple (C, F, U ) where• C = (C, ⌦, I) is a traced symmetric monoidal category(TSMC);• F : C ! C is a traced symmetric monoidal functor,
equipped with the following retractions (which are monoidal
natural transformations).
e : F F C F : e0d : id C F : d0
c : F ⌦ F C F : c0
w : KI C F : w 0Comultiplication
Dereliction
Contraction
Weakening

Here KI is the constant functor into the monoidal unit I;• U 2 C is an object (called reflexive object), equipped withthe following retractions.
j : U ⌦U CU : k
ICUu : FU C U : v

Hasuo (NII, JP)GoI situation
Defn. (GoI situation [AHS02])
A GoI situation is a triple (C, F, U ) where• C = (C, ⌦, I) is a traced symmetric monoidal category(TSMC);

Monoidal category (C, ⌦, I)
String diagrams• F : C ! C is a traced symmetric monoidal functor,
equipped with the following retractions (which are monoidal
natural transformations).
e : FF C F : ed : id C F : d00c : F ⌦ F C F : c0
w : KI C F : w 0Comultiplication
Dereliction

A

f

!B
A

Contraction
Weakening

B

g f

!C

A

g

!C

f
B

g

C

Here KI is the constant functor into the monoidal unit I;• U 2 C is an object (called reflexive object), equipped withthe following retractions.
j : U ⌦U CU : k
ICUu : FU C U : v

A

f

!B

A⌦C

h

C

f ⌦g

g

!D

!B⌦D

(f ⌦ g)

C

A

f
B

g

D

g

f

h

Hasuo (NII, JP)GoI situation
Defn. (GoI situation [AHS02])
A GoI situation is a triple (C, F, U ) where• C = (C, ⌦, I) is a traced symmetric monoidal category(TSMC);• F : C ! C is a traced symmetric monoidal functor,
equipped with the following retractions (which are monoidal
natural transformations).
e : F F C F : e0d : id C F : d0
c : F ⌦F CF : cw : KI C F : w 00Comultiplication
Dereliction
Contraction
Weakening

Here KI is the constant functor into the monoidal unit I;

Traced monoidal category“feedback”
A⌦C
A

that isf!B⌦Ctr(f )!B• U 2 C is an object (called reflexive object), equipped withthe following retractions.
j : U ⌦U CU : k
ICU

A

f

u : FU C U : v

B

A

C
tr

C

7 !

tr(f )

B

Hasuo (NII, JP)

String Diagram vs.
“Pipe Diagram”
I use two ways of depicting partial
functions N * N
In the monoidal category(Pfn, +, 0)

N
JM K

N

Pipe diagram

String diagram

Hasuo (NII, JP)Traced Sym. Monoidal Category(Pfn, +, 0)Category Pfn of partial functions
Obj. A set X
Arr. A partial function
X ! Y in Pfn
XY, partial function

Xf
Y

is traced symmetric monoidal
Hasuo (NII, JP)Traced Sym. Monoidal Category(Pfn, +, 0)
X +Z
X

X

f

!Y +Z

tr(f )!Yin PfnZ

f
Y

in PfnZ

How?

fXY (x) :=fYf (x) if f (x) 2 Y?
o.w.

Similar for fXZ , fZY , fZZ
Execution formula (Girard)
Partiality is essential(infinite loop)

Trace operator:X(

tr(f ) =
fXY t

a

n2N

fZY

(fZZ )nfXZ!

Hasuo (NII, JP)GoI situation
Defn. (GoI situation [AHS02])
A GoI situation is a triple (C, F, U ) where• C = (C, ⌦, I) is a traced symmetric monoidal category(TSMC);• F : C ! C is a traced symmetric monoidal functor,
equipped with the following retractions (which are monoidal
natural transformations).
e : FF C F : ed : id C F : d00c : F ⌦ F C F : c0
w : KI C F : w 0

Traced sym. monoidal cat.
Where one can “feedback”
A

Comultiplication
Dereliction
Contraction
Weakening

Here KI is the constant functor into the monoidal unit I;• U 2 C is an object (called reflexive object), equipped withthe following retractions.

C

f
B

A
tr

C

7 !

tr(f )

B

Why for GoI?

j : U ⌦U CU : k
ICUu : FU C U : v

Hasuo (NII, JP)...
[|MN|]...

JM N K
=

...

[|M|]

[|N|]

...

...

...

JM K

JN K

in string diagram

GoI situation
Defn. (GoI situation [AHS02])
A GoI situation is a triple (C, F, U ) where

Traced sym. monoidal cat.

• C = (C, ⌦, I) is a traced symmetric monoidal category(TSMC);

Where one can “feedback”• F : C ! C is a traced symmetric monoidal functor,
equipped with the following retractions (which are monoidal
natural transformations).
e : FF C F : ed : id C F : d00c : F ⌦ F C F : c0
w : KI C F : w 0

A

Comultiplication
DerelictionfContraction
Weakening

B

A
tr

C

7 !

tr(f )

B

Why for GoI?

Here KI is the constant functor into the monoidal unit I;• U 2 C is an object (called reflexive object), equipped withthe following retractions.
j : U ⌦U CU : k
ICUu : FU C U : v

C

M

N

=

M
N

[ ]

= tr

M

N

Leading example: Pfn

Hasuo (NII, JP)GoI situation
Defn. (GoI situation [AHS02])
A GoI situation is a triple (C, F, U ) where• C = (C, ⌦, I) is a traced symmetric monoidal category(TSMC);• F : C ! C is a traced symmetric monoidal functor,
equipped with the following retractions (which are monoidal
natural transformations).
e : F F C F : e0d : id C F : d0
c : F ⌦F CF : cw : KI C F : w 00Defn. (Retraction)
A retraction from X to Y ,f :XCY :g ,Comultiplication
Dereliction
Contraction
WeakeningfidHere KI is the constant functor into the monoidal unit I;• U 2 C is an object (called reflexive object), equipped withthe following retractions.
j : U ⌦U CU : k
ICUu : FU C U : v“embedding”

is a pair of arrows

such that g

9X h

(

Y

g

“projection”

f = idX .

Functor F
For obtaining ! : A → A
Hasuo (NII, JP)GoI situation
Defn. (GoI situation [AHS02])
A GoI situation is a triple (C, F, U ) where• C = (C, ⌦, I) is a traced symmetric monoidal category(TSMC);• F : C ! C is a traced symmetric monoidal functor,
equipped with the following retractions (which are monoidal
natural transformations).
e : F F C F : e0d : id C F : d0
c : F ⌦F CF : cw : KI C F : w 00Comultiplication
Dereliction
Contraction
Weakening

Here KI is the constant functor into the monoidal unit I;• U 2 C is an object (called reflexive object), equipped withthe following retractions.

The reflexive object U
Retr.
j

,

j
U ⌦ Uh
k

)

U

k

with
j
k

= id

j : U ⌦U CU : k
ICUu : FU C U : v

Hasuo (NII, JP)GoI situation

The reflexive object U

Defn. (GoI situation [AHS02])
A GoI situation is a triple (C, F, U ) where• C = (C, ⌦, I) is a traced symmetric monoidal category(TSMC);• F : C ! C is a traced symmetric monoidal functor,
equipped with the following retractions (which are monoidal
natural transformations).
e : F F C F : e0d : id C F : d0
c : F ⌦ F C F : c0
w : KI C F : w 0Comultiplication
Dereliction
Contraction
Weakeningj,k

Why for GoI?

M

N

Here KI is the constant functor into the monoidal unit I;• U 2 C is an object (called reflexive object), equipped withthe following retractions.
j : U ⌦U CU : k
ICUu : FU C U : v

Example in Pfn:

N ⇥ Pfn, with

N + N = N,
N·N=N

Hasuo (NII, JP)

A

f
B

A

C

GoI Situation: Summary
tr

C

7 !

tr(f )

B

Categorical axiomatics of
the “GoI animation”

Defn. (GoI situation [AHS02])
A GoI situation is a triple (C, F, U ) where• C = (C, ⌦, I) is a traced symmetric monoidal category(TSMC);• F : C ! C is a traced symmetric monoidal functor,
equipped with the following retractions (which are monoidal
natural transformations).
e : F F C F : e0d : id C F : d0
c : F ⌦F CF : cw : KI C F : w 0
0

For ! , via

Comultiplication
Dereliction
Contraction
WeakeningF

7 !
fHere K is the constant functor into the monoidal unit I;I

fff• U 2 C is an object (called reflexive object), equipped withthe following retractions.

u : FU C U : v,...

Example:j : U ⌦U CU : k
ICU

j

N

M

k

(Pfn, N ·
···

, N)
···

···

Hasuo (NII, JP)Categorical GoI:
Constr. of an LCA
Thm. ([AHS02])
Given a GoI situation (C, F, U ), the homset

Uf

C(U, U )U

2 C(U, U )carries a canonical LCA structure.

Applicative str. ⋅! operator

g·f:= tr (Uf) ⇥ k ⇥ g ⇥ jCombinators B, C, I, ...

=

g
f

=

g

f
Hasuo (NII, JP)Summary:
Categorical GoI
Defn. (GoI situation [AHS02])
A GoI situation is a triple (C, F, U ) where• C = (C, ⌦, I) is a traced symmetric monoidal category(TSMC);• F : C ! C is a traced symmetric monoidal functor,
equipped with the following retractions (which are monoidal
natural transformations).
e : F F C F : e0d : id C F : d0
c : F ⌦ F C F : c0
w : KI C F : w 0

Thm. ([AHS02])
Given a GoI situation (C, F, U ), the homset
C(U, U )carries a canonical LCA structure.

Comultiplication
Dereliction
Contraction
Weakening

Here KI is the constant functor into the monoidal unit I;• U 2 C is an object (called reflexive object), equipped withthe following retractions.
j : U ⌦U CU : k
ICUu : FU C U : v

Hasuo (NII, JP)Outline
Coalgebra meets higher-order computationin Geometry of Interaction [Girard, LC’88]
GoI w/“GoI Animation”

T-branchingÏÏ f : N ! TNf

[IH & Hoshino, LICS’11]

Categorical GoI[Abramsky, Haghverdi & Scott, MSCS’02]

Hasuo (NII, JP)Categories
of different
sets andKl(T) forbranching(functions with different branching/partiality)

Why Categorical Generalization?:monads T
Examples Other Than Pfn [AHS02]
Pfn (partial functions)(Potential) non-termination

X
Y in Pfn
XY, partial function where LY = {⇥} + Y
X
LY in Sets

Rel (relations)
X ⇤ Y in Rel
R ⇥ X Y, relation
X ⇤ PY in Sets

Non-determinism
where P is the powerset monad

DSRel

X ⇥ Y in DSRel
X ⇥ DY in Sets
X
where DY = {d : Y ⇥ [0, 1] |d(y)Probabilistic branching1}yHasuo (NII, JP)

➜

➜

➜

Different Branching in
The GoI Animation
Pfn (partial
functions)
Pipes can be stuck

↓

↓

↓

↓

1

2

3

4

Rel (relations)
Pipes can branch

...

1
1

✖

1

2

3

3

1

DSRel

...

Pipes can branchprobabilistically

↓

↓

↓

↓

Hasuo (NII, JP)Branching Monad: Source ofParticle-Style GoI Situations
Thm. ([Jacobs,CMCS10])
Given a “branching monad” T on Sets, themonoidal category

Monads in[Hasuo,Jacobs&Sokolova07]
Kl(T) is Cpo⊥enriched(K`(T ), +, 0)is• aunique decomposition[Haghverdi,PhD00], hence iscategory• a traced symmetric monoidal category.
Cor.
(K`(T ), +, 0), N ·, N is a GoI situation.

Particle-style: trace via
the execution formulatr(f ) =
fXY t

a

n2N

fZY

(fZZ )nfXZ!

Hasuo (NII, JP)

The Categorical GoI Workflow
Branching monad B
Coalgebraic trace semantics

Traced monoidal category C+ other constructs ➜ “GoI situation” [AHS02]

Fancy
monad
Fancy
TSMC

Categorical GoI [AHS02]

Linear combinatory algebra

Fancy
LCA

Realizability

Linear category

Model of fancy
language

Hasuo (NII, JP)Model for (a variant of) the
Selinger-Valiron
quantum λ-calculus

The Categorical GoI Workflow(linear λ + prep./Unitary/meas.)[Hasuo & Hoshino, LICS’11 & APAL’16]

Branching monad B

via theCoalgebraic
quantum branchingmonad
trace semantics... with considerable complication :(TracedCR
J ` M :monoidal⌧ K : J K !category(J⌧ K ( R) (+ other constructsp ➜ •“GoIq situation” [AHS02]
where
"
"
R=

⇢

0

• q

•
..
.

•
..
.

1

• q

•
..
.

•
..
.

p
p
q 2 [0, 1]
Categorical
GoIp ,[AHS02]
0

1

↵

Fancy
monad
Records measurement
outcomes

Fancy
R as a suitable final
TSMCin thecoalgebra

realizability category↵

Linear combinatory algebra

Fancy
LCA

Realizability

Linear category

Model of fancy
language

Hasuo (NII, JP)Challenge: Memorizing Effects
Already w/
nondeterminism!

...

Challenge: Memorizing Effects...

J x. x + xK
...

...

J( x. x + x)(3 t 5)K

Already w/
nondeterminism!

...

J3 t 5K(...x. x + x)(3 t 5)

!CBV 6 or 10 ??

➜ • Query ( x. x + x)(3 t 5)
➜ • Query x➜ • Answer 3 or 5
➜ • Query x➜ • Answer 3 or 5
➜ • Answer 3 + 3, 3 + 5, 5 + 3 or 5 + 5

The GoI Animation
JM K = ( NN, a partial function )= “piping”

↓

↓

↓

↓

0

1

2

3

...

(countably many)

[|M|]

...
↓

↓

↓

↓

Hasuo (NII, JP)An Idea
Let a traversing token rearrange piping!

Hasuo (NII, JP)

Memoryful GoI

Let a traversing token rearrange piping!
PythagoraSwitch, NHK Education(Created by (another) Masahiko Sato)

Hasuo (NII, JP)Outline
Coalgebra meets higher-order computationin Geometry of Interaction [Girard, LC’88]
GoI w/“GoI Animation”

T-branchingÏÏ f : N ! TNf

[IH & Hoshino, LICS’11]

x2X

f

Ï

Ï

f: X ⇥N !
T (X ⇥ N)

Memoryful GoI

Categorical GoI[Abramsky, Haghverdi & Scott, MSCS’02][Hoshino, Muroya & IH,
CSL-LICS’14 & POPL’16]

Hasuo (NII, JP)

Memoryful GoI
Equip piping withinternal states, or memorynotJ3 t 5K : N! PN ,sq 7 ! {3, 5}

but a transducer (Mealy machine)
J3 t 5K : X ⇥ N! P(X ⇥ N) ,

q/3

o
s
l
8

q/3

✏ q/5
/ sr
s0
g

q/5

Not a new idea:
Slices in GoI for additives [Laurent, TLCA’01]
Resumption GoI [Abramsky, CONCUR’96]
Hasuo (NII, JP)

Memoryful GoI
We introduce memory in a structured manner...
➜the “traced monoidal category” of transducers
Trans(T )Objects: sets A, B, . . .
Arrows:Ac! B in Trans(T )X, X ⇥ A ! T (X ⇥ B), x0 2 X , T -transducer

with operations
likeA(X,c,x)B(Y,d,y)C

composition ◦

C

A

C

A

(X,c,x)(Y,d,y)(X,c,x)B

DB

tensor ⊗C

trace
Hasuo (NII, JP)Trans(T) by Coalgebraic
Component Calculus[Barbosa ’03][IH & Jacobs ’11]

Trans(T )Objects: sets A, B, . . .
Arrows:Ac! B in Trans(T )X, X ⇥ A ! T (X ⇥ B), x0 2 X , T -transducerAC(X,c,x)

A

C

A

B

(X,c,x)(Y,d,y)(X,c,x)(Y,d,y)

B

D

B

C

tensor ⊗composition ◦
0

B
B
B
B
B
B
B
B
BX ⇥ Y,
B
B
B
B
B
B
@

(X ⇥ Y ) ⇥ A⇠=! (X ⇥ A) ⇥ Y

trace
1

C
C
! T (X ⇥ B) ⇥ Y
C
C
str0
C
! T (X ⇥ B) ⇥ Y
C⇠=C! T X ⇥ (Y ⇥ B)
C
,
(x,
y)
C
T (X⇥d)C! T X ⇥ T (Y ⇥ C)
C
C
T str
C
! T T X ⇥ (Y ⇥ C)C
µTC
! T X ⇥ (Y ⇥ C)A⇠=
! T (X ⇥ Y ) ⇥ C
c⇥YC

Hasuo (NII, JP)Trans(T) by Coalgebraic
Component Calculus[Barbosa ’03][IH & Jacobs ’11]

Trans(T )Objects: sets A, B, . . .
Arrows:Ac! B in Trans(T )X, X ⇥ A ! T (X ⇥ B), x0 2 X , T -transducerAC(X,c,x)

A

C

A

B

(X,c,x)(Y,d,y)(X,c,x)(Y,d,y)

B

D

B

C

tensorFix: quotient modulo
behavioral equivalenceAA(X,c,x)(X,c,x)B(Y,d,y)C(Z,e,z)
D

⇠
=
6
=

( )

Trans(T) is a“category”...

trace

( )

composition

C

B(Y,d,y)C(Z,e,z)D(homomorphisms of T-transducers) ➜ resumptions [Abramsky]
Hasuo (NII, JP)

The Memoryful GoI Framework• Exception 1 + E + ( )Given:– with 0-ary opr. raisee (e 2 E)

a monad T on Sets,
s.t. Kl(T) is Cppo-enriched• Nondeterminism P– with binary opr. t• Probability D, where

DX = {d : X ! [0, 1] |Px d(x)  1}

– with binary opr. tp (p 2 [0, 1])

an alg. signature Σ withalgebraic operations on T

• Global state (1 + S ⇥)S– with |V |-ary lookupl and unary updatel,v[Plotkin & Power]

For the calculus: λc + (alg. opr. from Σ) + (co)products + arith.
We give

| |

N
N

L

N

...

N

...

N

` M: ⌧ M

Nin Trans(T)Hasuo (NII, JP)Interpretation

Recursion:asusualComponentimplemented
Calculusfor
Recursion
J K : E↵Val! T (N)⌃N

Girard(Adequacy)style
MackieTheorem(exploiting freeconti. styleΣ-alg.)
fixed point operator
fixed point operator

Let ` M : nat. Then, as elem. of T (N),
N×A

A

A
N×A

c
A

c
N×A

c

N
L c` M. .:. nat M
N

!†

∗
e˜′ A

r

N×A

=

∗
c˜′ A

N×A

d̃∗
A

N×N×A

|M
c |

N×A

c̃∗
A

N×A

z

.

N×N×A

∗
d˜′ A

ẽ∗
A

Opr. sem.:
Plotkin-Powereffect-value.
E.g.
Finitary
string diagram
A

feeding a queryand observing
Obviously a fixed
point
the
outcomeFixed-point induction

N×A

3 t (5 t div)

t
=

t

3

Theorem The two coincide.
15 (for any suitable T!)
Muroya (U. Tokyo)
5?

Hasuo (NII, JP)Our Tool TtT

Develo pe d by Koko Muroyahttp://koko-m.github.io/TtT/

Hasuo (NII, JP)Summary
Coalgebra meets higher-order computationin Geometry of Interaction [Girard, LC’88]
GoI w/“GoI Animation”

T-branchingÏÏ f : N ! TNf

[IH & Hoshino, LICS’11]

x2X

f

Ï

Ï

f: X ⇥N !
T (X ⇥ N)

Memoryful GoI

Categorical GoI[Abramsky, Haghverdi & Scott, MSCS’02][Hoshino, Muroya & IH,
CSL-LICS’14 & POPL’16]

Hasuo (NII, JP)Abstraction in a Theory:“Categorical Transfer”
Categorical Geometry of Interaction[Abramsky, Haghverdi, Scott]✓Defn.

T (e) =

theory of coalgebrasin K`(Be )◆, where Be is a monad

Coalgebra
Abstract TechniqueThm. Coalgebraic proof methods (such as (bi)simulations) are v
A

T[_]
Identify“mathematicalessense”

Chooseparameter e1

T1 = T[e1]Geometry of Interaction[Girard]true | false | A1 ^ A2 | ¬A | a1 < a2 |8x 2 ⇤N. A | 8x 2 ⇤R. A[Jacobs,
Rutten, …]
By the following characterizations in K`(B ).
e

FX
O
c
X

F behc /

F OZ
final
/Z

behc
system behavior

Existing Technique
Automata,
Mealy machines, …

Proof.

::=

FX
O
c
X

Ff
w

/ FY
O
d
/Y

f
simulation

Chooseparameter e2
Novel TechniqueT[e2]
GoI with nondeterministic, probabilistic,
quantum, and other effects… ➜ Memoryful
Geometry of Interaction [Hoshino, Muroya, Hasuo, …]
54

Retracing some paths in Process Algebra
Samson Abramsky
Laboratory for the Foundations of Computer Science
University of Edinburgh

1Introduction

The very existence of the concur conference bears witness to the fact that“concurrency theory” has developed into a subject unto itself, with substantially diﬀerent emphases and techniques to those prominent elsewhere in thesemantics of computation.
Whatever the past merits of this separate development, it seems timely
to look for some convergence and unification. In addressing these issues, I
have found it instructive to trace some of the received ideas in concurrency
back to their origins in the early 1970’s. In particular, I want to focus ona seminal paper by Robin Milner [Mil75]1 , which led in a fairly direct line
to his enormously influential work on ccs [Mil80, Mil89]. I will take (to theextreme) the liberty of of applying hindsight, and show how some diﬀerent
paths could have been taken, which, it can be argued, lead to a more unified
approach to the semantics of computation, and moreover one which may
be better suited to modelling today’s concurrent, object-oriented languages,
and the type systems and logics required to support such languages.

Such unification
had been alreadysuggested by
Samson!

Ï2

The semantic universe: transducers

Milner’s starting point was the classical automata-theoretic notion of transducers, i.e. structures(Q, X, Y, q0 , δ)

CONCUR’96
Hasuo (NII, JP)Hasuo (NII, JP)Outline
Abstraction in a Theory I
Categorical GoI (geometry of interaction)[Abramsky, Haghverdi & Scott, MSCS’02] [Hasuo & Hoshino, LICS’11] [Hoshino, Muroya & Hasuo, CSL-LICS’14][Muroya, Hoshino & Hasuo, POPL’16] [Hasuo & Hoshino, APAL’17]

Abstraction in a Theory II
Codensity Bisimulation Games[Katsumata & Sato, CALCO’15] [Sprunger, Katsumata, Dubut & Hasuo, CMCS’18][Komorida, Katsumata, Hu, Klin & Hasuo, submitted (soon on arXiv)]

Abstraction in a ProjectIntroducing ERATO MMSD Project:from categorical foundations to automated driving

Abstraction in an Inspiring Mind
57

Hasuo (NII, Tokyo)

Abstraction in a Theory II
Codensity Bisimulation Games[Katsumata & Sato, CALCO’15] [Sprunger, Katsumata, Dubut & Hasuo, CMCS’18][Komorida, Katsumata, Hu, Klin & Hasuo, submitted (soon on arXiv)]
58

Hasuo (NII, Tokyo)

“Categorical Transfer”
Codensity bisimilarity
in a ﬁbration

Coalgebra[Jacobs, Rutten, …]

Defn.

Codensity
games✓

T (e) =

theory of coalgebrasin K`(Be )◆, where Be is a monad

Abstract TechniqueThm. Coalgebraic proof methods (such as (bi)simulations) are v
A

T[_]
Identify“mathematicalessense”
Automata,
Mealy Existingmachines, …Technique

Proof.

::=

true | false | A1 ^ A2 | ¬A | a1 < a2 |8x 2 ⇤N. A | 8x 2 ⇤R. A

By the following characterizations in K`(Be ).
FX
O
c
X

F behc /

F OZ
final
/Z

behc
system behavior

Chooseparameter e1

FX
O
c
X

Ff
w

/ FY
O
d
/Y

f
simulation

Chooseparameter e2
Novel Technique

T1 = T[e1]T[e2]Games for bisimulation
metric, topology, …

Bisimulation
games
59

LaTeX slides

60

Hasuo (NII, Tokyo)

“Categorical Transfer”
Codensity bisimilarity
in a ﬁbration

Coalgebra[Jacobs, Rutten, …]

Defn.

Codensity
games✓

T (e) =

theory of coalgebrasin K`(Be )◆, where Be is a monad

Abstract TechniqueThm. Coalgebraic proof methods (such as (bi)simulations) are v
A

T[_]
Identify“mathematicalessense”
Automata,
Mealy Existingmachines, …Technique

Proof.

::=

true | false | A1 ^ A2 | ¬A | a1 < a2 |8x 2 ⇤N. A | 8x 2 ⇤R. A

By the following characterizations in K`(Be ).
FX
O
c
X

F behc /

F OZ
final
/Z

behc
system behavior

Chooseparameter e1

FX
O
c
X

Ff
w

/ FY
O
d
/Y

f
simulation

Chooseparameter e2
Novel Technique

T1 = T[e1]T[e2]Games for bisimulation
metric, topology, …

Bisimulation
games
61

Perspectives
Games ➜ algorithms
Infinite state?
➜ CEGAR, template-based symbolic presentation, …
The roles of observations and indistinguishability inbisimulation notions, formalized
relational
metrictopological ➜ domain theory!
open = observable
continuous = computable
62

Hasuo (NII, Tokyo)

Outline
Abstraction in a Theory I
Categorical GoI (geometry of interaction)[Abramsky, Haghverdi & Scott, MSCS’02] [Hasuo & Hoshino, LICS’11] [Hoshino, Muroya & Hasuo, CSL-LICS’14][Muroya, Hoshino & Hasuo, POPL’16] [Hasuo & Hoshino, APAL’17]

Abstraction in a Theory II
Codensity Bisimulation Games[Katsumata & Sato, CALCO’15] [Sprunger, Katsumata, Dubut & Hasuo, CMCS’18][Komorida, Katsumata, Hu, Klin & Hasuo, submitted (soon on arXiv)]

Abstraction in a ProjectIntroducing ERATO MMSD Project:from categorical foundations to automated driving

Abstraction in an Inspiring Mind
63

Hasuo (NII, Tokyo)

The Power of Abstraction
in atheoryin aproject

… and
in an
inspiring mind
64

Hasuo (NII, Tokyo)

Outline
Abstraction in a Theory I
Categorical GoI (geometry of interaction)[Abramsky, Haghverdi & Scott, MSCS’02] [Hasuo & Hoshino, LICS’11] [Hoshino, Muroya & Hasuo, CSL-LICS’14][Muroya, Hoshino & Hasuo, POPL’16] [Hasuo & Hoshino, APAL’17]

Abstraction in a Theory II
Codensity Bisimulation Games[Katsumata & Sato, CALCO’15] [Sprunger, Katsumata, Dubut & Hasuo, CMCS’18][Komorida, Katsumata, Hu, Klin & Hasuo, submitted (soon on arXiv)]

Abstraction in a ProjectIntroducing ERATO MMSD Project:from categorical foundations to automated driving

Abstraction in an Inspiring Mind
65

Hasuo (NII, Tokyo)

On ERATO MMSDJST ERATO Project, 2016/10-2022/03.
Several faculty members,
15+ researchers, 20+ students, 6 sites
Our goal:formal methods for cyber-physical systems (CPS)
Extend formal methods, from software to CPS
Safety, reliability, V&V (Verification & Validation).
“Check if a system behaves as expected”

The Autonomoose Project,
U Waterloo

Automated driving as a strategic target domain.
Collaboration with U Waterloo: www.autonomoose.net
Our principle: broaden the realm of CPS research
Theory:abstract mathematical metatheory➜ scale out to diverse applications

CPS
research

Practice: real-world systems (not only toy examples)66

Hasuo (NII, Tokyo)

Cyber-Physical Systems:
Control Theory and Formal Methods/Software Science
Cyber-Physical System (CPS)“A mechanism that is controlled or monitored by computer-based algorithms,
tightly integrated with the Internet and its users” (Wikipedia)
Physical plant (continuous) + Digital control (discrete)
In US: NSF Key Area of Research (2006-)
Formal methods: Logical proofs for “correctness” of (discrete) programs
Model checking [Pnueli, Clarke, Emerson, Sifakis, …]Theorem Proving (Coq, Agda, …) [Milner, Coquand, Leroy, Voevodsky, …]
Control Theory: Analysis of continuous dynamics
Stability, Lyapunov function, …
Their similarity is widely recognizede.g. HSCC, one of the main conferences ofannual CPS Week
67

CPS Research, So Far(the V&V Aspect)
CPS(esp. hybrid systems)
Analysis⇤(p ) ⌃q)<latexit sha1_base64="hv19xxln5Ihgt0PDz00mX3beYGs=">AAACF3icbZC7TsMwFIadcivlVmCEwaJCKkuVICQYq8LAWBC9SE1UOY7TWnXsYDtAFXXhLXgDVngBNsTKyM6D4LYZoOVIln79/znH9ufHjCpt219WbmFxaXklv1pYW9/Y3Cpu7zSVSCQmDSyYkG0fKcIoJw1NNSPtWBIU+Yy0/MH5OG/dEamo4Dd6GBMvQj1OQ4qRNla3uO/WxEM5dq9pr6+RlOLevaAoEjyAt0fdYsmu2JOC88LJRAlkVe8Wv91A4CQiXGOGlOo4dqy9FElNMSOjgpsoEiM8QD3SMZKjiCgvnfxiBA+NE8BQSHO4hhP390SKIqWGkW86I6T7ajYbm/9lnUSHZ15KeZxowvH0ojBhUAs4RgIDKgnWbGgEwpKat0LcRxJhbcAV3PHCDGHqCxaMDBZnFsK8aB5XHLviXJ2UqrUMUB7sgQNQBg44BVVwCeqgATB4BM/gBbxaT9ab9W59TFtzVjazC/6U9fkDl7ugSA==</latexit>

FormalMethods

Col

Control
Theorylabo

x0 = f (x, u)<latexit sha1_base64="OLHwdpyatx3yKIFqo/K47yv4v90=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDIjgm6EohuXFexD2qFk0kwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy09cCFwzn3JveeIGJUG9f9cnJLyyura/n1wsbm1vZOcXevoWWsMKljyaRqBUgTRgWpG2oYaUWKIB4w0gyGN6nffCRKUynuzTgiPkd9QUOKkbHSw+j4KiyPTuOTbrHkVtwp4CLxMlICGWrd4nenJ3HMiTCYIa3bnhsZP0HKUMzIpNCJNYkQHqI+aVsqECfaT6YLT+CRVXowlMqWMHCq/p5IENd6zAPbyZEZ6HkvFf/z2rEJL/2Eiig2RODZR2HMoJEwvR72qCLYsLElCCtqd4V4gBTCxmZU6KQPZmklgWS9iY3Fmw9hkTTOKp5b8e7OS9XrLKA8OACHoAw8cAGq4BbUQB1gwMEzeAGvzpPz5rw7H7PWnJPN7IM/cD5/AH9Ul5E=</latexit>
sha1_base64="4LCzMseb0W4aHc9jzDSRRbHgPjA=">AAAB63icbZC7TsMwGIX/lFsJBcrMYlEhMVUJC4xILIxFoheprSrHcVqrjh3Zf5BK1Bdg5QXYEI/EzoPgtBmg5UiWjs7x5fcXZVJYDIIvr7azu7d/UD/0jxr+8clps9GzOjeMd5mW2gwiarkUindRoOSDzHCaRpL3o/l92fefubFCqydcZHyc0qkSiWAUXdSZNFtBO1iJbJuwMi2oNGl+j2LN8pQrZJJaOwyDDMcFNSiY5Et/lFueUTanUz50VtGU23GxGnNJLl0Sk0QbtxSSVfr7REFTaxdp5HamFGd2syvD/7phjsntuBAqy5Ertn4oySVBTco/k1gYzlAunKHMCDcrYTNqKENHxh+VF1aMikjLeOmohJsMtk3vuh0G7fAxgDqcwwVcQQg3cAcP0IEuMIjhFd68F+/d+1jTq3kVxjP4I+/zB6n+kjc=</latexit>
sha1_base64="wdgUGz0/4fuZ88hKGlj8zgUTtXk=">AAAB93icbZDLSgMxGIX/qbdaq1a3boJFrCBlxo1uBMGNywr2Iu1QMmmmDU0yQ5KRlqE738CtvoA78Wnc+yBm2llo64HA4Zxc/nxBzJk2rvvlFNbWNza3itulnfLu3n7loNzSUaIIbZKIR6oTYE05k7RpmOG0EyuKRcBpOxjfZn37iSrNIvlgpjH1BR5KFjKCjY0eJ6fXYW1ynpz1K1W37s6FVo2XmyrkavQr371BRBJBpSEca9313Nj4KVaGEU5npV6iaYzJGA9p11qJBdV+Oh94hk5sMkBhpOySBs3T3ydSLLSeisDuFNiM9HKXhf913cSEV37KZJwYKsnioTDhyEQo+z0aMEWJ4VNrMFHMzorICCtMjGVU6mUX5rTSIOKDmcXiLUNYNa2LuufWvXsXinAEx1ADDy7hBu6gAU0gIOAFXuHNeXbenY8FwIKTkzyEP3I+fwD4XJYk</latexit>
sha1_base64="Hx+nB8T5F5UCLoxoqCIXEBH+afA=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDLjRjdC0Y3LCvYh7VAymUwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy0euDC4Zx7k3tPEDOqjet+OoWl5ZXVteJ6aWNza3unvLvX0jJRmDSxZFJ1AqQJo4I0DTWMdGJFEA8YaQej68xvPxClqRR3ZhITn6OBoBHFyFjpfnx8GVXHp8lJv1xxa+4M8C/xclIBORr98lcvlDjhRBjMkNZdz42NnyJlKGZkWuolmsQIj9CAdC0ViBPtp7OFp/DIKiGMpLIlDJypPydSxLWe8MB2cmSGetHLxP+8bmKiCz+lIk4MEXj+UZQwaCTMrochVQQbNrEEYUXtrhAPkULY2IxKvezBPK00kCyc2li8xRD+ktZZzXNr3q1bqV/lARXBATgEVeCBc1AHN6ABmgADDp7AM3hxHp1X5815n7cWnHxmH/yC8/ENfhSXjQ==</latexit>

rati
on

Challenge: scalability, esp. for real-world CPSs
Require complete understanding of a white-box model
Insist on being absolutely sound and correct
Little tolerance to uncertainty and noise➜ don’t get along with statistical machine learning

68

CPS Research:
Our Comprehensive Approach
Control Theory

Mathematical
Metatheory

Formal Methods

Statistical
MachineLearning

SoftwareEngineering69

70

Logic, esp. model theoryDefn.

T (e) =✓

theory of coalgebrasin K`(Be )◆, where Be is a monad

Abstract TechniqueThm. Coalgebraic proof methods (such as (bi)simulations) are v
A

T[_]

Proof.

Discrete dynamics

FX
O
c
X

T1 = T[e1]F behc /

F OZ
final
/Z

behc
system behavior

FX
O
c
X

Continuous dynamics

w

/ FY
O
d
/Y

f
simulation

Novel TechniqueT[e]2Probabilistic simulation

Example 1: Coalgebraic Unfolding[Hasuo, Urabe, Shimizu et al.]Example 2: Nonstandard Transfer[Suenaga, Hasuo, Sekine, Kido71
et al.]

Ff

Chooseparameter e2

Chooseparameter e1

Existing Technique

Boolean simulation

true | false | A1 ^ A2 | ¬A | a1 < a2 |8x 2 ⇤N. A | 8x 2 ⇤R. A

By the following characterizations in K`(Be ).

Categorical simulation

Identify“mathematicalessense”::=

Our Organization
International and multi-disciplinary. “creative chaos”
Group 0 @ NII:
Metatheoretical Integration
Leader: Shin-ya Katsumata

Kyoto U RIMS Site:
Categorical
Infrastructure
Leader:Masahito Hasegawa

Topics:Programming
Languages,
Formal Semantics,
Categorical Models,Mathematical
Logic, …

Kyushu U Site:
Optimization for
CPS V&V
Leader:Hayato Waki

Group 3 @ NII:
Formal Methods andIntelligence
Leader: Fuyuki Ishikawa
Topics:SoftwareEngineering,Formal Modeling,
Testing, Safe &Explainable AI

Group 2 @ U Waterloo:
Formal Methods in Industry
Leader: Krzysztof Czarnecki

Osaka U Site:
Control Theory for
CPS
Leader:Toshimitsu Ushio

Group 1 @ NII:
Heterogeneous Formal Methods
Leader: Ichiro Hasuo
Topics:Automata Theory,
Formal Verification,
Proof Assistants,
Automated
Deduction,
Runtime Verification

Topics:Automated
Driving, Software
Engineering,
Machine Learning

Hasuo (NII, Tokyo)

Our Categorical Team:ERATO MMSD Group 0
Shin-ya Katsumata (Group Leader, PhD (Edinburgh)):fibration, lambda-calculus, categorical semantics, monoidal category,
programming language, program verification

Group 0 @ NII:
Metatheoretical Integration
Leader: Shin-ya Katsumata
Topics:Programming
Languages,
Formal Semantics,
Categorical Models,Mathematical
Logic, …

Jérémy Dubut (PhD (ENS Paris Saclay, 2017)):
concurrency, directed topology, topos theory, coalgebra, verification, hybrid system
David Sprunger (PhD (Indiana, 2017)):
coalgebra, monoidal category, categorical logic, fibration, machine learning
Clovis Eberhart (PhD (U Savoie Mont Blanc, 2018)):
game semantics, nominal set, verification, machine learning
Kenta Cho (PhD expected (Nijmegen)):categorical logic, quantum mechanics & logic, verification, machine learning
Soichiro Fujii (PhD confirmed (Tokyo)):Lawvery theory, higher-dimensional category, algebraic eﬀect
Natsuki Urabe (PhD confirmed (Tokyo)):coalgebra, concurrency, model checking, game, verification, probabilistic systems
Yuichi Komorida (PhD student (NII/Sokendai)):fibration, coalgebra, game… and at Kyoto Site (Masahito “Hassei” Hasegawa, Naohiko Hoshino, Koko Muroya, and more)
73

Hasuo (NII, Tokyo)

Group 2

F

Cyber-Physical Systems,
esp. Safety ofAutomated Driving

Group 1
D

Statistical ML/AI

Group 3

B

Software Science
Formal Verification
ProgrammingC
Control
TheoryLanguages

PJ
StatusGroup 0E✓

theory of coalgebrasin K`(Be )◆SoftwareEngineeringDefn.

T (e) =

Thm.

Coalgebraic proof methods (such as (bi)simulations) are valid in T (e) too.

Proof.

By the following characterizations in K`(Be ).

A(Meta-)Theoretical 74
Foundation

FX
O
c
X

F behc /

F OZ
final
/Z

behc
system behavior, where Be is a monad suited for e

FX
O
c
X

Ff
w

/ FY
O
d
/Y

f
simulation

Group 2

F

Safetyarchitecture

Kolcak+submitted

Group 1

Waga+
Submitted

Cyber-Physical Systems,
esp. Safety ofAutomated Driving

Andre+ICECCS’18

Zhang+
Submitted

Hasuo+
Submitted

Andre+TACAS’19

Okudono+Submitted
D’Argenio+
FoSSaCS’18

B

Avanzini+
FLOPS’18

Group 0

Arcaini+
ECSA’18

Sprunger+
Submitted
Eberhart+
Submitted
Takisaka+
ATVA’18
Categorical
Event-B

Wissmann+
FpSSaCS’19

PJ
StatusGroup 3

Arcaini+
ICSA’18

E

Divason+
ITP’18

Katsumata
FoSSaCS’18

Statistical ML/AI

Budde+TACAS’18

Kura+
TACAS’19

Komorida+
Submitted

Ishikawa
ER’18

Safe learning

Software Science
Formal Verification
ProgrammingC
Control
TheoryLanguages
Miyazaki+
POPL’19D

Submitted

Ongoing

DSL fortestingZhang+EMSOFT’18

Waga+
EMSOFT’18

Published

Dubut
FpSSaCS’19

A(Meta-)Theoretical 75
Foundation

SoftwareEngineeringGroup 2
Next Step 3:
Automotive appl.
with visibilityGroup 1F

Safetyarchitecture

Kolcak+submitted

Waga+
Submitted

Cyber-Physical Systems,
esp. Safety ofAutomated Driving

Andre+ICECCS’18

Zhang+
Submitted

Hasuo+
Submitted

Andre+TACAS’19

Okudono+Submitted
D’Argenio+
FoSSaCS’18

B

Avanzini+
FLOPS’18

Group 0

Arcaini+
ECSA’18

Sprunger+
Submitted

SoftwareEngineering

Eberhart+
Submitted
Takisaka+
ATVA’18
Categorical
Event-B

Wissmann+
FpSSaCS’19

PJ
StatusGroup 3

Arcaini+
ICSA’18

E

Divason+
ITP’18

Katsumata
FoSSaCS’18

Statistical ML/AI

Next Step 2:
Further Advances
to ML/AI

Budde+TACAS’18

Kura+
TACAS’19

Komorida+
Submitted

Ishikawa
ER’18

Safe learning

Software Science
Formal Verification
ProgrammingC
Control
TheoryLanguages
Miyazaki+
POPL’19D

Submitted

Ongoing

DSL fortestingZhang+EMSOFT’18

Waga+
EMSOFT’18

Published

Dubut
FpSSaCS’19

A(Meta-)Theoretical 76
Foundation

Next Step 1:
From SS, CT, TF to
Software EngineeringOutline
Abstraction in a Theory I
Categorical GoI (geometry of interaction)[Abramsky, Haghverdi & Scott, MSCS’02] [Hasuo & Hoshino, LICS’11] [Hoshino, Muroya & Hasuo, CSL-LICS’14][Muroya, Hoshino & Hasuo, POPL’16] [Hasuo & Hoshino, APAL’17]

Abstraction in a Theory II
Codensity Bisimulation Games[Katsumata & Sato, CALCO’15] [Sprunger, Katsumata, Dubut & Hasuo, CMCS’18][Komorida, Katsumata, Hu, Klin & Hasuo, submitted (soon on arXiv)]

Abstraction in a ProjectIntroducing ERATO MMSD Project:from categorical foundations to automated driving

Abstraction in an Inspiring Mind
77

Hasuo (NII, Tokyo)

??

λ-calculus
concurrency

??
??

game
domaintheory semantics
bisimulation

databasequantummechanics

contextuality

Chu spaces

economics
78

Hasuo (NII, Tokyo)

The Power of Abstraction
To come any close
to an
inspiring mind…

individual eﬀorts… and our collective eﬀort
79

Hasuo (NII, Tokyo)