Send the link below via email or IMCopy
Present to your audienceStart 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.
Make your likes visible on Facebook?
You can change this under Settings & Account at any time.
Transcript of Group MMM
Mathematical and Metamathematical Modeling
Dept. Computer Science, the University of Tokyo
Category Theory (and Algebra)
A modern math. language, with
Reveals the "same structure" obscured by set-theoretic explicit descriptions
how an entity is constructed
how it relates to others
, described mathematically and syntactically
Computer Systems: Correctness
Everywhere, important roles... but buggy
(Manual) theorem proving
(Coq, Agda, PVS, ...);
automatic theorem proving
Computer Systems: Emerging Concerns
Pervasiveness ==> new concerns
Quality of service
"Correct? Yes/No" ==> "How often?", "at what cost?", ...
extract essence w/
P = P_
P = P_
new computation paradigms
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]
Nonstandard analysis and theorem proving [ICALP 2011] [CAV 2012] [POPL 2013]
Program logic and input synthesis [HAS 2014]
Coalgebraic simulation and matrices [CONCUR 2014]
Coinductive predicates [MFPS 2013]
Games and program logic [CMCS 2014]
Semantics of quantum lambda calculus [LICS 2011]
Quantum proof nets [ESOP 2014]
Group seminar 1/week
Topicwise seminars (lambda, hybrid, quantitative, quantum) 1/week
Regular: Kohei Suenaga, Naohiko Hoshino (Kyoto)
More from abroad, industry, ...
Summer seminar w/ CS Group, RIMS, Kyoto Univ.
Trips abroad (conferences, summer schools, ...)
Even more so, if we get
applications with impact
(and that makes our lives much easier...)
i.e. Work Hard, Play Harder!