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 Stéphane Le Roux and Matthias Fuegger.
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
- 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.