International Conference on
Rewriting, Deduction, and Programming
June 29 to July 3, 2015
Warsaw, Poland


PhD Open Lecture

Ugo Dal Lago

Is it possible to automatically evaluate the time complexity of any functional program? How far could one go, given the intrinsic limitations imposed by computability theory? Giving an answer to the questions above, even a partial one, would be beneficial in any context in which programs with too-high time complexity are harmful (or should simply ruled out from the game), like in security and cryptography. In this course, we will show how to the problems above can be approached by first characterizing relatively small time complexity classes by simple, paradigmatic programming languages, then turning the latter into formal methods. We will do that (at least) for term rewrite systems and the lambda-calculus.

Homotopy for Laymen

Krzysztof Ziemiański

Homotopy Type Theory is a very dynamically growing branch of the study within the type theory. Understanding its dynamics requires good knowledge of both type theory and topology. To bring the developments closer to a wider audience within community of people who study types, we propose a quick introduction to the basic notions of homotopy theory with necessary geometrical insights and suggestion of how combinatorial structures appearing in homotopy theory can be exploited for type theoretical considerations.

Coq for Algebraic Topologists

Jacek Chrząszcz

An important advantage of systems such as Coq is that they make it possible to manage complicated proof structures. As a result, it becomes possible to do reliable proofs for mathematical models that are bigger than so far employed. This is evidenced by successful developments of formal proofs for the Four Colour Theorem and Odd Order Theorem - both being theorems that brought many doubts about the correctness of the final argument. These doubts arised because those proofs were clearly on the verge of efficiency for traditional paper and pencil mathematical methods.

Currently, the mathematical models used in algebraic topology become more and more sophisticated, which creates potential to apply proof assistants in the field. A short course of Coq will be presented on the content that comes from the algebra to show the potential of Coq in analysis of algebraic models.

Important information

Plenary speakers

Valid XHTML 1.1 Valid CSS!