TypiCal

Abstract:

The object of this thesis is the study of the ability of the Coq system to mix proofs and programs in practice. Our approach consists in implementing part of the program Kenzo, a computer algebra tool for homological algebra under some constraint. We want to be able to read the program as a proof with a computational content, these proofs much compute efficiently, and we try to avoid duplication of proofs or part thereof.

We show, first, how the requirement of efficiency leads to revise some aspects of traditional mathematics. We propose a suitable categorical abstraction, both for clarity and to avoid duplications. This abstraction, though different from what is customary in mathematics, allow to formulate the constructs of homological algebra in a style much like that of Kenzo. We propose, then, modifications to the Coq programm. A first one to make proofs more convenient, by allowing the use of more fine grain tactics which are often necessary when dependent types are common. The second modification to leverage the arithmetical abilities of the processor to compute more efficiently on integers.

Finally, we propose some leads to improve both sharing and clarity of the proofs. Unfortunately, they push the system beyond its limits. Hence, we show that Coq is not always up to its promises and that theoretical works will be necessary to understand how these limits can be relaxed.

We present some general methods to prove properties about specific distributed algorithms and generic results from this field. We principally study local computations systems, an abstract model of distributed algorithms based on labelled graph transformations. We first introduce this model, and a few examples of correctness and impossibility proofs. Then we describe the structure of the Coq library we are building for this purpose. Finally, we underline the importance of dealing with randomized distributed algorithms, and show how we plan to use the Alea library in order to formally prove randomized algorithms in Coq.

Abstract:

I discuss two examples of program extraction from proofs using induction and coinduction.

The first example builds on coinductive predicates characterising "approximable" real numbers and continuous real functions. From proofs of closure properties of these predicates one extracts implementations of a range of continuous functions with respect to the signed digit representation of real numbers. Due to the coinductive nature of the predicates one obtains implementations of continuous functions as infinite data structures.

In the second example I show how to extract monadic parser combinators from proofs that certain labelled transition systems are finitely branching. While in the first example coinduction is central, here induction features prominently because finiteness is an inductive concept.

Links:

• the slides

First- and higher-order terms are both sufficient syntaxes for mathematics. Neither of these give direct access to the names of variables; "x" denotes something but is not in itself a thing that can easily be denoted. This causes difficulty in "nominal" applications (having to do with names), such as specifying logics and reduction systems with binders, or building denotations for name-passing calculi, or representing atomic secrets in cryptography, and so on. Permissive nominal terms are a syntax for mathematics very similar to first-order syntax, and having an easy sets-based denotation, but with the advantage that names have first-class status. If you imagine that permissive nominal terms are a suitable "formal meta-level" for the ordinary mathematics, in the spirit of designing good theorem-provers but with an emphasis on names and binding, then you will not go far wrong. To place this in the context of research taking place at LIX, this is similar to what Dale Miller does but with less proof-theory and more sets denotations. I will give a talk on these issues which I hope may be of interest to designers of theorem-provers, proof-theories, and nominal calculi e.g. for concurrency or security. Further details can be found on my webpage gabbay.org.uk including two papers on permissive nominal terms Permissive nominal terms and their unification and Permissive nominal logic.

We prove formally that the first order theory of algebraically closed fields enjoys quantifier elimination, and hence is decidable. This proof is organized in two modular parts. We first reify the first order theory of rings and prove that quantifier elimination leads to decidability. Then we implement an algorithm which constructs a quantifier free formula from any first order formula in the theory of ring. If the underlying ring is in fact an algebraically closed field, we prove that the two formulas have the same semantic. The algorithm producing the quantifier free formula is programmed in continuation passing style, which leads to both a concise program and an elegant proof of semantic correctness.

We propose a formal study of interval analysis that concentrates on theoretical aspects rather than on computational ones. In particular we are interested in conditions for regularity of interval matrices. An interval matrix is called regular if all scalar matrices included in the interval matrix have non-null determinant and it is called singular otherwise. Regularity plays a central role in solving systems of linear interval equations. Several tests for regularity are available and widely used, but sometimes rely on rather involved results, hence the interest in formally verifying such conditions of regularity. In this talk we show how we define intervals, interval matrices and operations on them in the proof assistant Coq, and verify criteria for regularity and singularity of interval matrices.

