Vincent Demange

Recherche

Présentation succincte

Thèmes d'intérêt

Mots-clés:

Informatique théorique; logique; lambda-calculs typés; méthodes formelles; sûreté; certification; vérification; Coq; Spike.

Articles de revues

V. Demange. Pedagogical lambda-cube: the λ² case. Journal of Logic and Computation, Vol. 25, No. 3, pp 743--779, 2015.
Trois présentations différentes d'un sous-système pégagogique du calcul des constructions au sens de [JUCS, 2013] sont proposées, et leur équivalence est démontrée: l'une avec motivations explicites totales, l'autre avec motivations totales, et la dernière avec motivations partielles. Le lien est fait avec les précédents travaux de Colson et Michel sur le second ordre par un plongement: on récupère alors un plongement du calcul propositionnel du second ordre usuel ainsi que du second ordre classique (λμ-calcul) dans ces systèmes. De plus le problème de la vérification du typage (type-checking) est étudié pour ces calculs.
L. Colson et V. Demange. Investigations on a pedagogical calculus of constructions. Journal of Universal Computer Science, Vol. 19, No. 6, pp. 729-749, 2013. [sources Coq].
Après un exposé succinct des travaux précédents sur la pédagogisation des systèmes formels, et un essai de pédagogisation, nous proposons la première définition formelle d'un sous-système pédagogique du calcul des constructions.

Conférences internationales avec actes

S. Stratulat et V. Demange. Automated certification of implicit induction proofs. CPP 2011, LNCS 7086, pp. 37-53. Springer-Verlag, 2011.
Des traces d'exécution du démonstrateur automatique Spike sont utilisées pour produire des preuves Coq de formules de façon automatique. Cet article propose une version constructive, ainsi que des améliorations du temps de vérification des preuves Coq produites, notamment en parallélisant l'étape de vérification.

Communications

P. Balbiani, V. Demange, D. Galmiche. A sequent calculus with labels for PAL. Advances in Modal Logic 2014.
Nous présentons un calcul des séquents avec labels correct et complet pour la logique des annonces publiques PAL.
V. Demange. Thèse: Vers un Calcul des Constructions pédagogique (transparents).
Les systèmes pédagogiques sont apparus récemment à propos des calculs propositionnels (jusqu'à l'ordre supérieur), et consistent à donner systématiquement des exemples des notions (hypothèses) introduites. Formellement, cela revient à contraindre la règle d'hypothèse (Hyp) en déduction naturelle en une règle (P-Hyp) nécessitant la donnée d'exemples (i.e. instances prouvées) de formules introduites dans l'environnement. Autrement dit pour mettre un ensemble G de formules en hypothèse, il est requis de donner une substitution s telle que l'instance s(G) soit démontrable. Cette nécessité d'exemplification ayant été pointée du doigt par Poincaré (1913) comme relevant du bon sens: une définition d'un objet par postulat n'ayant d'intérêt que si un tel objet existe. Cette restriction appliquée à des systèmes formels intuitionnistes rejoint l'idée des mathématiques sans négation défendues par Griss (1946) au milieu du siècle dernier, et présentées comme une version radicale de l'intuitionnisme. À travers l'isomorphisme de Curry-Howard (1980), la contrepartie calculatoire est l'utilité des programmes définis dans les systèmes fonctionnels correspondant: toute fonction peut être appliquée à un argument clos. Les premiers résultats concernant les calculs propositionnels jusqu'au second ordre ont été publiés récemment par Colson et Michel (2007, 2008, 2009). Nous exposons dans ce rapport une tentative d'uniformisation et d'extension au Calcul des Constructions (CC) des précédents résultats. Tout d'abord une définition formelle et précise de sous-système pédagogique du Calcul des Constructions est introduite, puis différents tels sous-systèmes sont déclinés en exemple..
S. Stratulat et V. Demange. Validating Implicit Induction Proofs Using Certified Proof Environments. SecDay 2010.
Résumé sur un exemple simple de l'approche de validation des preuves de Spike en Coq.
V. Demange. Rapport de Master 2 recherche: formalisation de rudiments de théorie des treillis dans Coq.
J'ai effectué mon stage de Master recherche à l'université Paul-Verlaine de Metz sous la direction de Loïc Colson. L'objectif était de formaliser des morceaux de théorie du point fixe (Knaster-Tarski, Niwinski, Colson) dans l'assistant à la preuve Coq dans sa version 8.1pl3, tout en respectant au mieux le «style mathématique». Ainsi il a été fait intensivement usage des notations ainsi que des preuves non-automatisées (mais explicatives).
Ce développement rudimentaire peut servir comme point d'entrée à la formalisation des mathématiques ainsi qu'à l'utilisaton de l'assistant à la preuve Coq. Remarque: le code n'a pas été mis à jour pour les versions supérieures et ne compilera pas tel quel (p. ex. le module Setoid a subit de profondes modifications). Le code peut être simplifié pour profiter des dernières nouveautés.

