**Group MMM**

**Our Mission**

Modern, abstract

mathematics

**Mathematical and Metamathematical Modeling**

Hasuo Laboratory

Dept. Computer Science, the University of Tokyo

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

Applied to

computer science

Category Theory (and Algebra)

Logic

A modern math. language, with

arrows

Reveals the "same structure" obscured by set-theoretic explicit descriptions

Emphasis on

structure

not

how an entity is constructed

but

how it relates to others

Reasoning

, described mathematically and syntactically

Metamathematics

Computer Systems: Correctness

Everywhere, important roles... but buggy

(Manual) theorem proving

(Coq, Agda, PVS, ...);

automatic theorem proving

(SMT, ...);

model checking

Formal verification

providing a

mathematical proof

for correctness

not testing

Computer Systems: Emerging Concerns

Pervasiveness ==> new concerns

Quality of service

(QoS),

quantitative

verification

"Correct? Yes/No" ==> "How often?", "at what cost?", ...

Cyber-Physical Systems

Digital control

in

physical environment

i.e. (discrete)

jump

& (continuous)

flow

**Our Strategy**

Existing

concrete

theory

Mathematical

abstract

theory

New

concrete

theory

extract essence w/

"mathematical eyes"

abstract, generic

w/ parameter

P

P = P_

1

P = P_

2

New applications

,

new concerns

and

new computation paradigms

**Our Topics**

**Logic**

**Algebra**

**Category Theory**

Modal

Logic

Nonstandard Analysis

Categorical Logic

Coalgebra

Semantics of Functional Programs

Geometry of Interaction (GoI) as a compilation technique [CSL-LICS 2014] [LOLA 2014]

Linear logic, proof nets, GoI [CSL-LICS 2014]

Lambda Calculus

Nonstandard analysis and theorem proving [ICALP 2011] [CAV 2012] [POPL 2013]

Program logic and input synthesis [HAS 2014]

Cyber-Physical

Systems

Coalgebraic simulation and matrices [CONCUR 2014]

Coinductive predicates [MFPS 2013]

Games and program logic [CMCS 2014]

Quantitative

Verification

Semantics of quantum lambda calculus [LICS 2011]

Quantum proof nets [ESOP 2014]

Quantum Programming

**Our Events**

Seminars (almost)

every day

!

Group seminar 1/week

Topicwise seminars (lambda, hybrid, quantitative, quantum) 1/week

Guests

Regular: Kohei Suenaga, Naohiko Hoshino (Kyoto)

More from abroad, industry, ...

Summer seminar w/ CS Group, RIMS, Kyoto Univ.

Trips abroad (conferences, summer schools, ...)

Our Philosophies

Math

is fun

Even more so, if we get

applications with impact

(and that makes our lives much easier...)

i.e. Work Hard, Play Harder!