REPORT seminaire PPS du 19 Fevrier

Chers tous,
donne que jeudi c'est journée nationale de manifestations,
le seminaire du 19/2 par Matthieu Sozeau
est reporte à la semaine prochaine, le Jeudi 26 Février, salle 0C2, 11h.

claudia

> Bonjour,
> le prochaine seminaire PPS sera donné par
>
> Matthieu Sozeau (LRI, Orsay)
> le Jeudi 19 Février, salle 0C2:
>
> "Programming with Dependent Types in Coq"
> ------------------------------------------------
>
> 19/2 Matthieu Sozeau (LRI Orsay)
> Programming with Dependent Types in Coq
>
> Coq is a mature proof assistant based on a dependent type theory. However,
> while the use of dependent types is the very basis of all the proofs that
> are developed in the system, it still requires considerable expertise to
> tame their full power when programming. We present a solution to alleviate
> this problem as an additional layer on top of the core type theory that
> eases programming with strong specifications. We develop a new language
> inspired by PVS that allows to separate algorithmic and correctness
> concerns when developing programs with rich types, generating proof
> obligations on the side in a standard way. We also demonstrate the Program
> extension to Coq that implements this method on a non-trivial example:
> Finger Trees. We develop an indexed version of this data structure from
> which we can derive correct-by-construction priority queues or ropes. This
> development also illustrates a recently implemented type class extension
> to Coq.
>