Exposés

Résumé de mes activités de recherche

Durant mon stage de Master recherche, j'ai formalisé en Coq des théorèmes de point fixe dans des treillis complets connus (e.g. Knaster-Tarski) et plus évolués comme les théorèmes de points fixes diagonaux de Niwinski ou de Colson.

Mon travail doctoral a consisté en l'étude de systèmes formels et fonctionnels pédagogiques en particulier autour du Calcul des Constructions. J'ai aussi participé à la validation des preuves d'un démonstrateur automatique (Spike) à l'aide d'un démonstrateur interactif (Coq).

Et récemment, dans le cadre du projet ANR DynRes (Dynamic Resources and Separation and Update Logics), je me suis intéressé à la conception et l'étude de systèmes formels pour des logiques modales et/ou de ressources.

Formalisation de mathématiques Des théorèmes de points fixes apparaissent souvent en informatique théorique: calcul d'invariant, fonctions récursives et lambda-calcul, état stable d'un système, etc. Celui de Knaster, généralisé par Tarski aux treillis complets, permet notamment d'exprimer un prédicat de vérité syntaxique lors de la démonstration de cohérence de l'arithmétique de Peano à l'intérieur de l'arithmétique du second ordre. Ces théorèmes sont souvent très abstraits (e.g. auto-référence, imprédicativité, etc.), et leur formalisation contribue à augmenter la confiance qu'on leur porte. Plus généralement cette nécessité de certification de démonstrations mathématiques devient cruciale et ravive des questions des fondements des mathématiques et de l'informatique, notamment en termes de praticabilité comme en attestent par exemple les développements récents du mathématicien Vladimir Voevodsky et son programme d'Univalent foundations.

Concernant ce travail de fin d'étude, la formalisation de rudiments de théorie du point fixe dans les treillis a été menée dans l'outil de preuve interactif Coq avec comme objectifs principaux la facilité de lecture et de suivi des démonstrations, en particulier par une personne non experte du système Coq. Les possibilités offertes par Coq comme les notations et leurs portés, les structures mathématiques, les conversions implicites, le langage de tactiques, etc. permettent d'approcher le style mathématique informel usuel, et laissent entrevoir une évolution nécessaire dans les processus de diffusion scientifique. Par exemple notre article [JUCS2013] a été partiellement formalisé en Coq en s'appuyant sur un travail antérieur de Barras ( Coq en Coq).

Systèmes formels pédagogiques La caractéristique principale des systèmes formels pédagogiques est de demander systématiquement à l'utilisateur de fournir des exemples des hypothèses utilisées. Cette nécessité d'exemplification ayant été pointée du doigt par Poincaré dans le cas des définitions par postulat comme relevant du bon sens: une définition d'un objet par postulat n'ayant d'intérêt que si un tel objet existe. Concrètement, dans les systèmes de déduction naturelle cela revient à exiger que tout ensemble d'hypothèses Γ possède une instance σ·Γ dont toutes les formules sont démontrables. Cette restriction appliquée à des systèmes formels intuitionnistes empêche l'utilisation de la négation et le raisonnement par contradiction: il n'est pas possible d'admettre comme hypothèse une formule A afin d'aboutir à une contradiction car une telle formule ne possèderait aucune instance prouvable. Cela rejoint l'idée des mathématiques sans négation défendues par Griss au milieu du siècle dernier, et présentée comme une version forte de l'intuitionnisme de Brouwer. Ici cependant la contrainte est positive —la donnée systématique d'exemples— là où chez Griss elle était négative —la suppression de la négation. Il est d'ailleurs tout à fait envisageable d'étudier des systèmes formels pédagogiques en dehors du cadre de l'intuitionnisme.

