POPL 2017
Sun 15 - Sat 21 January 2017
Sat 21 Jan 2017 14:00 - 15:00 at Auditorium - Midday Session Chair(s): Sandrine Blazy

Dealing with logical complexity in mathematics has a long tradition of building models for complex logics from models for simpler logics, using construction such as the sheaf construction. In computer science, there is a dual practice which consists in giving meaning to a complex language using a compilation phase into a simpler one.

In my presentation, I will show how the compilation phase approach also makes sens in logic, via the Curry-Howard isomorphism, and is more precise than the model extension approach because it takes computation into account. To illustrate this, I will show examples of program transformations in type theory, with applications to the Coq proof assistant.

Sat 21 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 15:30
Midday SessionCoqPL at Auditorium
Chair(s): Sandrine BlazyUniversity of Rennes 1, France
Invited Talk -- Managing Logical and Computational Complexity using Program Transformations
I: Nicolas TabareauInria, France
Session with the Coq Development Team