The Coq mailing list

[Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>]

[Désolé pour les copies multiples/Sorry for duplicate posts]

Bonjour à tous,

 j'ai le plaisir de vous inviter à la soutenance de ma thèse intitulée:

 « Un environnement pour la programmation avec types dépendants »

 La soutenance aura lieu salle 79 du LRI à Orsay le lundi 8 décembre à
10h30 (pour se rendre au LRI: http://www.lri.fr/srubrique.php?news=24)
et le jury sera composé de:

Mme Véronique Benzaken,        Professeur à l'université de Paris-Sud  
11 (examinatrice)
Mr  Thierry Coquand,           Professeur à l'université de Göteborg,  
Suède (rapporteur)
Mr  James McKinna,             Professeur à l'université de Nimègue,  
Pays-Bas (examinateur)
Mme Christine Paulin-Mohring,  Professeur à l'université de Paris-Sud  
11 (directrice de thèse)
Mr  François Pottier,          Directeur de recherche à l'INRIA  
Rocquencourt (rapporteur)
Mr  Philip Wadler,             Professeur à l'université d'Edimbourg,  
Écosse (examinateur)

 Vous êtes bien sûr conviés au traditionel pot qui suivra. Merci de  
m'indiquer
votre présence pour que l'on puisse s'organiser au mieux.

Résumé:

 Les systèmes basés sur la Théorie des Types prennent une importance
considérable tant pour la vérification de programmes qu'en tant
qu'outils permettant la preuve formelle de théorèmes mettant en jeu des
calculs complexes. Ces systèmes nécessitent aujourd'hui une grande
expertise pour être utilisés efficacement. Nous développons des
constructions de haut niveau permettant d'utiliser les langages basés
sur les théories des types dépendants aussi simplement que les langages
de programmation fonctionnels usuels, sans sacrifier pour autant la
richesse des constructions disponibles dans les premiers. Nous étudions
un nouveau langage permettant l'écriture de programmes certifiés en ne
donnant que leur squelette algorithmique et leur spécification. Le
typage dans ce système donne lieu à la génération automatique
d'obligations de preuve pouvant être résolues a posteriori. Nous
démontrons les propriétés métathéoriques essentielles du système, dont
les preuves sont partiellement mécanisées, et détaillons son
implémentation dans l'assistant de preuve Coq. D'autre part, nous
décrivons l'intégration et l'extension d'un système de "Type Classes"
venu d'Haskell à Coq via une simple interprétation des constructions
liées aux classes dans la théorie des types sous-jacente. Nous
démontrons l'utilité des classes de types dépendantes pour la
spécification et la preuve et présentons une implémentation économique
et puissante d'une tactique de réécriture généralisée basée sur les
classes. Nous concluons par la mise en œuvre de l'ensemble de ces
contributions lors du développement d'une bibliothèque certifiée de
manipulation d'une structure de données complexe, les "Finger Trees".

Abstract:

 Systems based on dependent type theory are getting considerable
attention for the verification of computer programs as well as a
practical tool for developing formal mathematical proofs involving
complex and expensive computations. These systems still require
considerable expertise from the users to be used efficiently. We design
high-level constructs permitting to use languages based on dependent
type theory as easily as modern functional programming languages,
without sacrificing the powerful constructs of the former. We study a
new language allowing to build certified programs while writing only
their algorithmical squeleton and their specification. Typing in this
system gives rise to proof obligations that can be handled interactively
a posteriori. We demonstrate the main metatheoretical properties on this
system, whose proofs are partially mechanized, and present its
implementation in the Coq proof assistant. Then we describe an
integration and extension of the type classes concept à la Haskell into
Coq, providing a simple interpretation of the constructs linked with
type classes into the underlying dependent type theory. We demonstrate
the usefulness of these dependent type classes for specifications and
proofs and present an economical yet powerful implementation of a
generalized rewriting tactic based on them. We conclude by employing
these contributions in the development of a certified library of a
complex data structure called Finger Trees.

 Une version préliminaire et en couleurs du manuscript est disponible
sur ma page: http://www.lri.fr/~sozeau

Faites passer!
-- Matthieu