(配送されなかった可能性があります） 皆様、
INRIA Nantes の Pierre-Marie Pédrot が以下の講義を行う予定です。 定理証明支援系Coqの開発者の一人で、型理論の専門家です。
Jacques Garrigue
日時 11月28日(木) 10:30-12:00 / 13:00-14:30 場所 名古屋大学多元数理科学研究科 452号室(午前)・109号室(午後)
題名：Type Theories with a Side of Effects 話者：Pierre-Marie Pédrot (INRIA Nantes)
Abstract: Side-effects are a staple of real-world programming. Even Haskell, which boasts about its purity, allows non-terminating programs, which is a form of side-effects. On the other hand, dependent type theories constitute a family of type systems that can be considered among the most powerful and expressive ones. How come effectful dependent type theories are not more pervasive? In this talk, we will give a broad answer to this question, explaining the trade-offs at stake.