La conjecture de catégoricité non dénombrable de Los affirme qu'une théorie est catégorique pour toute cardinal non dénombrable si elle l'est pour au moins un tel cardinal. Morley donna une preuve basée sur de proprietés des ensembles fortement minimaux (c.a.d. irréductibles de dimension 1) qui ont en suite été reconnus comme les briques élémentaires pour analyser toute structure de rang de Morley fini. Zilber conjectura qu'il n'existe que trois archétypes de tels ensembles. Ceci fut contredit très ingénieusement par Hrushovski ; sa méthode est l'outil principal pour construire des ensembles fortement minimaux exotiques. Cet exposé s'adressera à un publique non spécialisé en théorie des modèles. On utilisera des exemples concrets pour illustrer les résultats présentés.

Matrices represented by computer programs, also called black-box matrices, are a popular topic in Computer Algebra. Since the seminal paper (Wiedemann 86), algorithms to do arithmetic operations on them, as multiplication, determinant, minimal polynomial, etc., have been intensely studied and are now well understood.

The status of transposition of black box matrices is much less clear. It is a (not so well known) theorem in Algebraic Complexity that black-box matrices given by (non-uniform) arithmetic circuits can be transposed without changing the complexity of the circuit. In the more familiar Turing model, this translates to a principle, often known as "transposition principle" or "Tellegen's principle" in the Computer Algebra community, that gives a "recipe" to "transpose" an algorithm "without changing its complexity".

In this talk I will give a formal proof of the transposition principle in the touring model and sketch the implementation of a compiler that transposes algorithms written in our ad-hoc algebraic language Transalpyne. (Maybe not so) Surprisingly, we discovered some connections with Type Systems and Categoty Theory while attacking this problem: I will try to explain these connections and point out some possible research directions.

Abstract:

Je parlerai de quelques aspects du travail mené dans l'équipe Parsifal, et de la façon dont cela pourrait s'articuler avec Coq.

Dans une première partie je présenterai les logiques avec points fixes (définitions inductives et coinductives) que nous utilisons, en comparant un peu avec le calcul des constructions inductives. Cela me permettra d'introduire certains fragments et des stratégies de recherche de preuve, en discutant de la pertinence de leur adaptation à Coq.

Dans une seconde partie, je traiterai de la notion plus délicate de quantification générique (nabla). Cette notion apporte une expressivité très intéressante à nos logiques, puisqu'elle permet de spécificier naturellement des systèmes tels que le lambda ou le pi-calcul, mais son "adaptation" à Coq semble difficile; j'évoquerai cependant des pistes.

Liens: Les transparents de l'exposé

Abstract:

Le thème central de cet exposé prend ces racines dans une question philosophique : quelle est la signification des constants logiques ? Ou encore, et avec plus d’ambition : y a-t-il un critère pour identifier les ‘bonnes’ constants logiques ?

Une réponse possible à ces questions peut être trouvée dans la maxime wittgensteinienne selon laquelle ‘la signification est l’usage (dans le langage)’ ; en l’appliquant au cas des constants logiques cela conduit à l’idée que leur signification est donnée par leurs règles d’inférence (position inférentialiste). Mais, ainsi formulée, cette idée est encore trop naïve, comme cela a été montré par A. Prior, grâce au connecteur pathologique tonk. Ce connecteur est défini par des règles d’inférence apparemment légitimes, mais qui, ajoutées à celles des connecteurs logiques standards, amène à l’inconsistance du système. Une manière d’éviter des connecteurs pathologiques de ce type est d'exiger la propriété de l’élimination des coupures. Toutefois, rajouter cette propriété à notre cahier des charges pour l’identification des bonnes constants logiques nous dit seulement comment éviter certaines constants pathologiques, mais elle n’explique pas la cause de la pathologie. C’est seulement en passant par une traduction de tonk dans une système d’inférence modulo certaines règles de réécriture (i.e. dans la déduction modulo) que cette explication devient possible.

Enfin, à l’aide de cette approche via règles de réécriture, j’essayerai de montrer comme même l’élimination des coupures n’est pas une condition suffisante pour l’identification des bonnes constants logiques. Ce type d’investigation me permettra aussi de regarder de plus près certaines conditions imposées sur le système de réécriture utilisés en déduction modulo (notamment la propriété de non-confusion des connecteurs).

Liens: les transparents de l'exposé.

All information here: http://www.lix.polytechnique.fr/~cousineau/research.php?lang=eng

Les espaces cohérents probabilistes ont été introduits par Jean-Yves Girard dans son article sur les espaces cohérents quantiques. Nous reprenons et raffinons un peu sa définition, et nous montrons que ces objets fournissent un modèle de la logique linéaire au complet. Nous montrons qu'ils permettent aussi d'interpréter, sans faire appel aux powerdomains, une version probabiliste du langage fonctionnel PCF et prouvons une version probabiliste du théorème d'adéquation de Plotkin pour ce langage, dont la sémantique opérationnelle est décrite par une matrice stochastique infinie. Enfin, nous décrivons un modèle probabiliste du lambda-calcul pur dans les espaces cohérents probabilistes. Il s'agit d'un travail commun avec Vincent Danos.

