Loading presentation...

Present Remotely

Send the link below via email or IM

Copy

Present to your audience

Start remote presentation

  • Invited audience members will follow you as you navigate and present
  • People invited to a presentation do not need a Prezi account
  • This link expires 10 minutes after you close the presentation
  • A maximum of 30 users can follow your presentation
  • Learn more about this feature in our knowledge base article

Do you really want to delete this prezi?

Neither you, nor the coeditors you shared it with will be able to recover it again.

DeleteCancel

Group MMM

No description
by

Ichiro Hasuo

on 3 July 2014

Comments (0)

Please log in to add your comment.

Report abuse

Transcript of Group MMM

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!
Full transcript