24 found
Sort by:
  1. Thierry Coquand & Giovanni Sambin (forthcoming). Preface of Special Issue on Formal Topology. Annals of Pure and Applied Logic.
    Direct download  
     
    My bibliography  
     
    Export citation  
  2. Thierry Coquand (2013). About Goodmanʼs Theorem. Annals of Pure and Applied Logic 164 (4):437-442.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  3. Andrej Bauer, Thierry Coquand, Giovanni Sambin & Peter M. Schuster (2012). Preface. Annals of Pure and Applied Logic 163 (2):85-86.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  4. Thierry Coquand, Erik Palmgren & Bas Spitters (2011). Metric Complements of Overt Closed Sets. Mathematical Logic Quarterly 57 (4):373-378.
    No categories
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  5. Stefano Berardi, Thierry Coquand & Susumu Hayashi (2010). Games with 1-Backtracking. Annals of Pure and Applied Logic 161 (10):1254-1269.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  6. Thierry Coquand (2009). Space of Valuations. Annals of Pure and Applied Logic 157 (2):97-109.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  7. Thierry Coquand, Type Theory. Stanford Encyclopedia of Philosophy.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  8. Thierry Coquand & Henri Lombardi (2008). A Note on the Axiomatisation of Real Numbers. Mathematical Logic Quarterly 54 (3):224-228.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  9. Thierry Coquand & L. Henri Lombardi (2008). A Note on the Axiomatisation of Real Numbers. Mathematical Logic Quarterly 54 (3):224-228.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  10. Bernhard Banaschewski, Thierry Coquand & Giovanni Sambin (2006). Preface. Annals of Pure and Applied Logic 137 (1-3):1-2.
    No categories
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  11. Thierry Coquand & Bas Spitters (2005). A Constructive Proof of the Peter‐Weyl Theorem. Mathematical Logic Quarterly 51 (4):351-359.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  12. Thierry Coquand (2004). About Brouwer's Fan Theorem. Revue Internationale de Philosophie 230:483-489.
    No categories
     
    My bibliography  
     
    Export citation  
  13. Sara Negri, Jan von Plato & Thierry Coquand (2004). Proof-Theoretical Analysis of Order Relations. Archive for Mathematical Logic 43 (3):297-309.
    A proof-theoretical analysis of elementary theories of order relations is effected through the formulation of order axioms as mathematical rules added to contraction-free sequent calculus. Among the results obtained are proof-theoretical formulations of conservativity theorems corresponding to Szpilrajn’s theorem on the extension of a partial order into a linear one. Decidability of the theories of partial and linear order for quantifier-free sequents is shown by giving terminating methods of proof-search.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  14. Thierry Coquand, Giovanni Sambin, Jan Smith & Silvio Valentini (2003). Inductively Generated Formal Topologies. Annals of Pure and Applied Logic 124 (1-3):71-106.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  15. Thierry Coquand & Erik Palmgren (2002). Metric Boolean Algebras and Constructive Measure Theory. Archive for Mathematical Logic 41 (7):687-704.
    This work concerns constructive aspects of measure theory. By considering metric completions of Boolean algebras – an approach first suggested by Kolmogorov – one can give a very simple construction of e.g. the Lebesgue measure on the unit interval. The integration spaces of Bishop and Cheng turn out to give examples of such Boolean algebras. We analyse next the notion of Borel subsets. We show that the algebra of such subsets can be characterised in a pointfree and constructive way by (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  16. Thierry Coquand & Erik Palmgren (2000). Intuitionistic Choice and Classical Logic. Archive for Mathematical Logic 39 (1):53-74.
    . The effort in providing constructive and predicative meaning to non-constructive modes of reasoning has almost without exception been applied to theories with full classical logic [4]. In this paper we show how to combine unrestricted countable choice, induction on infinite well-founded trees and restricted classical logic in constructively given models. These models are sheaf models over a $\sigma$ -complete Boolean algebra, whose topologies are generated by finite or countable covering relations. By a judicious choice of the Boolean algebra we (...)
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  17. Thierry Coquand, Sara Sadocco, Giovanni Sambin & Jan M. Smith (2000). Formal Topologies on the Set of First-Order Formulae. Journal of Symbolic Logic 65 (3):1183-1192.
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  18. Thierry Coquand (1999). A Boolean Model of Ultrafilters. Annals of Pure and Applied Logic 99 (1-3):231-239.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  19. Stefano Berardi, Marc Bezem & Thierry Coquand (1998). On the Computational Content of the Axiom of Choice. Journal of Symbolic Logic 63 (2):600-622.
    We present a possible computational content of the negative translation of classical analysis with the Axiom of (countable) Choice. Interestingly, this interpretation uses a refinement of the realizability semantics of the absurdity proposition, which is not interpreted as the empty type here. We also show how to compute witnesses from proofs in classical analysis of ∃-statements and how to extract algorithms from proofs of ∀∃-statements. Our interpretation seems computationally more direct than the one based on Godel's Dialectica interpretation.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  20. Thierry Coquand (1998). Two Applications of Boolean Models. Archive for Mathematical Logic 37 (3):143-147.
    Semantical arguments, based on the completeness theorem for first-order logic, give elegant proofs of purely syntactical results. For instance, for proving a conservativity theorem between two theories, one shows instead that any model of one theory can be extended to a model of the other theory. This method of proof, because of its use of the completeness theorem, is a priori not valid constructively. We show here how to give similar arguments, valid constructively, by using Boolean models. These models are (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  21. Thierry Coquand (1997). Minimal Invariant Spaces in Formal Topology. Journal of Symbolic Logic 62 (3):689-698.
  22. Thierry Coquand (1995). A Semantics of Evidence for Classical Arithmetic. Journal of Symbolic Logic 60 (1):325-337.
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  23. Thierry Coquand (1992). An Intuitionistic Proof of Tychonoff's Theorem. Journal of Symbolic Logic 57 (1):28-32.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation