报告题目：A syntactic approach to polynomial functors and opertopes

报告人：Pierre-Louis Curien 教授

主持人：张敏

报告时间：6月15日（周四）11:00—12:00

报告地点：中北校区数学馆201室

报告摘要：

Polynomial functors and opetopes are gadgets used in higher algebra for providing the definition of higher categories (which themselves are important for the foundations of (homotopy) type theory). Polynomial functors have been also independently discovered in computer science, under the name of containers (Abbott-Altenkirch-Ghani), in order to describe shape polymorphism of data structures. This talk will introduce these notions and offer a syntactic (and ``type-theoretic'') notation to describe them. This is research in progress, whose long-term ambition is to contribute to the formalization of higher structures (now pervasive in many areas of mathematics, where invariants, say of knots, are more and more sophisticated: numbers, polynomials, categories, 2-categories...) in proof assistants.

报告人简介：

Pierre-Louis Curien is a Senior Researcher at CNRS (a sort of equivalent to CAS). He entered the Ecole Normale Supérieure (ENS – a school with which ECNU has official relations). He got a PhD in Computer Science from University Paris 7 in 1979. He created the laboratory PPS (Proofs, Programs and Systems) at Paris 7 University, of which he was the director until 2009. He won the IBM France Computer Science Award in 1990.

He is head of the joint INRIA – University Paris Diderot – CNRS team. His research activities spread over the semantics of programming languages, proof theory, category theory, and more recently homotopical algebra. He is editor in chief of the journal Mathematical Structures in Computer Science. He co-organized the first thematic semester fostering Computer Science at the prestigious Institut Poincar/’e in 2014 (on the semantics of proof and programs). He is the author of around 60 research papers and has directed more than 20 PhD theses.