We describe how to compute very far decimals of $$\pi$$ and how to provide formal guarantees that the decimals we compute are correct. In particular, we report on an experiment …
We describe how to compute very far decimals of $$\pi$$ and how to provide formal guarantees that the decimals we compute are correct. In particular, we report on an experiment where 1 million decimals of $$\pi$$ and the billionth hexadecimal (without the preceding ones) have been computed in a formally verified way. Three methods have been studied, the first one relying on a spigot formula to obtain at a reasonable cost only one distant digit (more precisely a hexadecimal digit, because the numeration basis is 16) and the other two relying on arithmetic-geometric means. All proofs and computations can be made inside the Coq system. We detail the new formalized material that was necessary for this achievement and the techniques employed to guarantee the accuracy of the computed digits, in spite of the necessity to work with fixed precision numerical computation.
We describe the formalisation in Coq of a proof that the numbers `e` and `pi` are transcendental. This proof lies at the interface of two domains of mathematics that are …
We describe the formalisation in Coq of a proof that the numbers `e` and `pi` are transcendental. This proof lies at the interface of two domains of mathematics that are often considered separately: calculus (real and elementary complex analysis) and algebra. For the work on calculus, we rely on the Coquelicot library and for the work on algebra, we rely on the Mathematical Components library. Moreover, some of the elements of our formalized proof originate in the more ancient library for real numbers included in the Coq distribution. The case of `pi` relies extensively on properties of multivariate polynomials and this experiment was also an occasion to put to test a newly developed library for these multivariate polynomials.
We describe the formalisation in Coq of a proof that the numbers e and $\pi$ are transcendental. This proof lies at the interface of two domains of mathematics that are …
We describe the formalisation in Coq of a proof that the numbers e and $\pi$ are transcendental. This proof lies at the interface of two domains of mathematics that are often considered separately: calculus (real and elementary complex analysis) and algebra. For the work on calculus, we rely on the Coquelicot library and for the work on algebra, we rely on the Mathematical Components library. Moreover, some of the elements of our formalized proof originate in the more ancient library for real numbers included in the Coq distribution. The case of $\pi$ relies extensively on properties of multivariate polynomials and this experiment was also an occasion to put to test a newly developed library for these multivariate polynomials.
We describe the formalisation in Coq of a proof that the numbers e and $\pi$ are transcendental. This proof lies at the interface of two domains of mathematics that are …
We describe the formalisation in Coq of a proof that the numbers e and $\pi$ are transcendental. This proof lies at the interface of two domains of mathematics that are often considered separately: calculus (real and elementary complex analysis) and algebra. For the work on calculus, we rely on the Coquelicot library and for the work on algebra, we rely on the Mathematical Components library. Moreover, some of the elements of our formalized proof originate in the more ancient library for real numbers included in the Coq distribution. The case of $\pi$ relies extensively on properties of multivariate polynomials and this experiment was also an occasion to put to test a newly developed library for these multivariate polynomials.
We study several formal proofs and algorithms related to the number pi in the context of Coq's standard library. In particular, we clarify the relation between roots of the cosine …
We study several formal proofs and algorithms related to the number pi in the context of Coq's standard library. In particular, we clarify the relation between roots of the cosine function and the limit of the alternated series whose terms are the inverse of odd natural numbers (known as Leibnitz' formula).We give a formal description of the arctangent function and its expansion as a power series. We then study other possible descriptions of pi, first as the surface of the unit disk, second as the limit of perimeters of regular polygons with an increasing number of sides.In a third section, we concentrate on techniques to effectively compute approximations of pi in the proof assistant by relying on rational numbers and decimal representations.
This short note reviews the relations between homotopy theory and type theory, especially the similarity between paths in homotopy and proofs of equality in type theory.
This short note reviews the relations between homotopy theory and type theory, especially the similarity between paths in homotopy and proofs of equality in type theory.
Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of …
Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of mathematics. On the one hand, Voevodsky's subtle and beautiful "univalence axiom" implies that isomorphic structures can be identified. On the other hand, "higher inductive types" provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory. Both are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of "logic of homotopy types". This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an "invariant" conception of the objects of mathematics -- and convenient machine implementations, which can serve as a practical aid to the working mathematician. This book is intended as a first systematic exposition of the basics of the resulting "Univalent Foundations" program, and a collection of examples of this new style of reasoning -- but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.
This article presents the formal proof of correctness for a plane Delaunay triangulation algorithm. It consists in repeating a sequence of edge flippings from an initial triangulation until the Delaunay …
This article presents the formal proof of correctness for a plane Delaunay triangulation algorithm. It consists in repeating a sequence of edge flippings from an initial triangulation until the Delaunay property is achieved. To describe triangulations, we rely on a combinatorial hypermap specification framework we have been developing for years. We embed hypermaps in the plane by attaching coordinates to elements in a consistent way. We then describe what are legal and illegal Delaunay edges and a flipping operation which we show preserves hypermap, triangulation, and embedding invariants. To prove the termination of the algorithm, we use a generic approach expressing that any non-cyclic relation is well-founded when working on a finite set.
This article presents the formal proof of correctness for a plane Delaunay triangulation algorithm. It consists in repeating a sequence of edge flippings from an initial triangulation until the Delaunay …
This article presents the formal proof of correctness for a plane Delaunay triangulation algorithm. It consists in repeating a sequence of edge flippings from an initial triangulation until the Delaunay property is achieved. To describe triangulations, we rely on a combinatorial hypermap specification framework we have been developing for years. We embed hypermaps in the plane by attaching coordinates to elements in a consistent way. We then describe what are legal and illegal Delaunay edges and a flipping operation which we show preserves hypermap, triangulation, and embedding invariants. To prove the termination of the algorithm, we use a generic approach expressing that any non-cyclic relation is well-founded when working on a finite set.
Gilles Kahn was born in Paris on April 17th, 1946 and died in Garches, near Paris, on February 9th, 2006. He received an engineering diploma from Ecole Polytechnique (class of …
Gilles Kahn was born in Paris on April 17th, 1946 and died in Garches, near Paris, on February 9th, 2006. He received an engineering diploma from Ecole Polytechnique (class of 1964), studied for a few years in Stanford and then joined the computer science branch of the French Atomic Energy Commission (CEA), which was to become the CISI company. He joined the French research institute in computer science and control theory (IRIA, later renamed INRIA) in 1976. He stayed with this institute until his death, at which time he was the chief executive officer of the institute. He was a member of Academia Europaea from 1995 and a member of the French Academy of Science from 1997.
We describe how the formal description of a programming language can be encoded in the Coq theorem prover. Four aspects are covered: Natural semantics (as advocated by Gilles Kahn), axiomatic …
We describe how the formal description of a programming language can be encoded in the Coq theorem prover. Four aspects are covered: Natural semantics (as advocated by Gilles Kahn), axiomatic semantics, denotational semantics, and abstract interpretation. We show that most of these aspects have an executable counterpart and describe how this can be used to support proofs about programs.
We propose a (limited) solution to the problem of constructing stream values defined by recursive equations that do not respect the guardedness condition. The guardedness condition is imposed on definitions …
We propose a (limited) solution to the problem of constructing stream values defined by recursive equations that do not respect the guardedness condition. The guardedness condition is imposed on definitions of corecursive functions in Coq, AGDA, and other higher-order proof assistants. In this paper, we concentrate in particular on those non-guarded equations where recursive calls appear under functions. We use a correspondence between streams and functions over natural numbers to show that some classes of non-guarded definitions can be modelled through the encoding as structural recursive functions. In practice, this work extends the class of stream values that can be defined in a constructive type theory-based theorem prover with inductive and coinductive types, structural recursion and guarded corecursion
In Constructive Type Theory, recursive and corecursive definitions are subject to syntactic restrictions which guarantee termination for recursive functions and productivity for corecursive functions. However, many terminating and productive functions …
In Constructive Type Theory, recursive and corecursive definitions are subject to syntactic restrictions which guarantee termination for recursive functions and productivity for corecursive functions. However, many terminating and productive functions do not pass the syntactic tests. Bove proposed in her thesis an elegant reformulation of the method of accessibility predicates that widens the range of terminative recursive functions formalisable in Constructive Type Theory. In this paper, we pursue the same goal for productive corecursive functions. Notably, our method of formalisation of coinductive definitions of productive functions in Coq requires not only the use of ad-hoc predicates, but also a systematic algorithm that separates the inductive and coinductive parts of functions.
In Constructive Type Theory, recursive and corecursive definitions are subject to syntactic restrictions which guarantee termination for recursive functions and productivity for corecursive functions. However, many terminating and productive functions …
In Constructive Type Theory, recursive and corecursive definitions are subject to syntactic restrictions which guarantee termination for recursive functions and productivity for corecursive functions. However, many terminating and productive functions do not pass the syntactic tests. Bove proposed in her thesis an elegant reformulation of the method of accessibility predicates that widens the range of terminative recursive functions formalisable in Constructive Type Theory. In this paper, we pursue the same goal for productive corecursive functions. Notably, our method of formalisation of coinductive definitions of productive functions in Coq requires not only the use of ad-hoc predicates, but also a systematic algorithm that separates the inductive and coinductive parts of functions.
interpreters are tools to compute approximations for behaviors of a program. These approximations can then be used for optimisation or for error detection. In this paper, we show how to …
interpreters are tools to compute approximations for behaviors of a program. These approximations can then be used for optimisation or for error detection. In this paper, we show how to describe an abstract interpreter using the type-theory based theorem prover Coq, using inductive types for syntax and structural recursive programming for the abstract interpreter's kernel. The abstract interpreter can then be proved correct with respect to a Hoare logic for the programming language.
We extend the work of A. Ciaffaglione and P. di Gianantonio on the mechanical verification of algorithms for exact computation on real numbers, using infinite streams of digits implemented as …
We extend the work of A. Ciaffaglione and P. di Gianantonio on the mechanical verification of algorithms for exact computation on real numbers, using infinite streams of digits implemented as a co-inductive type. Four aspects are studied. The first concerns the proof that digit streams correspond to axiomatised real numbers when they are already present in the proof system. The second re-visits the definition of an addition function, looking at techniques to let the proof search engine perform the effective construction of an algorithm that is correct by construction. The third concerns the definition of a function to compute affine formulas with positive rational coefficients. This is an example where we need to combine co-recursion and recursion. Finally, the fourth aspect concerns the definition of a function to compute series, with an application on the series that is used to compute Euler's number e . All these experiments should be reproducible in any proof system that supports co-inductive types, co-recursion and general forms of terminating recursion; we used the C OQ system (Dowek et al . 1993; Bertot and Castéran 2004; Giménez 1994).
We describe several views of the semantics of a simple programming language as formal documents in the calculus of inductive constructions that can be verified by the Coq proof system. …
We describe several views of the semantics of a simple programming language as formal documents in the calculus of inductive constructions that can be verified by the Coq proof system. Covered aspects are natural semantics, denotational semantics, axiomatic semantics, and abstract interpretation. Descriptions as recursive functions are also provided whenever suitable, thus yielding a a verification condition generator and a static analyser that can be run inside the theorem prover for use in reflective proofs. Extraction of an interpreter from the denotational semantics is also described. All different aspects are formally proved sound with respect to the natural semantics specification.
We describe the basic notions of co-induction as they are available in the coq system. As an application, we describe arithmetic properties for simple representations of real numbers.
We describe the basic notions of co-induction as they are available in the coq system. As an application, we describe arithmetic properties for simple representations of real numbers.
These notes provide a quick introduction to the Coq system and show how it can be used to define logical concepts and functions and reason about them. It is designed …
These notes provide a quick introduction to the Coq system and show how it can be used to define logical concepts and functions and reason about them. It is designed as a tutorial, so that readers can quickly start their own experiments, learning only a few of the capabilities of the system. A much more comprehensive study is provided in [1], which also provides an extensive collection of exercises to train on.
We propose to use Tarski's least fixpoint theorem as a basis to define recursive functions in the calculus of inductive constructions. This widens the class of functions that can be …
We propose to use Tarski's least fixpoint theorem as a basis to define recursive functions in the calculus of inductive constructions. This widens the class of functions that can be modeled in type-theory based theorem proving tool to potentially non-terminating functions. This is only possible if we extend the logical framework by adding the axioms that correspond to classical logic. We claim that the extended framework makes it possible to reason about terminating and non-terminating computations and we show that common facilities of the calculus of inductive construction, like program extraction can be extended to also handle the new functions.
We extend the work of A. Ciaffaglione and P. Di Gianantonio on mechanical verification of algorithms for exact computation on real numbers, using infinite streams of digits implemented as co-inductive …
We extend the work of A. Ciaffaglione and P. Di Gianantonio on mechanical verification of algorithms for exact computation on real numbers, using infinite streams of digits implemented as co-inductive types. Four aspects are studied: the first aspect concerns the proof that digit streams can be related to the axiomatized real numbers that are already axiomatized in the proof system (axiomatized, but with no fixed representation). The second aspect re-visits the definition of an addition function, looking at techniques to let the proof search mechanism perform the effective construction of an algorithm that is correct by construction. The third aspect concerns the definition of a function to compute affine formulas with positive rational coefficients. This should be understood as a testbed to describe a technique to combine co-recursion and recursion to obtain a model for an algorithm that appears at first sight to be outside the expressive power allowed by the proof system. The fourth aspect concerns the definition of a function to compute series, with an application on the series that is used to compute Euler's number e. All these experiments should be reproducible in any proof system that supports co-inductive types, co-recursion and general forms of terminating recursion, but we performed with the Coq system [12, 3, 14].
We describe the basic notions of co-induction as they are available in the coq system. As an application, we describe arithmetic properties for simple representations of real numbers.
We describe the basic notions of co-induction as they are available in the coq system. As an application, we describe arithmetic properties for simple representations of real numbers.
These notes provide a quick introduction to the Coq system and show how it can be used to define logical concepts and functions and reason about them. It is designed …
These notes provide a quick introduction to the Coq system and show how it can be used to define logical concepts and functions and reason about them. It is designed as a tutorial, so that readers can quickly start their own experiments, learning only a few of the capabilities of the system. A much more comprehensive study is provided in [1], which also provides an extensive collection of exercises to train on.
We develop the theoretical foundation of a new representation of real numbers based on the infinite composition of linear fractional transformations (lft), equivalently the infinite product of matrices, with non-negative …
We develop the theoretical foundation of a new representation of real numbers based on the infinite composition of linear fractional transformations (lft), equivalently the infinite product of matrices, with non-negative coefficients. Any rational interval in the one point compactification of the real line, represented by the unit circle S1, is expressed as the image of the base interval [0, ∞] under an lft. A sequence of shrinking nested intervals is then represented by an infinite product of matrices with integer coefficients such that the first so-called sign matrix determines an interval on which the real number lies. The subsequent so-called digit matrices have non-negative integer coefficients and successively refine that interval. Based on the classification of lft's according to their conjugacy classes and their geometric dynamics, we show that there is a canonical choice of four sign matrices which are generated by rotation of S1 by π/4. Furthermore, the ordinary signed digit representation of real numbers in a given base induces a canonical choice of digit matrices.
A theory of recursive and corecursive definitions has been developed in higher-order logic (HOL) and mechanized using Isabelle. Least fixedpoints express inductive data types such as strict lists: greatest fixedpoints …
A theory of recursive and corecursive definitions has been developed in higher-order logic (HOL) and mechanized using Isabelle. Least fixedpoints express inductive data types such as strict lists: greatest fixedpoints express coinductive data types, such as lazy lists. Well-founded recursion expresses recursive functions over inductive data types: corecursion expresses functions that yield elements of coinductive data types. The theory rests on a traditional formalization of infinite trees. The theory is intended for use in specification and verification. It supports reasoning about a wide range of computable functions, but it does not formalize their operational semantics and can express noncomputable functions also. The theory is illustrated using finite and infinite lists. Corecursion expresses functions over infinite lists, coinduction reasons about such functions.
Click to increase image sizeClick to decrease image size This article is part of the following collections: Mathematics of Pi
Click to increase image sizeClick to decrease image size This article is part of the following collections: Mathematics of Pi
This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the official …
This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the official published account of the now completed Flyspeck project.
We describe a HOL Light formalization of Hermite's proof that the base of the natural logarithm e is transcendental. This is the first time a proof of this fact has …
We describe a HOL Light formalization of Hermite's proof that the base of the natural logarithm e is transcendental.
This is the first time a proof of this fact has been formalized in a theorem prover.
Floating point operations are fast, but require continuous effort on the part of the user in order to ensure that the results are correct. This burden can be shifted away …
Floating point operations are fast, but require continuous effort on the part of the user in order to ensure that the results are correct. This burden can be shifted away from the user by providing a library of exact analysis in which the computer handles the error estimates. Previously, we [Krebbers/Spitters 2011] provided a fast implementation of the exact real numbers in the Coq proof assistant. Our implementation improved on an earlier implementation by O'Connor by using type classes to describe an abstract specification of the underlying dense set from which the real numbers are built. In particular, we used dyadic rationals built from Coq's machine integers to obtain a 100 times speed up of the basic operations already. This article is a substantially expanded version of [Krebbers/Spitters 2011] in which the implementation is extended in the various ways. First, we implement and verify the sine and cosine function. Secondly, we create an additional implementation of the dense set based on Coq's fast rational numbers. Thirdly, we extend the hierarchy to capture order on undecidable structures, while it was limited to decidable structures before. This hierarchy, based on type classes, allows us to share theory on the naturals, integers, rationals, dyadics, and reals in a convenient way. Finally, we obtain another dramatic speed-up by avoiding evaluation of termination proofs at runtime.
We extend the work of A. Ciaffaglione and P. di Gianantonio on the mechanical verification of algorithms for exact computation on real numbers, using infinite streams of digits implemented as …
We extend the work of A. Ciaffaglione and P. di Gianantonio on the mechanical verification of algorithms for exact computation on real numbers, using infinite streams of digits implemented as a co-inductive type. Four aspects are studied. The first concerns the proof that digit streams correspond to axiomatised real numbers when they are already present in the proof system. The second re-visits the definition of an addition function, looking at techniques to let the proof search engine perform the effective construction of an algorithm that is correct by construction. The third concerns the definition of a function to compute affine formulas with positive rational coefficients. This is an example where we need to combine co-recursion and recursion. Finally, the fourth aspect concerns the definition of a function to compute series, with an application on the series that is used to compute Euler's number e . All these experiments should be reproducible in any proof system that supports co-inductive types, co-recursion and general forms of terminating recursion; we used the C OQ system (Dowek et al . 1993; Bertot and Castéran 2004; Giménez 1994).
Let ƒ( x ) be one of the usual elementary functions (exp, log, artan, sin, cosh, etc.), and let M ( n ) be the number of single-precision operations required …
Let ƒ( x ) be one of the usual elementary functions (exp, log, artan, sin, cosh, etc.), and let M ( n ) be the number of single-precision operations required to multiply n -bit integers. It is shown that ƒ( x ) can be evaluated, with relative error Ο (2 - n ), in Ο ( M ( n )log ( n )) operations as n → ∞, for any floating-point number x (with an n -bit fraction) in a suitable finite interval. From the Schönhage-Strassen bound on M ( n ), it follows that an n -bit approximation to ƒ( x ) may be evaluated in Ο ( n log 2 ( n ) log log( n )) operations. Special cases include the evaluation of constants such as π, e , and e π . The algorithms depend on the theory of elliptic integrals, using the arithmetic-geometric mean iteration and ascending Landen transformations.
In Constructive Type Theory, recursive and corecursive definitions are subject to syntactic restrictions which guarantee termination for recursive functions and productivity for corecursive functions. However, many terminating and productive functions …
In Constructive Type Theory, recursive and corecursive definitions are subject to syntactic restrictions which guarantee termination for recursive functions and productivity for corecursive functions. However, many terminating and productive functions do not pass the syntactic tests. Bove proposed in her thesis an elegant reformulation of the method of accessibility predicates that widens the range of terminative recursive functions formalisable in Constructive Type Theory. In this paper, we pursue the same goal for productive corecursive functions. Notably, our method of formalisation of coinductive definitions of productive functions in Coq requires not only the use of ad-hoc predicates, but also a systematic algorithm that separates the inductive and coinductive parts of functions.
A summary is not available for this content so a preview has been provided. Please use the Get access link above for information on how to access this content.
A summary is not available for this content so a preview has been provided. Please use the Get access link above for information on how to access this content.
A fertile field of research in theoretical computer science investigates the representation of general recursive functions in intensional type theories. Among the most successful approaches are: the use of wellfounded …
A fertile field of research in theoretical computer science investigates the representation of general recursive functions in intensional type theories. Among the most successful approaches are: the use of wellfounded relations, implementation of operational semantics, formalization of domain theory, and inductive definition of domain predicates. Here, a different solution is proposed: exploiting coinductive types to model infinite computations. To every type A we associate a type of partial elements Partial(A), coinductively generated by two constructors: the first, return(a) just returns an element a:A; the second, step(x), adds a computation step to a recursive element x:Partial(A). We show how this simple device is sufficient to formalize all recursive functions between two given types. It allows the definition of fixed points of finitary, that is, continuous, operators. We will compare this approach to different ones from the literature. Finally, we mention that the formalization, with appropriate structural maps, defines a strong monad.
An important topic, which is on the boundary between numerical analysis and computer science ?. I found the book well written and containing much interesting material, most of the time …
An important topic, which is on the boundary between numerical analysis and computer science ?. I found the book well written and containing much interesting material, most of the time disseminated in specialized papers published in specialized journals difficult to find. Moreover, there are very few books on these topics and they are not recent.
Paper 8: Gert Almkvist and Bruce Berndt, “Gauss, Landen, Ramanujan, the arithmetic-geometric mean, ellipses, pi, and the Ladies Diary,” American Mathematical Monthly, vol. 95 (1988), pg. 585–608. Copyright 1988 Mathematical …
Paper 8: Gert Almkvist and Bruce Berndt, “Gauss, Landen, Ramanujan, the arithmetic-geometric mean, ellipses, pi, and the Ladies Diary,” American Mathematical Monthly, vol. 95 (1988), pg. 585–608. Copyright 1988 Mathematical Association of America. All Rights Reserved.
It is shown that an intuitionistic model of set theory with the axiom of choice has to be a classical one.
It is shown that an intuitionistic model of set theory with the axiom of choice has to be a classical one.
Recent work on homotopy type theory exploits an exciting new correspondence between Martin-Lof's dependent type theory and the mathematical disciplines of category theory and homotopy theory. The mathematics suggests new …
Recent work on homotopy type theory exploits an exciting new correspondence between Martin-Lof's dependent type theory and the mathematical disciplines of category theory and homotopy theory. The mathematics suggests new principles to add to type theory, while the type theory can be used in novel ways to do computer-checked proofs in a proof assistant. In this paper, we formalize a basic result in algebraic topology, that the fundamental group of the circle is the integers. Our proof illustrates the new features of homotopy type theory, such as higher inductive types and Voevodsky's univalence axiom. It also introduces a new method for calculating the path space of a type, which has proved useful in many other examples.
Teaching high-school mathematics using a general theorem prover becomes a reach- able goal for the near future. In this article, we present a library dealing with geometry in Coq. This …
Teaching high-school mathematics using a general theorem prover becomes a reach- able goal for the near future. In this article, we present a library dealing with geometry in Coq. This library is dedicated to high-school teaching. We stress on using a graphical interface and a drawing tool which ease the accessibility to formal statements. We present some signif- icant examples of statements with figures and proofs developed with Coq. Then we discuss the difficulties encountered in this work.
Is it reasonable to do constructive mathematics without the axiom of countable choice?Serious schools of constructive mathematics all assume it one way or another, but the arguments for it are …
Is it reasonable to do constructive mathematics without the axiom of countable choice?Serious schools of constructive mathematics all assume it one way or another, but the arguments for it are not compelling.The fundamental theorem of algebra will serve as an example of where countable choice comes into play and how to proceed in its absence.Along the way, a notion of a complete metric space, suitable for a choiceless environment, is developed.
We present a new approach to introducing an extensional propositional equality in Intensional Type Theory. Our construction is based on the observation that there is a sound, intensional setoid model …
We present a new approach to introducing an extensional propositional equality in Intensional Type Theory. Our construction is based on the observation that there is a sound, intensional setoid model in Intensional Type theory with a proof-irrelevant universe of propositions and /spl eta/-rules for /spl Pi/and /spl Sigma/-types. The Type Theory corresponding to this model is decidable, has no irreducible constants and permits large eliminations, which are essential for universes.
A representation of the computable real numbers by continued fractions is introduced. This representation deals with the subtle points of undecidable comparison and integer division, as well as representing the …
A representation of the computable real numbers by continued fractions is introduced. This representation deals with the subtle points of undecidable comparison and integer division, as well as representing the infinite 1/0 and undefined 0/0 numbers. Two general algorithms for performing arithmetic operations are introduced. The algebraic algorithm, which computes sums and products of continued fractions as a special case, basically operates in a positional manner, producing one term of output for each term of input. The transcendental algorithm uses a general formula of Gauss to compute the continued fractions of exponentials, logarithms, trigonometric functions, and a wide class of special functions. A prototype system has been implemented in LeLisp and the performance of these algorithms is promising.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">></ETX>
Setoids commonly take the place of sets when formalising mathematics inside type theory. In this note, the category of setoids is studied in type theory with universes that are as …
Setoids commonly take the place of sets when formalising mathematics inside type theory. In this note, the category of setoids is studied in type theory with universes that are as small as possible (and thus, the type theory is as weak as possible). In particular, we will consider epimorphisms and disjoint sums. We show that, given the minimal type universe, all epimorphisms are surjections, and disjoint sums exist. Further, without universes, there are countermodels for these statements, and if we use the Logical Framework formulation of type theory, these statements are provably non-derivable.
In this paper, we construct and investigate a model of the Univalent Foundations of Mathematics in the category of simplicial sets. To this end, we rst give a new technique …
In this paper, we construct and investigate a model of the Univalent Foundations of Mathematics in the category of simplicial sets. To this end, we rst give a new technique for constructing models of dependent type theory, using universes to obtain coherence. We then construct a (weakly) universal Kan bration, and use it to exhibit a model in simplicial sets. Lastly, we introduce the Univalence Axiom, in several equivalent formulations, and show that it holds in our model. As a corollary, we conclude that Univalent Foundations are at least as consistent as ZFC with two inaccessible cardinals.
We describe how the formal description of a programming language can be encoded in the Coq theorem prover. Four aspects are covered: Natural semantics (as advocated by Gilles Kahn), axiomatic …
We describe how the formal description of a programming language can be encoded in the Coq theorem prover. Four aspects are covered: Natural semantics (as advocated by Gilles Kahn), axiomatic semantics, denotational semantics, and abstract interpretation. We show that most of these aspects have an executable counterpart and describe how this can be used to support proofs about programs.
(2007). The Jordan Curve Theorem, Formally and Informally. The American Mathematical Monthly: Vol. 114, No. 10, pp. 882-894.
(2007). The Jordan Curve Theorem, Formally and Informally. The American Mathematical Monthly: Vol. 114, No. 10, pp. 882-894.
Nous nous proposons d'automatiser les preuves d'egalites sur les nombres reels dans le systeme Coq en utilisant la theorie des corps commutatifs. L'idee de l'algorithme consiste a se debarrasser des …
Nous nous proposons d'automatiser les preuves d'egalites sur les nombres reels dans le systeme Coq en utilisant la theorie des corps commutatifs. L'idee de l'algorithme consiste a se debarrasser des inverses an de pouvoir se brancher sur la procedure de decision deja existante sur les anneaux abeliens (Ring). L'elimination des inverses se fait de maniere completement reexive et la reexion est realisee au moyen d'un nouveau langage de tactiques integre au systeme Coq (version V7). Nous pensons etendre cette tactique a tous les corps commutatifs bien qu'actuellement, seuls les nombres reels soient concernes.
This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the official …
This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the official published account of the now completed Flyspeck project.
We define a class of ranked tree automata TABG generalizing both the tree automata with local tests between brothers of Bogaert and Tison (1992) and with global equality and disequality …
We define a class of ranked tree automata TABG generalizing both the tree automata with local tests between brothers of Bogaert and Tison (1992) and with global equality and disequality constraints (TAGED) of Filiot et al. (2007). TABG can test for equality and disequality modulo a given flat equational theory between brother subterms and between subterms whose positions are defined by the states reached during a computation. In particular, TABG can check that all the subterms reaching a given state are distinct. This constraint is related to monadic key constraints for XML documents, meaning that every two distinct positions of a given type have different values. We prove decidability of the emptiness problem for TABG. This solves, in particular, the open question of the decidability of emptiness for TAGED. We further extend our result by allowing global arithmetic constraints for counting the number of occurrences of some state or the number of different equivalence classes of subterms (modulo a given flat equational theory) reaching some state during a computation. We also adapt the model to unranked ordered terms. As a consequence of our results for TABG, we prove the decidability of a fragment of the monadic second order logic on trees extended with predicates for equality and disequality between subtrees, and cardinality.
Bishop's informal set theory is briefly discussed and compared to Lawvere's Elementary Theory of the Category of Sets (ETCS). We then present a constructive and predicative version of ETCS, whose …
Bishop's informal set theory is briefly discussed and compared to Lawvere's Elementary Theory of the Category of Sets (ETCS). We then present a constructive and predicative version of ETCS, whose standard model is based on the constructive type theory of Martin-Lof. The theory, CETCS, provides a structuralist foundation for constructive mathematics in the style of Bishop.
We define a notion of weak ω-category internal to a model of Martin-Löf's type theory, and prove that each type bears a canonical weak ω-category structure obtained from the tower …
We define a notion of weak ω-category internal to a model of Martin-Löf's type theory, and prove that each type bears a canonical weak ω-category structure obtained from the tower of iterated identity types over that type. We show that the ω-categories arising in this way are in fact ω-groupoids.
This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing …
This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing the Hofmann-Streicher groupoid model of Martin-Loef type theory.
We implement in the formal language of homotopy type theory a new set of axioms called cohesion. Then we indicate how the resulting cohesive homotopy type theory naturally serves as …
We implement in the formal language of homotopy type theory a new set of axioms called cohesion. Then we indicate how the resulting cohesive homotopy type theory naturally serves as a formal foundation for central concepts in quantum gauge field theory. This is a brief survey of work by the authors developed in detail elsewhere.
The elementary functions (sine, cosine, exponentials, logarithms . . . ) are the most commonly used mathematical functions. Computing them quickly and accurately is a major goal in computer arithmetic
The elementary functions (sine, cosine, exponentials, logarithms . . . ) are the most commonly used mathematical functions. Computing them quickly and accurately is a major goal in computer arithmetic