LSV Seminar

The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Laurent Doyen and Stefan Göller.

The seminar is open to public and does not require any form of registration.

Past Seminars

Building proof automations in dependently-typed languages to make Type-Driven Development come true

Visit website for this news | Export event in iCalendar format

 Franck Slama
Date
Tuesday, December 12 2017 at 11:00AM
Place
Salle de Conférence (Pavillon des Jardins)
Speaker
Franck Slama (University of St Andrews)

Proving program correctness is as old as programming, but we must admit that formal proofs and proof assistants is far from being part of day-to-day programming. Writing proof is a passion for us --logicians, mathematicians, and people into fundamental computer science-- but is not easily accessible to programmers. Indeed, the current standard in the industry is to not prove anything. Between these two extreme of proving every little property and not proving anything, some intermediate scenarios must be found. In this talk, I'll use the dependently-typed programming language Idris to advocate a way of programming with dependent types that brings some safety, which goes in the direction of Type-Driven Development (TDD). Unfortunately, this kind of programming with dependent types also brings some proof obligations, and TDD is therefore inaccessible to programmers without some proof automations. I'll show that dependent types can be used to easily build many proof automations, using a type-safe reflection mechanism, where reflected terms are indexed by the original Idris expression, which leads to straightforward construction and manipulation of proofs. The result is a hierarchy of reflexive tactics for proving equivalences in semi-groups, monoids, commutative monoids, groups, commutative groups, semi-rings and rings that helps programming with dependent types. This construction shows that dependent types can be of great value to address some of the problems they have caused.


About LSV

Agenda

Export agenda in iCalendar format | Past seminars

Tue, Dec 19
Tue, Jan 30

Past seminars