-
Fri, 9 Oct 2009
-
Thu, 1 Jan 2009
-
Fri, 6 Feb 2009
TypiCal seminars
A Formal Proof of the Kepler Conjecture: The Flyspeck Project.
Tue, 2011-05-24 09:08 | by assiaMixing proofs and programs in Coq
Fri, 2011-01-28 15:39 | by notinThe 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.
Demi-arités, demi-équations et sémantiques initiales
Tue, 2011-03-22 12:43 | by notinLa séparation entre syntaxe et sémantique ne cesse de s'estomper, les méthodes de la syntaxe élargissant progressivement leur couverture de la sémantique. On montrera dans cet exposé comment l'approche privilégiant les modules sur les monades offre de nouvelles perspectives pour cette évolution. Cette approche, étudiée notamment dans les thèses de J.Zsido et B.Ahrens, conduit à des notions générales d'arité et d'équation (ou d'inéquation) donnant lieu à de nouvelles constructions de sémantiques initiales. Nos exemples tournent autour du lambda-calcul plus ou moins typé, avec substitution plus ou moins explicite, et beta-réduction plus ou moins orientée.
Formal proofs of Local Computation Systems
Tue, 2011-02-15 07:58 | by assiaRéalisabilité et paramétricité dans les PTS
Mon, 2011-02-07 10:52 | by assiaJe décrirai une méthode systématique pour construire une logique à partir d'un lambda-calcul typé décrit comme un système de types pur (PTS). Cette logique, elle-même présentée sous forme de PTS, fournit des formules pour exprimer des propriétés des termes. Elle offre ainsi un cadre adéquat pour développer une théorie de la paramétricité ainsi qu'une théorie de la réalisabilité du langage d'origine. Enfin, grâce à la généralité des PTS, je montrerai comment paramétricité et réalisabilité s'avèrent être inter-définissables dans ce cadre.
Program extraction from proofs: computable analysis and parser generation
Tue, 2011-01-11 18:38 | by assiaI 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:Using Intuitionistic Logic as a basis for Legal Ontologies
Fri, 2010-10-08 09:29 | by assiaPermissive nominal terms
Thu, 2010-09-30 13:30 | by assiaUne analyse calculatoire de la transformation de preuve par forcing
Tue, 2010-06-15 08:33 | by assiaLe forcing est une technique inventée par Cohen pour démontrer la cohérence et/ou l'indépendance de certains axiomes vis à vis de la théorie des ensembles. Du point de vue de la théorie de la démonstration, le forcing repose sur une traduction des formules et des preuves paramétrée par un ensemble ordonné quelconque: l'ensemble des "conditions de forcing". Récemment, Krivine a proposé une méthode permettant de combiner le forcing avec la théorie de la réalisabilité classique, et a montré que la traduction des preuves par forcing correspond (au niveau des termes de preuves à la Curry) à une transformation de programme étonamment compréhensible.
Suite aux travaux de Krivine, je montrerai comment reformuler le forcing en arithmétique d'ordre supérieur, en me plaçant dans une extension adéquate du système F-omega (classique) avec termes de preuves à la Curry. Je présenterai la traduction des formules et la transformation de preuve-programme sous-jacente. Enfin, j'analyserai le comportement calculatoire des programmes traduits, et en déduirai une extension de la machine de Krivine avec environnements explicites - la KFAM - conçue pour traiter directement les preuves par forcing sans passer par la transformation de programme. Je concluerai sur les liens que cette étude fait apparaître entre la méthode de forcing et certains principes à la base des systèmes d'exploitation, ainsi que sur les perspectives en logique.
Liens: les transparents de l'exposéA formal quantifier elimination for algebraically closed fields
Wed, 2010-04-28 17:41 | by assiaVérification formelle et utilisation d'un solveur SMT dans Coq
Tue, 2010-04-06 12:59 | by assiaInterval Analysis in Coq
Thu, 2010-03-04 16:15 | by assiaOn the completeness of quantum computation models
Fri, 2010-02-26 10:13 | by assiaCatégoricité et classification des ensembles fortement minimaux
Wed, 2010-02-24 17:56 | by assiaOn using sums-of-squares for exact computations without strict feasibility
Fri, 2010-01-08 15:06 | by assiaIn order to prove that a system of real polynomial inequalities has no solution, the usual method is to compute a cylindrical algebraic decomposition (CAD) of that system, which yields a false/true answer - for instance, using Mathematica's Reduce function. CAD implementations, especially those that implement optimizations necessary to go beyond toy examples, are notoriously complex and trusting such a massive amount of code for applications such as proving mathematical theorems or proving safety-critical programs is methodologically disputable.
Instead of trusting a complex implementation, or building a certified version thereof, we would prefer the complex algorithm produces an easily checkable "witness" of its answer. For systems of polynomials inequalities, the Positivstellensatz theorems ensure the existence of witnesses made of sums of squares of polynomials. As a particular case, a nonnegative polynomial can often be expressed as a sum of squares of polynomials, and can always be expressed as a quotient of sums of squares of polynomials.
Such sums of squares are solutions of a semidefinite programming feasibility problem (that is, given F_0, ..., F_n symmetric matrices, finding y_i such that -F_0 + \sum_i y_i F_i is semidefinite positive, that is, has no negative eigenvalues). Unfortunately, direct application of semidefinite programming numerical methods is only possible if the solution set has nonempty interior. This is not the case in general.
We propose a workaround for this problem, based on LLL lattice reduction.
On the transposition of black-box matrices
Tue, 2010-01-19 17:05 | by assiaMatrices 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.
Learning in SAT
Mon, 2010-01-04 10:08 | by gfaureIn this talk we first give an introduction to modern SAT solving, and then we present several contributions to Conflict Driven Clause Learning (CDCL), which is one of the key components of modern SAT solvers. First, we propose an extended notion of implication graph containing additional arcs, called inverse arcs. These are obtained by taking into account the satisfied clauses of the formula, which are usually ignored in classical conflict analysis. Secondly, we present an original adaptation of conflict analysis for dynamic clauses subsumption. Our last contribution demonstrates that clause learning can be exploited at each step of the search tree, even if a conflict do not occurs. This last contribution aims to derive new but more powerful reasons leading to the implication of a given literal. For all these contributions, we discuss their possible integration to modern SAT solvers.
Liens: les transparents de l'exposéRecherche de preuve, points fixes et quantification générique: transfert vers Coq?
Thu, 2009-10-15 17:27 | by gfaureJe 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éWorkshop at Bordeaux (ARC Corias): deduction modulo
Mon, 2009-12-14 15:49 | by gfaureConstantes logiques: entre inférentialisme et réécriture
Thu, 2009-10-08 11:57 | by gfaureLe 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é.Numerical Computations for Coq Formal Proofs, and Vice Versa
Thu, 2009-10-08 11:56 | by gfaureWhen performing the certification of a piece of floating-point code, one usually has to prove properties about errors, which are mathematical expressions relating values from the program and values from the specification. These errors can be split in two categories: rounding errors and method errors, depending on their origin; and the methods for bounding them differ greatly.
I will present two Coq tactics dedicated to proving properties about numerical errors. The "gappa" tactic is an interface to the Gappa external tool; it queries the tool for properties on rounding errors. The "interval" tactic, on the other hand, is designed to deal with method errors, or more generally, differentiable expressions involving elementary functions.
A noteworthy point is that both tactics are themselves based on floating-point arithmetic. Indeed, the proofs they generate are checked by performing intensive numerical computations inside the formal system. For "gappa", these proofs are provided by an oracle, while they are fully reflexive for "interval". I will describe the arithmetic and some of the algorithms they use.
Models and proof normalisations
Wed, 2009-10-14 13:06 | by gfaureTyping in simple type theory a la Newman
Wed, 2009-10-14 13:07 | by gfaureThe type checking algorithm for simple type theory solves the problem whether an untyped lambda-term M has a type according to the rules of simple type theory. As usual, we distinguish between a type checking problem: M : A? (does the term M have type A?) and a type synthesis problem: M : ? (compute a type A for the term M). It is a classic result that for simple type theory, these problems are equivalent and decidable. The solution amounts to computing the principal type of M and then to check whether the given type A is an instance of it.
There is a (seemingly) different way to decide typing, due to Newman, already in 1943, and recently reviewed by Hindley. Newman's algorithm only decides whether a term is typable and does not compute a principal type. This is quite remarkable. We describe Newman's algorithm in a modern fashion as a manipulation of the tree that represents the lambda-term. We analyze Newman's algorithm and we show that it (implicitly) does compute a principal type, and that the way it computes it is actually quite close to Wand's version of the typing algorithm for simple type theory.
Espaces cohérents probabilistes: un modèle convexe de la logique linéaire.
Thu, 2009-10-15 15:53 | by gfaureModels and proof normalisations (répétition)
Thu, 2009-10-15 15:51 | by gfaureTabling with fixpoints
Wed, 2009-10-07 14:27 | by gfaureWe 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.
- 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.
- 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.
Une implémentation du Calcul des Constructions Inductives avec Presburger
Fri, 2009-07-31 12:46 | by assiaLe CCI/Presburger est une variante du Calcul des Constructions Inductives intégrant au sein de sa conversion (le fragment de Hoare de) l'arithmétique linéaire entière.
Après une brève présentation de CCI/Presburger, je présenterai mon implémentation de ce calcul au sein du système Coq, notamment en soulignant les modifications apportées au noyau.
J'aborderai également le problème de la confiance en un tel noyau, via l'utilisation de procédures de décisions certifiées ou générant des certificats. En particulier, je parlerai de la décision certifiée et efficace des arithmétiques linéaires entière et rationnelle.
Liens: les transparents de l'exposé, la page de l'intervenant.Integrating SAT and SMT Solvers with Isabelle/HOL
Mon, 2009-07-20 13:20 | by gfaure10: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
Europa : un vérificateur de types pour le lambda-pi-calcul-modulo.
Tue, 2009-06-09 17:28 | by assiaLe lambda-pi-calcul est un calcul avec types dépendants permettant l'expression de preuves en logique minimales des prédicats. En étendant ce calcul avec des règles de réécriture, il devient possible d'exprimer des preuves dans des théories bien plus riches. On obtient ainsi le lambda-pi-calcul-modulo. Un encodage de tous les PTS fonctionnels est par exemple possible. Se pose alors la question des stratégies à mettre en oeuvre pour l'implantation de vérificateurs efficaces de preuves encodées ainsi. En effet, vérifier la plus simple de ces preuves nécessite l'application de nombreuses règles de réécriture, ce qui peut être coûteux en temps de calcul.
Je montrerai comment se tirer d'affaire à peu de frais, en compilant les preuves exprimées dans le lambda-pi-calcul-modulo vers un programme fonctionnel, dont l'évaluation par des environnements d'exécution usuels en permet la vérification. Nous ferons la démonstration de l'outil clé d'un tel modèle, le méta-vérificateur Europa, traitant de bout en bout son implantation très simple.
Liens: les transparents de l'exposéImportation de preuves HOL-Light en Coq
Tue, 2009-06-09 17:30 | by assiaL'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éExtension d'un prouveur basé sur la résolution avec la résolution modulo polarisée.
Mon, 2009-06-08 15:06 | by assiaAu cours de cet exposé, j'expliquerai l'architecture générale des prouveurs basés sur la résolution. Je rappellerai certaines techniques utilisées pour réduire le non-déterminisme lié à l'application de la règle de résolution. En particulier je présenterai la résolution avec ensemble de support et la résolution ordonnée avec sélection, en insistant sur les conditions qui permettent de conserver la complétude réfutationnelle. Nous verrons qu'en combinant ces deux dernières techniques, on peut perdre la complétude réfutationnelle. Je rappellerai alors l'équivalence de cette combinaison avec la résolution modulo polarisé, puis je montrerai que sa complétude est équivalente avec l'admissibilité des coupures en déduction modulo. Je présenterai enfin comment appliquer ces idées pour modifier un prouveur existant (en l'occurrence iprover) afin d'y ajouter la résolution polarisée modulo.
Liens: http://www.loria.fr/~burel/Diagrammatic Confluence and Completion
Thu, 2009-06-18 16:32 | by assiaWe 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)
Dans quelle théorie démontrer la complétude d'une méthode de démonstration automatique ?
Fri, 2009-06-05 10:21 | by assiaDepuis le théorème de Gödel, on sait que, dans toute extension cohérente de l'arithmétique, il existe des propositions qui ne sont pas démontrables, mais qui le deviennent dans certaines extensions de cette théorie. On montre, dans cet exposé, que les propositions qui expriment la complétude d'une méthode de démonstration automatique, c'est-à-dire la propriété que cette méthode trouve, en un temps fini, une démonstration pour toutes les propositions démontrables, sont des exemples de telles propositions. La théorie dans laquelle on peut démontrer la complétude d'une méthode de démonstration automatique donne un certain nombre d'informations sur ce que cette méthode peut faire et sur ce qu'elle ne peut pas faire. On illustrera ce point par une comparaison entre la résolution ordonnée avec sélection et la résolution modulo.
Liens : http://www.lix.polytechnique.fr/~dowek/index-fra.htmlPackaging mathematical structures
Tue, 2009-06-09 07:58 | by assiaIn 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, ArticleTotalité algébrique et complétude
Thu, 2009-04-09 14:00 | by notinRésumé: Les espaces de finitude forment une sémantique dénotationnelle de la logique linéaire dont les formules sont interprétées par des espaces vectoriels topologiques et les preuves par par des applications linéaires continues. En étudiant la topologie des espaces de finitude, nous avons défini une notion algébrique de totalité qui permet de définir un modèle de la logique linéaire plus fin que celui des espaces de finitude. Ainsi, nous avons obtenu un théorème de complétude pour un lambda-calcul avec une somme barycentrique et des constructions booléennes au premier ordre.
Cet exposé débutera par l'étude d'un lambda-calcul barycentrique booléen. Après en avoir introduit un modèle utilisant des polynômes, je présenterai un théorème de complétude pour ce calcul. Dans un second temps, je définirai les espaces de finitude et la totalité qui nous ont amenés à considérer ce théorème.
Liens: la page personnelle de l'intervenant, les transparents de l'exposé
Vérification interactive de programmes Caml purs
Thu, 2009-04-02 10:00 | by notinIntervenant: 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é.
Structures algébriques et tactiques de décisions
Thu, 2009-04-23 13:00 | by notinIntervenant: D. Pous
Date et lieu: Jeudi 23 avril 2009, 14h00-16h00, salle de conférence du LIX
Résumé: Formaliser des choses dans un assistant de preuve s'avère souvent pénible, de nombreuses étapes de raisonnement devant être explicitées alors qu'elles sont d'habitude laissées au relecteur scrupuleux. Ceci est en particulier vrai lorsque l'on doit travailler sur des relations binaires (réécriture, réductions, équivalences, etc...), très intuitives, mais pas complètement triviales.
Lorsque c'est possible, une première astuce consiste à considérer les relations de façon algébrique : en montant le niveau d'abstraction, on facilite la formalisation de certaines preuves. Une fois ce pas franchi, on réalise que les relations binaires sont un modèle des algèbres de Kleene, décidables par la théorie des automates finis.
Nous exposerons un travail en cours, sur une formalisation Coq des automates - via des matrices, afin d'obtenir une tactique de décision des algèbres de Kleene, par réflection. Plus généralement, nous exposerons les outils que nous développons pour raisonner sur ce genre de structures algébriques.
Extraction de programmes à partir de preuves classiques
Thu, 2009-04-16 17:33 | by assiaIntervenant : 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.
L'extraction classique en Coq
Thu, 2009-04-16 17:36 | by assiaIntervenant: Alexandre Miquel (ENS Lyon)
Date et lieu: 16/04/2009, 14h Salle de conférence du Lix
Résumé: Mon deuxième exposé (qui fera suite à l'exposé du matin) sera consacré à l'extraction classique dans le cadre de l'assistant à la preuve Coq. Dans un premier temps, je montrerai comment la théorie de la réalisabilité classique de Krivine - définie à l'origine pour l'arithmétique classique du second ordre - peut être étendue au calcul des constructions inductives (pICC) avec tiers-exclu. Ensuite je présenterai le schéma d'extraction classique étendu à pICC ainsi que les diverses optimisations mises en oeuvre dans le module d'extraction classique (notamment en ce qui concerne la représentation des entiers). Enfin, je terminerai mon exposé par quelques exemples de programmes extraits à partir de preuves classiques, sous la forme d'une démo.
Liens: Les transparents de l'exposé.
Calcul quantique par mesures
Thu, 2009-04-30 13:40 | by assiaIntervenant: 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é.
From a scalar type system to a vectorial type system (joint work with P. Arrighi)
Mon, 2009-05-04 13:00 | by assiaIntervenant: Alejandro Díaz-Caro (LIG)
Date et lieu: 04/05, 14h, salle de réunion du préfabriqué du Lix
Résumé: The Linear-Algebraic Lambda-Calculus (arXiv:quant-ph/0612199) is a higher-order lambda-calculus together with the possibility to make linear combinations of terms. Terms can be seen as forming a vectorial space. However, dealing with concepts such as orthogonality and unitarity is not trivial. The scalar type system (arXiv:0903.3741) is a System F-like type system with scalars in the types. It can be seen as a first step towards a vectorial type system, with which to reason about orthogonality and unitarity. The additive type system is a type system with sums of types on it, which can be seen as a subset of the intuitionistic-multiplicative-exponential linear logic (IMELL). Finally, the vectorial type system puts scalar and additive together, making a vectorial space of types. In this seminar we will present these three type systems and some clues as to whether the last one enables us to check for orthogonality.
Liens: Les transparents de l'exposé.
Extension du calcul des constructions implicite avec des types union et sous-ensemble
Thu, 2009-05-07 13:00 | by notinIntervenant: 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.
Un systeme de type polymorphe pour le lambda-calcul avec constructeurs.
Tue, 2009-05-26 09:23 | by assiaIntervenant : Barbara Petit (ENS Lyon)
Date et lieu : 11/06/09, salle de conférence du Lix
Résumé : Le lamba-calcul avec constructeurs, de Arbiser, Miquel et Rios est une extension du lambda calcul avec un mecanisme de filtrage. Le filtrage "a la ML" y est decomposé en deux opérations elementaires: une analyse de cas sur des constantes, et une regle de commutation -surprenante au premier abord- entre le case et l'application.
Apres avoir presenté ce calcul, je lui definirai un systeme de types polymorphe avec unions et intersections. Enfin je montrerai un modele de realisabilite (proche candidats de reductibilites de Girard) pour ce systeme, et les proprietes de normalisation forte et de sureté vis a vis du filtrage qui en decoulent.
Liens : http://perso.ens-lyon.fr/barbara.petit/recherche.php