Latest Past Events

The finitary content of sunny nonexpansive retractions

Facultatea de Matematica si Informatica, sala 202

Andrei Sipoș (TU Darmstadt & IMAR). The goal of proof mining is to extract quantitative information out of proofs in mainstream mathematics which are not necessarily fully constructive. Often, such

Logical Foundations: Simple Imperative Programs

Facultatea de Matematica si Informatica, sala 202

Presenter: Traian Serbanuta. This week we continue exploring Coq based on the Logical Foundations volume of Software Foundations, chapter "IMP: Simple Imperative Programs"