만나보세요
Prezi AI.
새로운 프레젠테이션 도우미가 기다리고 있어요.
뎌욱 빠르게 컨텐츠를 다듬고, 보강하고, 편집하고, 원하는 이미지를 찾고, 시각자료를 편집하세요.
트렌드 검색
로딩중
Group MMM
34
스크립트
Our Philosophies
- Math is fun
- Even more so, if we get applications with impact
- (and that makes our lives much easier...)
Group MMM
Mathematical and Metamathematical Modeling
i.e. Work Hard, Play Harder!
Hasuo Laboratory
Dept. Computer Science, the University of Tokyo
http://www-mmm.is.s.u-tokyo.ac.jp
Our Strategy
Our Mission
abstract, generic
w/ parameter P
- Modern, abstract mathematics
Mathematical
abstract theory
Category Theory (and Algebra)
Logic
- A modern math. language, with arrows
- Reasoning, described mathematically and syntactically
- Emphasis on structure
- not how an entity is constructed
- but how it relates to others
- Metamathematics
- Reveals the "same structure" obscured by set-theoretic explicit descriptions
- Applied to computer science
Existing
concrete theory
Computer Systems: Emerging Concerns
Computer Systems: Correctness
- Everywhere, important roles... but buggy
- Pervasiveness ==> new concerns
- Formal verification
- providing a mathematical proof for correctness
- not testing
- Cyber-Physical Systems
- Digital control in physical environment
- i.e. (discrete) jump & (continuous) flow
New applications,
new concerns and
new computation paradigms
- (Manual) theorem proving (Coq, Agda, PVS, ...); automatic theorem proving (SMT, ...); model checking
- Quality of service (QoS), quantitative verification
- "Correct? Yes/No" ==> "How often?", "at what cost?", ...
Our Topics
Our Events
Quantum Programming
Lambda Calculus
Quantitative
Verification
Cyber-Physical
Systems
Semantics of Functional Programs
- Semantics of quantum lambda calculus [LICS 2011]
- Quantum proof nets [ESOP 2014]
- Coalgebraic simulation and matrices [CONCUR 2014]
- Coinductive predicates [MFPS 2013]
- Games and program logic [CMCS 2014]
- Nonstandard analysis and theorem proving [ICALP 2011] [CAV 2012] [POPL 2013]
- Program logic and input synthesis [HAS 2014]
- Geometry of Interaction (GoI) as a compilation technique [CSL-LICS 2014] [LOLA 2014]
- Linear logic, proof nets, GoI [CSL-LICS 2014]
Coalgebra
- 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, ...)
Nonstandard Analysis
Modal
Logic
Categorical Logic
Logic
Category Theory
Algebra
P = P_2
New
concrete theory
P = P_1
extract essence w/
"mathematical eyes"
템플릿을 선택하세요
전 세계에 있는 프레젠테이션
프레지로 더욱 인상깊고 역동적인 프레젠테이션을 만들어 보세요