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.