1,721,071 research outputs found
Front Matter, Table of Contents, Preface, Conference Organization
No full textFront Matter, Table of Contents, Preface, Conference Organizatio
A formal proof of Hensel's lemma over the p-adic integers
No full textThe field of p-adic numbers p and the ring of p-adic integers p are essential constructions of modern number theory. Hensels lemma, described by Gouva as the most important algebraic property of the p-adic numbers, shows the existence of roots of polynomials over p provided an initial seed point. The theorem can be proved for the p-adics with significantly weaker hypotheses than for general rings. We construct p and p in the Lean proof assistant, with various associated algebraic properties, and formally prove a strong form of Hensels lemma. The proof lies at the intersection of algebraic and analytic reasoning and demonstrates how the Lean mathematical library handles such a heterogeneous topic.</p
Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules
Full text linkDependently typed languages such as Coq and Agda can statically guarantee the correctness of our proofs and programs. To provide this guarantee, they restrict users to certain schemes a- such as strictly positive datatypes, complete case analysis, and well-founded induction a- that are known to be safe. However, these restrictions can be too strict, making programs and proofs harder to write than necessary. On a higher level, they also prevent us from imagining the different ways the language could be extended. In this paper I show how to extend a dependently typed language with user-defined higher-order non-linear rewrite rules. Rewrite rules are a form of equality reflection that is applied automatically by the typechecker. I have implemented rewrite rules as an extension to Agda, and I give six examples how to use them both to make proofs easier and to experiment with extensions of type theory. I also show how to make rewrite rules interact well with other features of Agda such as-equality, implicit arguments, data and record types, irrelevance, and universe level polymorphism. Thus rewrite rules break the chains on computation and put its power back into the hands of its rightful owner: Yours.Programming Language
A Formalization of the LLL Basis Reduction Algorithm
Full text linkThe LLL basis reduction algorithm was the first polynomial-time algorithm to compute a reduced basis of a given lattice, and hence also a short vector in the lattice. It thereby approximates an NP-hard problem where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm has several applications in number theory, computer algebra and cryptography.In this paper, we develop the first mechanized soundness proof of the LLL algorithm using Isabelle/HOL. We additionally integrate one application of LLL, namely a verified factorization algorithm for univariate integer polynomials which runs in polynomial time
Meta-Programming for Proof Transfer in Dependent Type Theory
No full textEn mathématiques comme en informatique, il est d’usage de faire appel à des outils numériques de vérification pour augmenter la confiance dans les preuves et les logiciels. La pratique la plus commune est le test, mais elle est limitée. Les assistants de preuve interactifs sont des outils permettant d’effectuer des preuves avec une grande confiance, laissant l’humain trouver les idées des preuves tout en vérifiant méticuleusement que toutes les étapes de la preuve sont valides. Cette thèse s’inscrit dans une lignée de travaux visant à automatiser les preuves, avec l’objectif final de répandre l’usage des assistants de preuve à la place du test logiciel, partout où cela est possible et pertinent. On s’intéresse ici au partage de théorie formelle entre plu- sieurs représentations différentes d’un même concept mathématique, ou plusieurs implémentations d’une même spécification. Sur le plan théorique, cette étude s’appuie sur l’ana- lyse de traductions de paramétricité pour le Calcul des Constructions, et en propose une généralisation. Ces résultats s’incarnent dans la conception de deux outils de transfert de preuve, TRAKT et TROCQ, dont on discute ici l’implémentation, à l’aide du méta-langage COQ-ELPI.In both mathematics and computer science, it is common practice to use digital verification tools to increase confidence in proofs and software. The most common prac- tice is testing, but it is limited. Interactive proof assistants are tools made to perform proofs with high confidence, letting humans come up with proof ideas while meticulously checking that all proof steps are valid. This thesis is part of a line of work aimed at automat- ing proofs, with the ultimate goal of spread- ing the use of proof assistants in place of software testing, wherever possible and relevant. Here, we are interested in sharing of formal theory between several different representa- tions of the same mathematical concept, or several implementations of the same specifi- cation. From a theoretical point of view, this study is based on the analysis of parametric- ity translations for the Calculus of Constructions, and proposes a generalisation of them. These results are made concrete in the design of two proof transfer tools, TRAKT and TROCQ, whose implementation is discussed here, using the COQ-ELPI meta-language
Continuité en théorie des types
No full textDans cette thèse, j'étudie l’interaction entre la théorie des types et la continuité, un concept mathématique formalisant l’intuition qu’une fonction ne peut interroger qu’une partie finie de son argument avant de renvoyer une valeur Dans le premier chapitre, je décris la théorie des types et mon prisme de lecture: la correspondance preuve-programme, ou isomorphisme de Curry-Howard, qui affirme que calcul et preuve sont deux faces d’une même pièce. J’y explique comment la théorie des types bute encore sur l’intégration de principes dits classiques, comme l’axiome du choix ou le tiers- exclu. Dans le deuxième chapitre, j’analyse les différentes définition de la continuité, et comment celles-ci diffèrent les unes des autres d’un point de vue logique. Dans le troisième chapitre, je présente une première tentative d’intégration de la continuité en théorie des types, à travers un modèle syntaxique d’une théorie des types particulières, appelée Baclofen Type Theory. Enfin, dans le dernier chapitre, je détaille une théorie des types où toutes les fonctions sont continues, et présente des résultats préliminaires de normalisation de cette théorie.In this thesis, I study the interaction between type theory and continuity, a mathematical concept describing the intuition that a function can only query a finite part of its argument before returning a value. In the first Chapter, I describe type theory and my working paradigm: the proof-program correspondence, or Curry-Howard isomorphism, which asserts that computation and proof are two sides of the same coin. I explain how type theory is still struggling with the integration of so-called classical principles, such as the axiom of choice or the excluded-middle. In a second part I survey the different definitions of continuity, and how they differ from each other from a logical point of view. In the third Chapter I present a first attempt to mingle continuity and type theory, through a syntactic model of a particular type theory, dubbed Baclofen Type Theory. Finally, in the last Chapter I define a type theory where all functions are continuous, and present preliminar results on the proof of its normalisation
Machine-checked mathematics
Full text linkInternational audienceIn this article she gives an overview about machine-checked mathematics
Programming and certifying a CAD algorithm in the Coq system
No full textInternational audienceA. Tarski has shown in 1948 that one can perform quantifier elimination in the theory of real closed fields. The introduction of the Cylindrical Algebraic Decomposition (CAD) method has later allowed to design rather feasible algorithms. Our aim is to program a reflectional decision procedure for the Coq system, using the CAD, to decide whether a (possibly multivariate) system of polynomial inequalities with rational coefficients has a solution or not. We have therefore implemented various computer algebra tools like gcd computations, subresultant polynomial or Bernstein polynomials
Mathematical Structures in Dependent Type Theory (Invited Talk)
No full textIn this talk, we discuss the role and the implementation of mathematical structures in libraries of formalised mathematics in dependent type theory
- …
