seminaire PPS - 26 (oui 26!!) Fevrier

Desolee... petit erreur de date!!
Donc:

Matthieu Sozeau (LRI, Orsay)
le Jeudi 26 Février, 11h, salle 0C2:

"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.

seminaire PPS - 19 Fevrier

Chers tous,
le prochaine seminaire PPS est donne' par

Matthieu Sozeau (LRI, Orsay)
le Jeudi 19 Février, 11h, salle 0C2:

"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.

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.
>

seminaire PPS - 19 Fevrier

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.