D'autre part, la contrepartie calculatoire de l'absence de formule non prouvable est l'utilité des programmes définis dans les systèmes fonctionnels correspondant: toute fonction de type A → B où A est clos peut être appliquée à un élément de type A. Cette utilité peut être vue comme une propriété de vivacité des programmes pédagogiques que les λ-calculs typés usuels ne permettent pas de capturer simplement. Ainsi les systèmes fonctionnels pédagogiques sont plus proches des langages de programmation pour lesquels les types vides ne sont pas nécessaires, validant fortement la correspondance de Curry-(De Bruijn)-Howard entre preuves-programmes et formules-types.

Les premiers résultats concernant les calculs propositionnels pédagogiques jusqu'au second ordre ont été publiés récemment par Colson et Michel (2007, 2008, 2009). Ces calculs pédagogiques possèdent des propriétés expressives comparables à la version intuitionniste dont ils sont issus: à chaque fois le calcul intuitionniste initial peut être plongé dans sa version pédagogique, et les programmes initialement typables possèdent une traduction par continuation typable dans la version pédagogique. Ainsi expressivité logique et puissance calculatoire sont maintenues par la contrainte pédagogique.

Lors de mon travail doctoral, je me suis appliqué à uniformiser ces résultats dans le but de les étendre au Calcul des Constructions (CC) de Coquand et Huet et ainsi obtenir un traitement homogène de systèmes pédagogiques du λ-cube de Barendregt, première étape vers des pure type systems pédagogiques. J'ai alors commencé par définir formellement et précisément la notion de sous-système pédagogique du Calcul des Constructions [JUCS2013], puis j'ai décliné différents tels sous-systèmes en exemple: du second-ordre [JLC2015] jusqu'à l'ordre supérieur, aboutissant finalement à une conjecture d'un Calcul des Constructions pédagogique [Thèse2012].
Au passage je me suis intéressé à l'étude de la vérification du typage (type checking) pour ces systèmes [JLC2015], préalable nécessaire à une éventuelle implémentation sur machine. Il s'est alors avéré qu'un nouveau type de formalisme est nécessaire dans lequel je suggère d'annoter les types par des termes pour s'assurer de leur exemplifiabilité, à l'instar du passage du λ-calcul pur aux λ-calculs typés annotant les termes par des types pour assurer leur terminaison.

Comme développements futurs, je conçois l'utilisation effective de logiques pédagogiques pour des cas réels: par exemple la vérification des travaux informels de Griss à propos des mathématiques sans négation; ou encore l'extraction de programmes. Pour cela une implémentation sur machine est nécessaire, et il convient d'approfondir l'étude des systèmes formels et fonctionnels pédagogiques: d'une part il faut en concevoir un suffisamment puissant et expressif; d'autre part il faut remédier à certains aspects inhérents aux systèmes pédagogiques (e.g. redondances lors du type checking, production semi-automatisée d'exemples, construction de bibliothèques de théories et d'exemples, etc.).

Aussi il est envisageable d'étudier finement certains principes équivalents d'un point de vue intuitionnistes, mais distincts d'un point de vue pédagogique (loi de Pierce, tiers-exclu, double négation, etc.). Par exemple Ariola et Herbelin ont étendu le calcul propositionnel minimal (CPM) (intrinsèquement pédagogique) afin de donner une signification logique précise au λµ-calcul de Parigot en terme d'une logique intermédiaire entre CPM et la logique propositionnelle classique, qui démontre la loi de Pierce ((A → B) → A) → A mais pas le principe de double négation ¬¬ A → A.

