Title: Proofs and surfaces
Time： 10:00-11:30, December06 Friday,2019
Location:   Room 201, Mathematical Building 
Lecturer：Pierre-Louis Curien. 

Abstract:
Incidence theorems in Euclidean or projective geometry state that some incidences follow from other incidences, where a preincidence is a pair of a line and a point (or three points), and an incidence is a preincidence together with the information whether the point lies on the line or not.As remarked by Richter-Gebert, oriented closed surfaces given by triangular complexes give rise to such incidence results, in the form that  preincidences are attached to each triangle (they are called a Menelaus situation), and whenever all but one of these Menelaus situations hold (i.e.the preincidences are incidences), then so do the ones of the triangle left out.This gives rise to a logical system based on unilateral sequents with the intended meaning that each formula is implied by the remaining ones. It also gives rise to a cyclic operad (the notion will be explained in the talk),of which we give a presentation by generators and relations.  

Introduction of Lectuer:
Pierre-Louis Curien is Emeritus senior CNRS researcher at IRIF Laboratory (University Paris 7 and CNRS).He graduated from Ecole normale Supérieure (Paris), and received his PhD and « Thèse d’Etat » from University Paris 7 in 1979 and 1983, respectively. He received the IBM France prize in 1990. His research interests spread over computer science and mathematics, and cover the semantics of programming languages, category theory, ane more recently homotopical algebra. He was director or deputy-director of various research structures in France. He created the Inria joint team pi.r2 (whose research is build around the proof assistant Coq) in 2009 and headed it until his retirement in October 2019.