Résumé:

We consider the problem of automating and checking the use of previously proved lemmas in the proof of some main theorem. In particular, we call the collection of such previously proved results a table and use a partial order on the table's entries to denote the (provability) dependency relationship between tabled items. We incorporate tables into sequent calculus proofs by performing two steps. First, cuts are used to incorporate tabled items into a proof: one premise of the cut requires a proof of the lemma and the other premise has the lemma inserted into the set of assumptions. Second, to ensure that lemmas are not reproved, we exploit the non-canonicity of focusing systems and specify two specific focusing disciplines for tabled formulas.

1. We allow only atomic formulas in tables. Then, by exploiting the fact that, in focusing systems, atoms can be assigned positive or negative polarity, we impose the following polarity discipline: atoms that are in the table are given positive polarity and those not in the table are given negative polarity.
2. We restrict tabled formulas to fixed point literals, that is, fixed points and their negations, and universally quantified fixed point literals, denoting both finite successes and finite failures. Then, by exploiting the fact that fixed points can be frozen and be treated like atoms, we impose a second focusing discipline: fixed points that are instances of a tabled formula are frozen and those that are not instances of a tabled formula are not frozen.

We show that, in some fragments of first-order-logic, the only existing proofs and open derivations are those that do not attempt to (re)prove a tabled formula: for the first discipline, we use the hereditary Harrop formulas fragment of intuitionistic logic and for the second discipline, we use the fragment of intuitionistic logic with fixed points used in \cite{tiu05eshol}, where only formulas constructed from positive connectives appear in the left-hand-side of sequents and all fixed points are noetherian.

10:00 - 11:00 Tjark Weber: Integrating SAT and SMT in Isabelle/HOL (slides)
11:00 - 11:30 BREAK
11:30 - 12:30 Michael Armand: Integrating SAT in Coq (slides)
12:30 - 13:00 discussions

14:00 - 15:00 Sascha Boehme: Integrating SMT in Isabelle/HOL (slides)
15:00 - 15:30 BREAK
15:30 - 16:30 Pascal Fontaine: The veriT solver
16:30 - ... discussions

Résumé:

L'interaction entre assistants de preuves peut permettre d'utiliser des théorèmes "aisément" prouvés dans un assistant de preuve donné, dans un autre assistant de preuve dans lequel ils auraient été plus difficiles à prouver. Cependant, les systèmes de preuves peuvent parfois être très différents.

Dans cet exposé, je présenterai une méthode pour importer des preuves de HOL-Light en Coq, basée sur la réflection. Après avoir présenté HOL-Light rapidement, j'expliquerai comment d'une part construire un modèle de HOL-Light en Coq prouvé correct, d'autre part enregistrer et exporter les termes de preuve de HOL-Light.

Liens: les transparents de l'exposé

We give a new elegant proof that decreasing diagrams imply conflu-
ence based on a proof reduction technique, which is then the basis of a novel
completion method which proof-reduction relation transforms arbitrary proofs
into rewrite proofs even in presence of non-terminating reductions. Unlike pre-
vious methods, no ordering of the set of terms is required, but can be used if
available. Unlike ordered completion, rewrite proofs are closed under
instantiation. Examples are presented, including Kleene’s and Huet’s classical examples
showing that non-terminating local-confluent relations may not be confluent.

Joint work with Vincent van Oostrom (cf. ICALP 09)

Résumé : (a joint work with G. Gonthier, A. Mahboubi & L. Rideau)

In this talk, we will propose generic design patterns to define and combine algebraic structures, using dependent records, coercions and type inference, inside the Coq system. This alternative to telescopes in particular supports multiple inheritance, maximal sharing of notations and theories, and automated structure inference. Our methodology is robust enough to handle a hierarchy comprising a broad variety of algebraic structures, from types with a choice operator to algebraically closed fields. Interfaces for the structures enjoy the convenience of a classical setting, without requiring any axiom.

Liens : Page de l'orateur, Article

Intervenant: A. Charguéraud

Date et lieu: Jeudi 2 avril 2009, 10h00-12h00, salle de réunion du LIX