Validation de preuves automatiques Le démonstrateur automatique Spike, basé sur la réécriture et une technique de récurrence implicite, permet de vérifier de façon automatique des théorèmes du premier ordre, exprimés par des spécifications conditionnelles équationnelles sur des structures infinies et définies inductivement. L'originalité vient du fait qu'aucun principe de récurrence statique et explicite n'est énoncé a priori sur les types inductifs de la spécification. Essentiellement, l'idée est de tenter de réfuter les formules initiales, ceci en conservant un plus petit contre-exemple à chaque étape. Si le processus échoue dans sa recherche d'un tel plus petit contre-exemple, alors les conjectures sont nécessairement «vraies». À chaque étape, des instances de l'énoncé en cours de preuve peuvent être utilisés comme hypothèse. La validité de la dérivation est assurée in fine, en utilisant un ordre bien fondé sur les formules.

J'ai participé à la certification des dérivations de Spike dans l'assistant à la preuve Coq à l'aide d'un traducteur utilisant une trace d'exécution de Spike afin de générer un script de preuve Coq. Nous avons fait usage de la librairie Coccinelle développée au LRI de l'Université Paris Sud pour l'ordre RPO et son extension aux multi-ensembles.
Plusieurs exemples «jouets» ont ainsi déjà été validés de cette façon: spécifications conditionnelles booléennes, fonctions mutuellement récursives, etc. [SecDay2010]. Puis après avoir rendue la méthode constructive et améliorer son temps d'exécution, nous l'avons appliqué à un exemple réel: la validation du protocole d'équilibrage réseau ABR [CPP2011]. Enfin et plus récemment, Henaien et Stratulat ont étendus ces travaux en développant une tactique automatique sous forme de greffon au logiciel Coq.

Une toute autre démarche certainement ambitieuse que je suggère serait d'implémenter directement Spike en Coq, assurant ainsi la validité des preuves et développements futurs de Spike a priori. Ainsi Spike en tant qu'outil externe à Coq s'obtiendrait par extraction, ou bien pourrait être utilisé à l'intérieur de Coq par la technique de réflexivité obtenant par effet de bord une tactique automatique certifiée, robuste et plus facilement composable avec d'autres tactiques existantes.

Logiques de ressources Le projet ANR DynRes (Dynamic Resources and Separation and Update Logics) est une collaboration de membres des laboratoires IRIT de Toulouse, du LSV de Cachan et du Loria de Nancy. Les objets d'étude sont les logiques de ressources (e.g. BI, BBI, SL) et les logiques dynamiques (e.g. DEL, PAL) pour la modélisation de propriétés complexes de programmes (partage, concurrence, mise à jour, etc.). Le projet se découpe en plusieurs thèmes: l'étude des propriétés des ressources (partage, interaction, modèles abstraits et concrets, etc.); l'expressivité comparée et la décidabilité de fragments ou d'hybridations (séparation/modalités); et les systèmes de preuve, réfutations et contre-modèles, procédures de décision et outils logiciels.

Dans ce cadre, et dans l'objectif d'hybrider des logiques dynamiques (e.g. PAL pour public announcement logic) avec des logiques de ressources (e.g. BI pour bunched implication logic), j'ai participé au développement d'un calcul des séquents avec labels pour PAL [AiML2014] qui est issu d'une étude critique d'un travail de Maffezioli et Negri. L'élément clef réside dans la gestion d'une pile d'annonces associée aux formules et dont l'évaluation est repoussée aux atomes, évitant le recours à des notions de restriction de modèles. En effet permettre la restriction de modèles peut s'avérer problématique dans le cas des logiques de ressources: le modèle restreint peut perdre certaines de ses propriétés indispensables (e.g. être un monoïde).

D'autre part, ces logiques étant plutôt définies à travers leur sémantique, une théorie de la preuve simple et efficace complèterait avantageusement les approches actuelles de vérification principalement basées sur des techniques de model-checking. On peut par exemple envisager des outils de preuve semi-interactifs concernant certaines de ces logiques, parfois indécidables ou difficilement automatisables, bénéficiant de l'utilisateur comme guide à la preuve. Aussi cette méthode de séquents avec labels et piles est très certainement adaptable au traitement d'autres logiques faisant apparaître des restrictions de modèles similaires dans leur définition sémantique.