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.

Next Seminar

A formal set-theoretical model of Coq and its application to strong normalization

Visit website for this news | Export event in iCalendar format

 Bruno  Barras
Date
Tuesday, March 28 2017 at 11:00AM
Place
Auditorium Daniel Chemla (Bât. Institut D'Alembert)
Speaker
Bruno Barras (LIX, Ecole Polytechnique)

I will describe the formalization in Coq of two crucial metatheoretical properties of the formalism of the Coq proof assistant: consistency and strong normalization (SN). While it is clear why we prove the consistency of a logical formalism, I will give a motivation for the SN property.

Of course, as Gödel showed, proving the consistency of a formalism in itself is only proving it is inconsistent. The usual way out is to make Coq stronger by adding axioms. In our case, we have extended Coq to make it as strong as intuitionistic set-theory with Grothendieck universes (an intuitionistic counterpart of inaccessible cardinals).

Then, I will sketch an intuitive translation from the Calculus of Inductive Constructions (the formalism of Coq) to set theory, and prove that this interpretation is sound. The difficult part is to interpret inductive types. As a reward, we derive the consistency of Coq relative to the set theory described above.

Using a slight variant of the set-theoretical interpretation, I will explain how to build a strong normalization model, which soundness implies the SN property. The remarkable feature of this model is that it is very modular: the complexity of inductive types have been broken into simpler principles.


Upcoming Seminars

Runtime Analysis of Randomized Algorithms: A Dijkstra Déjà Vu

Visit website for this news | Export event in iCalendar format

 Joost-Pieter   Katoen
Date
Wednesday, March 29 2017 at 10:00AM
Place
Salle de Conférence (Pavillon des Jardins)
Speaker
Joost-Pieter Katoen (RWTH Aachen)

Randomization is an important tool in algorithm design for obtaining efficient solutions; e.g., random pivot selection in quicksort lowers the expected runtime (ER) to O(n log n). Reasoning about the ER of randomized algorithms is subtle and full of nuances, as:

  • they may have diverging runs but have a finite ER;
  • they may almost surely terminate but have an infinite ER;
  • running two finite-ER algorithms in sequence may yield an infinite ER.

ER analysis of randomized algorithms is typically done using classical probability theory, mostly with arguments relying on random variable expectations or martingales. These analyses partially follow an ad-hoc reasoning and take non-trivial relationships between random variables for granted.

In this talk, I'll present a formal verification approach towards the ER analysis using a weakest-precondition approach à la Dijkstra. It allows e.g. to prove the positive almost-sure termination: does a program terminate with probability one in finite expected time? We show proof rules for loops prove the soundness w.r.t a simple operational mode and argue that our approach conservatively extends Nielson's approach for deterministic programs.


TBA

Visit website for this news | Export event in iCalendar format

 Sébastien  Bardin and Richard  Bonichon
Date
Tuesday, April 25 2017 at 11:00AM
Place
Salle de Conférence (Pavillon des Jardins)
Speaker
Sébastien Bardin and Richard Bonichon (CEA, Paris-Saclay)


TBA

Visit website for this news | Export event in iCalendar format

Date
Tuesday, June 13 2017 at 11:00AM
Place
Salle de Conférence (Pavillon des Jardins)
Speaker
Colin Riba (LIP, ENS Lyon)


TBA

Visit website for this news | Export event in iCalendar format

 Pablo  Arrighi
Date
Tuesday, June 20 2017 at 11:00AM
Place
Salle de Conférence (Pavillon des Jardins)
Speaker
Pablo Arrighi (LIF, Université Aix-Marseille)


About LSV

Agenda

Export agenda in iCalendar format | Past seminars

Tue, Mar 28
Wed, Mar 29
Tue, Apr 25
Tue, Jun 13
Tue, Jun 20

Past seminars