Metric complements of overt closed sets (2009)
Coquand, Thierry, Palmgren, Erik, Spitters, Bas
We show that the set of points of an overt closed subspace of a metric completion of a Bishop-locally compact metric space is located. Consequently, if the subspace is, moreover, compact, then its...
Introduction About Stone’s notion of Spectrum (2008)
The goal of this paper is to analyse two remarkable notes by Stone [StoI, StoII]. Both describe a compact space in term of some algebra of functions over this space. This description
Constructive Gelfand duality for C*-algebras (2008)
Coquand, Thierry, Spitters, Bas
We present a constructive proof of Gelfand duality for C*-algebras by reducing the problem to Gelfand duality for real C*-algebras.
Integrals and Valuations (2008)
Coquand, Thierry, Spitters, Bas
We construct a homeomorphism between the compact regular locale of integrals on a Riesz space and the locale of (valuations) on its spectrum. In fact, we construct two geometric theories and show...
A NILREGULAR ELEMENT PROPERTY (2008)
Thierry Coquand, Henri Lombardi, Peter Schuster
Abstract. An element a of a commutative ring R is nilregular if and only if x is nilpotent whenever ax is nilpotent. More generally, an ideal I of R is nilregular if and only if x is nilpotent...
A logical approach to abstract algebra (2008)
Thierry Coquand, Henri Lombardi
Abstract. Recent work in constructive mathematics show that Hilbert’s program works for a large part of abstract algebra. Using in an essential way the ideas contained in the classical arguments,...
IOS Press A Logical Framework with Dependently Typed Records ∗ (2008)
Thierry Coquand, Chalmers Tekniska Högskola, Makoto Takeyama, Randy Pollack
Our long term goal is a system to formally represent complex structured mathematical objects, and proofs and computation on such objects; e.g. a foundational computer algebra system. Our approach is...
Carsten Schürmann (chair, Thierry Coquand, Dale Miller Inria, Carsten Schürmann, Andreas Abel, Jason Reed
Logical frameworks and meta-languages form a common substrate for representing, implementing, and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their...
We give an elementary and essentially self-contained proof 1 that a reduced ring R is seminormal if and only if the canonical map Pic R → Pic R[X] is an isomorphism, a theorem due to Swan [15],...
Geometric Hahn-Banach theorem (2008)
In [MP2] is proved in a constructive way the following result: a point x lies in a compact convex set K in a normed space if and only if it lies within any bound for K (a bound for K being...
Andreas Abel C, Thierry Coquand
Abstract. Martin-Löf’s Logical Framework is extended by strong Σ-types and presented via judgmental equality with rules for extensionality and surjective pairing. Soundness of the framework rules...
How to Define Measure of Borel Sets (2008)
One of the first definitions of measure, by Borel, provides an early example of generalised recursive definition of a function. It presented however an ambiguity problem.
A Topos Theoretic Fix Point Theorem (2007)
We present a fix point theorem that can be seen as an intuitionistic alternative to Bourbaki's lemma used in his presentation of Zorn's lemma [3]. Here however intuitionistic is taken in a...
HyperResolution and Stalmarck's method (2007)
We give an abstract presentation of Stalmarck's method, and explore some connections with
Metric boolean algrebras and constructive measure theory (2007)
Thierry Coquand, Erik Palmgren
In this paper, we analyse some aspects of measure theory from a constructive point of view. We present first a simple and direct way to define the algebra of Lebesgue measurable subsets (quotiented...
A Syntactical Proof Of The Marriage Lemma (2007)
. We give a proof of the classical Marriage Lemma [4] using completeness of hyperresolution. This argument is purely syntactical, and extends directly to the infinite case. As an application we give...
A Direct Proof of the Localic Hahn-Banach Theorem (2007)
Thierry Coquand Preliminary, Thierry Coquand
Using the notion of entailment relation [Sco74] we give a direct proof of the localic version of Hahn-Banach's theorem. 1 Introduction There are several examples of topological spaces naturally...
A Functional Programming View of Type Theory (2007)
Thorsten Altenkirch Thierry, Thierry Coquand
This paper suggests a method for the design of proof system based on type theory. We design first a partial type theory, which can be viewed as a functional programming language with dependent types...
Constructive Metric Completion Of Boolean Algebras (2007)
Thierry Coquand, Erik Palmgren
this paper, we analyse some aspects of measure theory from a constructive point of view. We present first a simple and direct way to define the algebra of Lebesgue measurable subsets (quotiented by...
A Representation Theorem for Stably Compact Spaces (2007)
Thierry Coquand Preliminary, Thierry Coquand
Introduction Motivated by a question of M. Escardo, we give a presentation of stably compact spaces and of compact regular spaces. 1 Information System We let ` be an entailment relation on a set of...
Inductive Definitions and Type Theory: An Introduction (2007)
Martin-Lof's type theory can be described as an intuitionistic theory of iterated inductive definitions developed in a framework of dependent types. It was originally intended to be a full-scale...
A Note on Formal Iterated Function Systems (2007)
Thierry Coquand Chalmers, Thierry Coquand
Introduction Edalat has introduced the notion of weakly hyperbolic iterated function systems [3] and showed that it allows for natural domain theoretic proofs (also for the probabilistic case). This...
Sequents, Frames, and Completeness (2007)
Thierry Coquand, Guo-qiang Zhang
. Entailment relations, originated from Scott, have been used for describing mathematical concepts constructively and for representing categories of domains. This paper gives an analysis of the...
Sequents, Frames, and Completeness (2007)
Thierry Coquand, Guo-qiang Zhang
. Entailment relations, originated from Scott, have been used for describing mathematical concepts constructively and for representing categories of domains. This paper gives an analysis of the...
Valuations and Dedekind's Prague Theorem (2007)
Thierry Coquand, Henrik Persson
To any field K we associate an entailment relation in the sense of Scott [12]. In this way we can interpret an abstract propositional theory representing a generic valuation ring of a field, and...
A Boolean Model of Ultrafilters (2007)
We introduce the notion of Boolean measure algebra. It can be described shortly using some standard notations and terminology. If B is any Boolean algebra, let B N denote the algebra of sequences...
A Formal Space of Paths (2007)
, April 1996 Introduction In general, a connected locally connected space may fail to be path-connected. This means that if X is a connected locally connected space, the map fl 7\Gamma! (fl(0);...
Formal Compact Hausdorff Spaces (2007)
Maximality Principle Let M be a commutative idempotent monoid with a zero element, that can equivalently be considered as a inf semi lattice with a greatest element 1 and a least element 0. We define...
ET SON APPLICATION A LA VERIFICATION (2007)
Suprieure De Lyon, Spcialit Informatique, De Systemes Communicants, Roberto Amadio, Roberto Amadio, ...
Thbse praparae k l'lcole normale suparieure de Lyon au sein du Laborat&re de l'informatique du paralldisme, Unita de Recherche Associae au CNRS No. 1398.
Thorsten Altenkirch, Thierry Coquand
Abstract. We give a nitary normalisation proof for the restriction of system F where we quantify only over rst-order type. As an application, the functions representable in this fragment are exactly...
HOW TO DEFINE MEASURE OF BOREL SETS (2007)
In [12] is presented a constructive definition of Borel subsets of Cantor space\Omega and their
Thierry Coquand, Giovanni Sambin, Silvio Valentini
Formal topology aims at developing general topology in intuitionistic and predicative mathematics. Many classical results of general topology have been already brought into the realm of constructive...
Compact spaces and distributive lattices (2007)
We give a general construction which associates a formal compact space to any distributive lattice. This construction is used to give a direct constructive proof of Tychonoff's and...
CONSTRUCTIVE BAIRE CATEGORY THEOREM (2007)
We recall the point-free definition of Borel sets in [?] of Cantor space. We define then what it means to be of empty interior, and we prove Baire category theorem for Cantor
Compact Spaces and Distributive Lattices (2007)
Introduction This note presents a general construction (theorem 2.1) connecting compact locales and distributive lattices. This allows us to reduce results about compactness of locales to theorems...
A Simple Proof of Stone-Weirstrass (2007)
We give a simple proof of Stone-Weierstrass theorem. This argument shows how to compute arbitrary approximation of the square root of an element in [0; 1] in any ordered ring with an element 1=2.
A Constructive Analysis of the Stone-Weierstrass Theorem (2007)
Thierry Coquand Version, Thierry Coquand
Introduction This note can be seen as a constructive comment on an older note of M.H. Stone [StII]. We give a simple, constructive localic proof of the Stone-Weierstrass theorem and a constructive...
A Logical Framework with Dependently Typed Records (2007)
Thierry Coquand, Randy Pollack, Y Pollack, Makoto Takeyama
this paper we propose an extension of Martin-Lof's logical framework [23, 19] with dependently typed records, and present the semantic fou;7 tion and the typechecking algorithm of ou r system....
Towards Constructive Homological Algebra in Type Theory (2007)
Coquand, Thierry, Spiwack, Arnaud
This paper reports on ongoing work on the project of representing the Kenzo system in type theory.
A Proof of Strong Normalisation Using Domain Theory (2007)
Coquand, Thierry, Spiwack, Arnaud
In 1961, Spector presented an extension of Gödel's system T by a new schema of definition called bar recursion. With this new schema, he was able to give an interpretation of Analysis, extending...
Towards Constructive Homological Algebra in Type Theory (2007)
Coquand, Thierry, Spiwack, Arnaud
This paper reports on ongoing work on the project of representing the Kenzo system in type theory.
A Proof of Strong Normalisation Using Domain Theory (2007)
Coquand, Thierry, Spiwack, Arnaud
In 1961, Spector presented an extension of Gödel's system T by a new schema of definition called bar recursion. With this new schema, he was able to give an interpretation of Analysis, extending...
Coherent logic How crucial is the use of non effective methods? Can we develop mathematics with only effective proofs?? Kronecker: in algebra the arguments should be effective “purity of...
A proof of strong normalisation using domain theory (2006)
Thierry Coquand, Chalmers Tekniska Högskola
U. Berger, [11] significantly simplified Tait’s normalisation proof for bar recursion [27], see also [9], replacing Tait’s introduction of infinite terms by the construction of a domain having...
A Nilregular Element Property (2006)
Coquand, Thierry, Lombardi, Henri, Schuster, Peter
An element or an ideal of a commutative ring is nilregular if and only if it is regular modulo the nilradical. We prove that if the ring is Noetherian, then every nilregular ideal contains a...
05021 Executive Summary -- Mathematics, Algorithms, Proofs (2006)
This workshop was the third MAP meeting, a continuation of the seminar "Verification and constructive algebra" held in Dagstuhl from 6 to 10 January 2003. The goal of these meetings is to bring...
05021 Abstracts Collection -- Mathematics, Algorithms, Proofs (2006)
Coquand, Thierry, Lombardi, Henri, Roy, Marie-Françoise
From 09.01.05 to 14.01.05, the Dagstuhl Seminar 05021 ``Mathematics, Algorithms, Proofs'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar,...
Certified mathematical hierarchies: the FoCal system. (2006)
Prevosto, Virgile, Coquand, Thierry, Lombardi, Henri, Roy, Marie-Franccoise
A Proof of Strong Normalisation using Domain Theory (2006)
Coquand, Thierry, Spiwack, Arnaud
U. Berger, significantly simplified Tait's normalisation proof for bar recursion, replacing Tait's introduction of infinite terms by the construction of a domain having the property that a term is...
A Proof of Strong Normalisation using Domain Theory (2006)
Coquand, Thierry, Spiwack, Arnaud
U. Berger, significantly simplified Tait's normalisation proof for bar recursion, replacing Tait's introduction of infinite terms by the construction of a domain having the property that a term is...
Abstract. We present a constructive proof of the Stone-Yosida representation theorem for Riesz spaces motivated by considerations from formal topology. This theorem is used to derive a representation...
Thierry Coquand, Krull Dimension, This Space Spec(l
Let L be a distributive lattice. The theory of prime filters of L is the theory
Abstract: We present a constructive proof of the Stone-Yosida representation theorem for Riesz spaces motivated by considerations from formal topology. This theorem is used to derive a representation...
Recent work in constructive algebra establishes experimentally that Hilbert’s program of elimination of ideal elements works for a large part of abstract algebra. We present an example. A logical...
About Stone's Notion of Spectrum (2003)
this paper is to analyse two remarkable notes by Stone [StI, StII] that both describe a compact space in term of some algebra of functions over this space. This description is intuitively in term of...
Abelian l-Groups, Generalised Reals and Open Locales (2003)
This is a summary of a discussion with Peter Schuster (march, 2003)
Thierry Coquand, Henri Lombardi
Hidden constructions in abstract algebra (3) Krull Dimension of distributive lattices and commutative rings
Modules as Dependently Typed Records (2002)
Thierry Coquand, Randy Pollack, Y Pollack, Makoto Takeyama
Syntax For expressions, we have fours categories: expressions, sorts, contexts and definitional context. The abstract syntax is e; a = e e j x j s j [x = e]e j [x : a]e j fx : age j e:x j !\Gamma? j...
Using the notion of entailment relation [Sco74] we give a simple proof of a basic result of Tarksi (1929) on the existence of an additive function over a monoid. 1 Introduction There are several...
About Stone's notion of Spectrum (2000)
Introduction Stone duality between Boolean algebra and compact totally disconnected spaces provides an algebraic and point-free presentation of a large class of topological spaces. A generalisation...
A Syntactical Proof Of The Marriage Lemma (2000)
. Y. Matiyasevich has found an interesting application of proof theory (especially, completeness of resolution and hyperresolution) to problems in discrete mathematics. In this note, we illustrate...
Inductive Solution of Borel's Measure Problem (2000)
this paper is to show the following.
1 Introduction We analyse the notion of Krull dimension of a commutative ring and of a distributive lattice. To any ring/distributive lattice we associate in an elementary way a distributive lattice...
Point-Free Characterisation of Borel Sets (2000)
Introduction We use the completness of propositional !-logic in order to give a point-free presentation of Borel subsets of Cantor space and of (0; 1): 1 oe-Completion of a Boolean algebra We recall...
Lewis Carroll, Gentzen and Entailment Relations (1999)
Introduction This note summarizes some remarks about entailment relations. Basically these are elementary facts about propositional logic, but I find it suggestive to formulate it in the simple...
Catarina Coquand, Thierry Coquand
Introduction We present our implementation AGDA of type theory. We limit ourselves in this presentation to a rather primitive form of type theory (dependent product with a simple notion of sorts)...
Invariant Measure on Compact Space (1999)
Introduction Let X be a compact space, and G a commutative group acting on X. It is well-known (Kakutani 's theorem) that there exists a G-invariant probablity measure on X: The formal...
To any commutative ring, we associate an entailment relation which describes its real spectrum [Joh82]. Introduction Johnstone gives an axiomatic description of the real spectrum of a commutative...
A Direct Proof of the Localic Hahn-Banach Theorem (1999)
Using the notion of entailment relation [Sco74] we give a direct proof of the localic version of Hahn-Banach's theorem. 1 Introduction There are several examples of topological spaces naturally...
Inductive Solution of Borel's Measure Problem (1999)
this paper is to show the following.
Intuitionistic Model Constructions and Normalization Proofs (1998)
We investigate semantical normalization proofs for typed combinatory logic and weak -calculus. One builds a model and a function `quote' which inverts the interpretation function. A...
Gröbner Bases in Type Theory (1998)
Thierry Coquand, Henrik Persson
We describe how the theory of Gröbner bases, an important part of computational algebra, can be developed within Martin-Löf's type theory. In particular, we aim for an integrated development...
Case Analysis, Variables and Parameters (1998)
Introduction We explain how the formal description of the spectrum of a ring with its constructible topology, which is a boolean algebra associated to this ring, can be used to formalise the notion...
Introduction Gavin Wraith has raised the question of a localic treatement of the notion of Haar measure on locally compact Haussdorf groups. This is an example of an object for which one can prove...
Integrated Development of Algebra in Type Theory (1998)
Thierry Coquand, Henrik Persson
We present the project of developing computational algebra inside type theory in an integrated way. As a first step towards this, we present direct constructive proofs of Dickson's lemma and...
Entailment Relations and Distributive Lattices (1998)
Jan Cederquist, Thierry Coquand
. To any entailment relation [Sco74] we associate a distributive lattice. We use this to give a construction of the product of lattices over an arbitrary index set, of the Vietoris construction, of...
Transfinite Games - To the infinite and beyond! (1998)
Stefano Berardi, Thierry Coquand
this paper. Let I be a well-ordered set, that is a set with a total order relation such that any non empty subset has a least element. I modelizes the set (possibly infinite) of turns of the play. We...
Formal Topologies on the Set of First-Order Formulae (1998)
Thierry Coquand, Sara Sadocco, Giovanni Sambin, Jan M. Smith
this paper that the question has a simple negative answer. This raised further natural questions on what can be said about the points of these two topologies; we give some answers. The observation...
A Proof-Theoretical Investigation of Zantema's Problem (1998)
Thierry Coquand, Henrik Persson
. We present a concrete example of how one can extract constructive content from a non--constructive proof. The proof investigated is a termination proof of the string--rewriting system 1100 !...
Course notes in typed lambda calculus (1997)
Since quite good books [12, 9] or review article [3, 10, 6, 18] are available on typed lambda calculi, these notes limit themselves to some historical remarks and some points that I consider...
Introduction In probability theory, for continuous stochastic processes, one may have to consider products of spaces over an index set such as [0; 1] or [0; +1[. Thus, one is lead to consider product...
A Note on the Open Induction Principle (1997)
Introduction In the reference [2], I described a possible point-free interpretation of a new induction principle, the open induction principle, that was use by J.C. Raoult for a new presentation of...
Two Applications of Boolean Models (1997)
Introduction This short note presents two simple applications of the notion of boolean models for first-order classical logic. One application is a constructive proof of the following conservativity...
A Topological Model of Ultrafilters (1997)
this paper is what should be a formal description of non separable topological spaces. This question seems to apply as well to the description of Stone-Cech compactification described in [2]. This...
Intuitionistic Choice and Classical Logic (1997)
Thierry Coquand, Erik Palmgren
this paper we show how to combine the unrestricted countable choice, induction on infinite well-founded trees and restricted classical logic in a constructively given model. For readers faniliar with...
The Hahn-Banach Theorem in Type Theory (1997)
Jan Cederquist, Thierry Coquand, Sara Negri
We give the basic deønitions for pointfree functional analysis and present constructive proofs of the Alaoglu and Hahn-Banach theorems in the setting of formal topology. 1 Introduction We present...
Computational Content of Classical Logic (1996)
Thierry Coqua Nd, Thierry Coquand
Introduction This course is an introduction to the research trying to connect the proof theory of classical logic and computer science. We omit important and standard topics, among them the...
Proof Theory in Type Theory (1996)
Introduction The negative translation provides a general way to make constructive sense of some non effective reasoning. However this method has some limitations. It does not work in presence of the...
Computational Content of Classical Logic (1996)
This course is an introduction to the research trying to connect the proof theory of classical logic and computer science. We omit important and standard topics, among them the connection between the...
An Algorithm for Type-Checking Dependent Types (1996)
We present a simple type-checker for a language with dependent types and let expressions, with a simple proof of correctness. Introduction Type Theory provides an interesting approach to the problem...
Minimal Invariant Spaces in Formal Topology (1996)
this paper, we extend our analysis to the case where X is a boolean space, that is compact totally disconnected. In such a case, we give a point-free formulation of the existence of a minimal...
Intuitionistic Model Constructions and Normalization Proofs (1996)
The traditional notions of strong and weak normalization refer to properties of a binary reduction relation. In this paper we explore an alternative approach to normalization, where we bypass the...
Formal Topology with Posets (1996)
Introduction We explore basic notions of formal topology with Dragalin's definition of formal spaces [1]. This definition appears also in the exercice 5, chapter IX of [3], as the notion of...
Formal Topology with Posets (1996)
Thierry Coquand Chalmers, Thierry Coquand
Introduction We explore basic notions of formal topology with Dragalin's de nition of formal spaces [1]. This de nition appears also in the exercice 5, chapter IX of [3], as the notion of...
An Application of Constructive Completeness. (1995)
this paper, we explore one possible effective version of this theorem, that uses topological models in a point-free setting, following Sambin [11]. The truth-values, instead of being simply booleans,...
On the computational content of the Axiom of Choice (1995)
Stefano Berardi, Marc Bezem, Thierry Coquand
We present a possible computational content of the negative translation of classical analysis with the Axiom of Choice. Our interpretation seems computationally more direct than the one based on...
Type Theory and Programming (1994)
Thierry Coquand, Bengt Nordström, Jan M. Smith, Björn Von Sydow
This paper gives an introduction to type theory, focusing on its recent use as a logical framework for proofs and programs. The first two sections give a background to type theory intended for the...
A-translation and Looping Combinators in Pure Type Systems (1994)
Thierry Coquand, Hugo Herbelin
We present here a generalization of A-translation to a class of Pure Type Systems. We apply this translation to give a direct proof of the existence of a looping combinator in a large class of...
Inductive Definitions and Type Theory: An Introduction (1994)
this paper also the quite elegant case notation for the definition of functions over data types. He also discussed the general method of structural induction for proving properties of programs which...
A New Paradox in Type Theory (1994)
this paper is to present a new paradox for Type Theory, which is a type-theoretic refinement of Reynolds' result [24] that there is no set-theoretic model of polymorphism. We discuss then one...
A proof of Higman's lemma by structural induction (1993)
Thierry Coquand, Daniel Fridlender
This paper gives an example of such an inductive proof for a combinatorial problem. While there exist other constructive proofs of Higman's lemma (see for instance [10, 14]), the present...
A constructive topological proof of van der Waerden's theorem (1993)
this paper was written, we became aware of the work [2, 15], which, in the quite different field of functional analysis, illustrates this common idea that localic methods can be used to find sharper...
Constructive Topology and Combinatorics (1992)
We present a method to extract constructive proofs from classical arguments proved by topogical means. Typically, this method will apply to the nonconstructive use of compactness in combinatorics,...
Pattern Matching with Dependent Types (1992)
Introduction This note deals with notation in type theory. The definition of a function by pattern matching is by now common, and quite important in practice, in functional programming languages (see...
Inheritance As Implicit Coercion (1991)
Val Breazu-tannen, Thierry Coquand, Carl A. Gunter, Andre Scedrov
. We present a method for providing semantic interpretations for languages with a type system featuring inheritance polymorphism. Our approach is illustrated on an extension of the language Fun of...
The paradox of trees in Type Theory (1991)
. We show how to represent a paradox similar to Russell's paradox in Type Theory with W -types and a type of all types, and how to use this in order to represent a fixed-point operator in such a...
Thierry Coquand, Jean Gallier, Le Chesnay Cedex
. We give a proof that all terms that type-check in the theory of constructions are strongly normalizing (under fi-reduction). The main novelty of this proof is that it uses a "Kripke-like"...
Domain Theoretic Models Of Polymorphism (1989)
Thierry Coquand, Inria Rocquencourt, Carl A. Gunter, Glynn Winskel
We give an illustration of a construction useful in producing and describing models of Girard and Reynolds' polymorphic -calculus. The key unifying ideas are that of a Grothendieck fibration and...
Newman's Lemma - a Case Study in Proof Automation and Geometric Logic (1988)
Yuri Gurevich, Marc Bezem, Thierry Coquand
Newman's Lemma states that a graph is confluent if it is locally confluent and has no infinite paths. Newman's Lemma requires essentially higher-order logic. We show that the induction step...
An Analysis of Girard's Paradox (1986)
this article is to present applications of the Burali-Forti paradox to some formal systems. The first such application is due to J.Y. Girard, who showed
A New Method for Establishing Conservativity of Classical Systems Over Their Intuitionistic Version
Thierry Coquand, Martin Hofmann
this paper we present such a method. Applied to I \Sigma
Infinite Objects in Type Theory
. We show that infinite objects can be constructively understood without the consideration of partial elements, or greatest fixedpoints, through the explicit consideration of proof objects. We...
Infinite Objects in Type Theory
We show that infinite objects can be constructively understood without the consideration of partial elements, or greatest fixed-points, through the explicit consideration of proof objects. We present...