Events

Abstract: Coq is a very popular proof assistant, used in a variety of academic and industrial projects, for formalizing both computer science results as well as mathematical ones. Coq is based on a theoretically very clean model, the Calculus of Inductive Constructions, which allows to express all of mathematics in a constructive manner. Following the Curry-Howard correspondence, Coq is also a functional programming language. A logical proposition is a type, and a proof of the proposition is a well-typed program of that type.

In this 1-hour quick tutorial, we will give a very brief introduction to the basics of Coq and how it can be used to reason about languages. Starting from an elementary language of arithmetic expressions, we will build a compiler to a simple stack machine and prove it correct. We will also implement a simple program rewriting optimization and prove it correct. This toy example should give you a good idea of what Coq is about, and the joy (and pain!) of mechanized semantics.

About the speaker: Éric Tanter is a Full Professor of the Computer Science Department of the University of Chile. He received his PhD from both the University of Nantes and the University of Chile in 2004. His research interests cover programming languages and software engineering, ranging from the theoretical underpinnings of programming languages to the empirical study of the practice of programming. He has published many articles in, and is regularly involved in the program committees and editorial boards of, major conferences and journals in these areas. Recently, he has been mostly involved in the foundations and practice of gradual typing and verification.

Date: Friday, June 22 2018, from 12:00-13:00.

Venue: Auditorio Philippe Flajolet, Universidad de Chile, Beauchef 851, Santiago.