Résumé: Je décrirai comment raisonner en Coq sur des programmes Caml purement fonctionnels, à travers un plongement profond du noyau de Caml dans Coq. Ceci consiste à décrire la syntaxe et la sémantique de Caml à l'aide d'inductifs Coq. On peut ainsi énoncer les spécifications de programmes donnés sous forme de lemmes, puis vérifier ces programmes en prouvant les lemmes de spécification de manière interactive. Cette approche a le bénéfice de n'imposer quasiment aucune restriction sur le code, et de disposer d'un langage de spécification et de preuve extrêmement riche à moindre frais. On verra que cette technique permet de certifier des programmes Caml complexes avec des scripts de longueur assez raisonnable. Pour finir, on discutera de la possibilité de définir une fonction logique Coq à partir du code certifié d'une fonction Caml (le processus inverse de l'extraction).

Liens: Les transparents de l'exposé.

Intervenant : Alexandre Miquel (ENS Lyon)

Date et lieu : 16/04/2004, 10h, Salle de conférence du Lix

Résumé : Mon premier exposé sera consacré aux problèmes posés (en général) par l'extraction de programmes à partir de preuves formalisées en logique classique (i.e. avec tiers-exclu). Je commencerai par rappeler en quoi consiste l'extraction de programme dans le cadre de la logique constructive (i.e. sans tiers-exclu), les problèmes que cela pose et les différentes solutions proposées (typage vs. réalisabilité, extraction à la MinLog vs. extraction à la Coq...) Ensuite je m'intéresserai aux traductions négatives (qui servent à rétracter des théories classiques sur leur fragment constructif) et je montrerai comment ces traductions permettent de mettre en oeuvre (de manière effective) l'extraction de programmes à partir de preuves classiques de formules Pi_2. Enfin, je montrerai comment la théorie de la réalisabilité classique introduite par Krivine permet d'exprimer les mêmes programmes en style direct (i.e. sans CPS ni traduction négative) grâce à l'utilisation de continuations.

Intervenant: Simon Perdix

Date et lieu: 30/04/09 à 14h, salle de séminaires du LPTP

Résumé: Le calcul quantique par mesures, introduit par Briegel et Raussendorf, est non seulement une des plus prometteuses propositions de réalisation physique de l'ordinateur quantique, mais ouvre aussi de nouvelles perspectives théoriques, notamment en termes de parallélisation des opérations quantiques. Dans cet exposé, je présenterai le measurement calculus, introduit par Danos, Kashefi et Panangaden, un cadre formel permettant d'étudier les propriétés du calcul quantique par mesures. La mesure, brique de base de ce modèle, a une évolution fondamentalement probabiliste. Aussi, l'existence d'une évolution globalement déterministe dépend de l'état initial du calcul qui est représenté par un graphe. Nous montrons que l'existence d'un flot généralisé dans ce graphe est une condition nécessaire et suffisante à l'existence d'une exécution globalement déterministe. De plus, nous introduisons un algorithme classique efficace permettant de décider si un graphe donné admet un flot généralisé.

Intervenant: Bruno Barras

Date et lieu: Jeudi 7 mai 2009, 14h00-16h00, salle de conférence du LIX

Résumé: La première partie de mon exposé fera des rappels au sujet du Calcul des Constructions Implicites (ICC). En particulier, je montrerai en quoi ICC est beaucoup plus souple que Coq en matière de spécification de programmes. Après ces rappels, je dresserai la stratégie pour étendre ce formalisme avec des types inductifs, dont un prototype est déjà implanté.

La première extension concerne l'égalité. Celle-ci est assez facile car le modèle de ICC d'Alexandre Miquel permet déjà de la justifier. Au passage je montrerai comment ajouter l'axiome K de Streicher (qui permet d'implanter le filtrage a la Epigram/Agda) à Coq en seulement 4 caractères.

L'extension de ICC avec des Sigma-types (paires dépendantes) sera plus difficile, si l'on inclut la notion (nouvelle) de Sigma-type implicite où l'une des 2 composantes de la paire est implicite. Suivant la composante considérée implicite, on introduit les notions de sous-type ou d'union de type. Si la métathéorie syntaxique ne pose pas de problème, le modèle d'espaces cohérents d'Alexandre n'est pas stable par union: l'union de types sémantiques n'est pas un type sémantique.

Récemment, Alexandre a prouvé qu'il était possible de "compléter" une union de types sémantiques en un type sémantique, et que cela justifie notre extension. Cette complétion a pour effet inattendu de fusionner certains éléments qui étaient distincts dans leur type d'origine. Pour mettre en évidence ce phénomène et expliquer en quoi cela est finalement intuitif, je présenterai de manière minimaliste le modèle d'Alexandre basé sur les espaces cohérents.