Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory (2009)
Andreas Abel, Thierry Coqu, Peter Dybjer
Abstract. Type-checking algorithms for dependent type theories often rely on the interpretation of terms in some semantic domain of values when checking equalities. Here we analyze a version of...
On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory (2009)
Abstract. An algebraic presentation of Martin-Löf’s intuitionistic type theory is given which is based on the notion of a category with families with extra structure. We then present a...
An Implementation of Type:Type (2008)
Abstract. We present a denotational semantics of a type system with dependent types, where types are interpreted as finitary projections. We prove then the correctness of a type-checking algorithm...
Mathematical Logic Quarterly c ○ WILEY-VCH Verlag Berlin GmbH 2001 (2008)
Thierry Coqu, Bas Spitters, Bas Spitters
Abstract. We present a new and constructive proof of the Peter-Weyl theorem on the representations of compact groups. We use the Gelfand representation theorem for commutative C*-algebras to give a...
on the set of first-order formulae, J. Symbolic Logic 65 (2000), no. 3, 1183–1192. MR (2008)
Thierry Coqu, Sara Sadocco, Giovanni Sambin, Jan M. Smith, Formal Topologies, Thierry Coqu, ...
Stefano Berardi, Silvio Valentini, Thierry Coqu, Giovanni Sambin, Jan Smith, Silvio Valentini, ...
[3] Silvio Valentini, An elementary proof of strong normalization for intersection types, Arch.
INHERITANCE AS IMPLICIT COERCION 1 (2008)
Abstract. 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...
Jan Cederquist, Thierry Coqu, Sara Negri
Wegive 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
Verifying a semantic βη-conversion test for Martin-Löf type theory (2008)
Andreas Abel, Thierry Coqu, Peter Dybjer
Abstract. Type-checking algorithms for dependent type theories often rely on the interpretation of terms in some semantic domain of values when checking equalities. Here we analyze a version of...
A Finitary Subsystem of Polymorphic-calculus (2007)
Thorsten Altenkirch, Thierry Coqu
We give a finitary normalisation proof for the restriction of system F where we quantify only over first-order type. As an application, the functions representable in this fragment
Valuations and Dedekind's Prague Theorem (2007)
Thierry Coquand And, Thierry Coqu, 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...
On the Equational Theory of Non-Normalising Pure Type Systems (2007)
Pure Type Systems [1, 8] provide a generic framework for the description of
Connecting a logical framework to a first-order logic prover (extended version (2005)
Andreas Abel, Thierry Coqu, Ulf Norell
Abstract. We present one way of combining a logical framework and first-order logic. The logical framework is used as an interface to a first-order theorem prover. Its main purpose is to keep track...
Connecting a logical framework to a first-order logic prover (extended version (2005)
Andreas Abel, Thierry Coqu, Ulf Norell
Abstract. We present one way of combining a logical framework and first-order logic. The logical framework is used as an interface to a firstorder theorem prover. Its main purpose is to keep track of...
Connecting a logical framework to a first-order logic prover (extended version (2005)
Andreas Abel, Thierry Coqu, Ulf Norell
Abstract. We present one way of combining a logical framework and first-order logic. The logical framework is used as an interface to a firstorder theorem prover. Its main purpose is to keep track of...
Untyped algorithmic equality for Martin-Löf’s logical framework with surjective pairs (2005)
Abstract. An untyped algorithm to test βη-equality for Martin-Löf’s Logical Framework with strong Σ-types is presented and proven complete using a model of partial equivalence relations between...
Connecting a logical framework to a first-order logic prover (extended version (2005)
Andreas Abel, Thierry Coqu, Ulf Norell
Abstract. We present one way of combining a logical framework and first-order logic. The logical framework is used as an interface to a firstorder theorem prover. Its main purpose is to keep track of...
Connecting a logical framework to a first-order logic prover (extended version (2005)
Andreas Abel, Thierry Coqu, Ulf Norell
Abstract. We present one way of combining a logical framework and first-order logic. The logical framework is used as an interface to a first-order theorem prover. Its main purpose is to keep track...
Thierry Coqu, Giovanni Sambin, Jan Smith, Silvio Valentini
Formal topology is today an established topic in the development of constructive, that is intuitionistic and predicative, mathematics. Many classical results of general topology have been already...