1 Introduction In this note, we show the inconsistency of a strong version of classical logic inthe type theory of Coq. More precisely, we show that from the assumption 8A:Prop{A} + {~A}, we can...
Degrees of Undecidability in Rewriting (2009)
Endrullis, Joerg, Geuvers, Herman, Zantema, Hans
Undecidability of various properties of first order term rewriting systems is well-known. An undecidable property can be classified by the complexity of the formula defining it. This gives rise to a...
An Interactive Algebra Course with Formalised Proofs and Definitions (2009)
Andrea Asperti, Herman Geuvers, Iris Loeb, Lionel Elie Mamane, Claudio Sacerdoti-coen
Abstract. We describe a case-study of the application of web-technology (Helm [2]) to create web-based didactic material out of a repository of formal mathematics (C-CoRN [5]), using the structure of...
LFM 2004 Preliminary Version A logical framework with explicit conversions Abstract (2008)
The type theory λP corresponds to the logical framework LF. In this paper we present λH, a variant of λP where convertibility is not implemented by means of the customary conversion rule, but...
Abstract. We study various well-known schemes for defining inductive and co-inductive types from a categorical perspective. Categorically, an inductive type is just an initial algebra and a...
Constructive Reals in Coq: Axioms and Categoricity (2008)
We describe a construction of the real numbers carried out in the Coq proof assistant. The basis is a set of axioms for the constructive real numbers as used in the FTA (Fundamental Theorem of...
C-CoRN, the Constructive Coq Repository at (2008)
Luís Cruz-filipe, Herman Geuvers, Freek Wiedijk
Nijmegen. It consists of a library of constructive algebra and analysis, formalized in the theorem prover Coq. In this paper we explain the structure, the contents and the use of the library....
An Interactive Algebra Course with Formalised Proofs and Definitions (2008)
Andrea Asperti, Herman Geuvers, Iris Loeb, Lionel Elie Mamane, Claudio Sacerdoti-coen
Abstract. We describe a case-study of the application of web-technology (Helm [2]) to create web-based didactic material out of a repository of formal mathematics (C-CoRN [5]), using the structure of...
Abstract. Deduction graphs [3] provide a formalism for natural deduction, where the deductions have the structure of acyclic directed graphs with boxes. The boxes are used to restrict the scope of...
An Interactive Algebra Course with Formalised Proofs and Definitions (2008)
Andrea Asperti, Herman Geuvers, Iris Loeb, Lionel Elie Mamane, Claudio Sacerdoti-coen
Abstract. We describe a case-study of the application of web-technology (Helm [0]) to create web-based didactic material out of a repository of formal mathematics (C-CoRN [0]), using the structure of...
An Interactive Algebra Course with Formalised Proofs and Definitions (2008)
Andrea Asperti, Herman Geuvers, Iris Loeb, Lionel Elie Mamane, Claudio Sacerdoti-coen
Abstract. We describe a case-study of the application of web-technology (Helm [2]) to create web-based didactic material out of a repository of formal mathematics (C-CoRN [5]), using the structure of...
C-CoRN, the Constructive Coq Repository at (2008)
Abstract. We present C-CoRN, the Constructive Coq Repository at Nijmegen. It consists of a library of constructive algebra and analysis, formalized in the theorem prover Coq. In this paper we explain...
LFM 2004 Preliminary Version A logical framework with explicit conversions Abstract (2008)
The type theory λP corresponds to the logical framework LF. In this paper we present λH, a variant of λP where convertibility is not implemented by means of the customary conversion rule, but...
Rewriting for Fitch style natural deductions (2008)
Abstract. Logical systems in natural deduction style are usually presented in the Gentzen style. A different definition of natural deduction, that corresponds more closely to proofs in ordinary...
Herman Geuvers, Y Pollack, Freek Wiedijk
We describe a framework of algebraic structures in the proof assistant Coq. We have developed this framework as part of the FTA project in Nijmegen, in which a constructive proof of the Fundamental...
C-CoRN, the Constructive Coq Repository at Nijmegen (2008)
Luís Cruz-filipe, Herman Geuvers, Freek Wiedijk
We present C-CoRN, the Constructive Coq Repository at Nijmegen. It consists of a mathematical library of constructive algebra and analysis formalized in the theorem prover Coq. We explain the...
(In)consistency of extensions of Higher Order Logic and Type Theory (2008)
Abstract. It is well-known, due to the work of Girard and Coquand, that adding polymorphic domains to higher order logic, HOL, or its type theoretic variant λHOL, renders the logic inconsistent....
The Logic and Mathematics of Occasion Sentences (2007)
Venanzio Capretta, Herman Geuvers
The prime purpose of this paper is to contribute to the development of an adequate logic of occasion sentences and a mathematical (Boolean) foundation for such a logic, thus preparing the ground for...
. We describe a method for constructing a model of second order dependent type theory out of a model of classical second order predicate logic. Apart from the construction being of interest by...
Olga Caprotti, Herman Geuvers, Martijn Oostdijk
Abstract. This paper deals with the problem of generating interactive natural language documents based on formal mathematics. It describes how formal mathematical developments, carried out in the...
Chapter 1 Proof-assistants using Dependent Type Systems (2007)
Henk Barendregt, Herman Geuvers
2 Type-theoretic notions for proof checking........................ 5 2.1 Proof checking mathematical statements...................... 5
Skeleton for the Proof development leading to the Fundamental Theorem of Algebra (2007)
Herman Geuvers, Y Pollack, Freek Wiedijk, Jan Zwanenburg
A basic ingredient of constructive real numbers is the apartness relation #. This is a constructive version of the (classical) inequality on reals: two real numbers are apart if it can positively be...
In this note, we show the inconsistency of a strong version of classical logic in the type theory of Coq. More precisely, we show that from the assumption
A Constructive Algebraic Hierarchy in Coq (2007)
Herman Geuvers, Y Pollack, Freek Wiedijk
We describe a framework of algebraic structures in the proof assistant Coq. We have developed this framework as part of the FTA project in Nijmegen, in which a constructive proof of the Fundamental...
C-CoRN, the Constructive Coq Repository at Nijmegan (2007)
We present C-CoRN, the Constructive Coq Repository at Nijmegen. It consists of a library of constructive algebra and analysis, formalized in the theorem prover Coq. In this paper we explain the...
met dank aan het Discrete Wiskunde dictaat van Wim Gielen Contents (2006)
1.1 Formele taal en natuurlijke taal.......................... 1
Herman Geuvers, Milad Niqui, Bas Spitters, Freek Wiedijk
In the present paper, we will discuss various aspects of computable/constructive analysis, namely semantics, proofs and computations. We will present some of the problems and solutions of exact real...
Herman Geuvers, Milad Niqui, Bas Spitters, Freek Wiedijk
In the present paper, we will discuss various aspects of computable/constructive analysis, namely semantics, proofs and computations. We will present some of the problems and solutions of exact real...
Herman Geuvers, Milad Niqui, Bas Spitters, Freek Wiedijk
In the present paper, we will discuss various aspects of computable/constructive analysis, namely semantics, proofs and computations. We will present some of the problems and solutions of exact real...
A Document-Oriented Coq Plugin for TEXmacs (2006)
Herman Geuvers, Lionel Elie Mamane
This article discusses the integration of the authoring of a mathematical document with the formalisation of the mathematics contained in that document. To achieve this we have started the...
The algebraic hierarchy of the FTA Project (2002)
Herman Geuvers, Y Pollack, Freek Wiedijk, Jan Zwanenburg
Abstract. We describe a framework for algebraic expressions for the proof assistant Coq. This framework has been developed as part of the FTA project in Nijmegen, in which a complete proof of the...
The algebraic hierarchy of the FTA Project (2002)
Herman Geuvers, Y Pollack, Freek Wiedijk, Jan Zwanenburg
Abstract. We describe a framework for algebraic expressions for the proof assistant Coq. This framework has been developed as part of the FTA project in Nijmegen, in which a complete proof of the...
Open Proofs and Open Terms: A Basis for Interactive Logic Herman Geuvers (2002)
And Gueorgui Jojgov, Herman Geuvers, Gueorgui I. Jojgov
When proving a theorem, one makes intermediate claims, leaving parts temporarily unspecified. These `open' parts may be proofs but also terms. In interactive theorem proving systems, one...
Open proofs and open terms: a basis for interactive logic (2002)
Abstract. In the process of interactive theorem proving one often works with incomplete higher order proofs. In this paper we address the problem of giving a correctness criterion for these...
A constructive proof of the Fundamental Theorem of Algebra without using the rationals (2001)
Herman Geuvers, Freek Wiedijk, Jan Zwanenburg
Abstract. In the FTA project in Nijmegen we have formalized a constructive proof of the Fundamental Theorem of Algebra. In the formalization, we have rst dened the (constructive) algebraic hierarchy...
A constructive proof of the Fundamental Theorem of Algebra without using the rationals (2001)
Herman Geuvers, Freek Wiedijk, Jan Zwanenburg
Abstract. In the FTA project in Nijmegen we have formalized a constructive proof of the Fundamental Theorem of Algebra. In the formalization, we have first defined the (constructive) algebraic...
Skeleton for the Proof development leading to the Fundamental Theorem of Algebra (2000)
Herman Geuvers, Randy Pollack, Y Pollack, Freek Wiedijk, Jan Zwanenburg
13.97> if its negation is the equality, i.e. :(a # b) $ a = b for all a; b. Fact 1.2 The negation of an apartness relation on S is an equivalence relation on S which is stable, i.e. :::(a # b) !...
Proof by Computation in the Coq system (2000)
Martijn Oostdijk, Herman Geuvers
In informal mathematics, statements involving computations are seldom proved. Instead, it is assumed that readers of the proof can carry out the computations on their own. However, when using an...
Skeleton for the Proof development leading to the Fundamental Theorem of Algebra (2000)
Herman Geuvers, Y Pollack, Freek Wiedijk, Jan Zwanenburg
Definition 1.1 A binary relation # on a set S is an apartness relation if
Safe proof checking in type theory with y (1999)
Abstract. We present an extension of type theory with a xed point combinator Y. We are particularly interested in using this Y for doing unbounded proof search in the proof system. Therefore we treat...
Safe Proof Checking in Type Theory with Y (1999)
Herman Geuvers, Erik Poll, Jan Zwanenburg
. We present an extension of type theory with a fixed point combinator Y . We are particularly interested in using this Y for doing unbounded proof search in the proof system. Therefore we treat in...
Herman Geuvers, ERIK BARENDSEN
this paper has appeared as (Harper et al. 1993).) As a matter of fact, they were the rst to actually state the problem. To prove adequacy of an encoding (Harper et al. 1987) devise a general...
Proof-assistants using Dependent Type Systems (1999)
Henk Barendregt, Herman Geuvers
Science and technology depend on true statements. Most of these are obtained via reasoning from experimental data using mathematics (models). Therefore the notion of proof that warrants correctness...
Proof-assistants using Dependent Type Systems (1999)
Henk Barendregt, Herman Geuvers
this article we will not attempt to describe all the dierent possible choices of type theories. Instead we want to discuss the main underlying ideas, with a special focus on the use of type theory as...
Explicit Substitution: on the Edge of Strong Normalization (1997)
We use the Recursive Path Ordering (RPO) technique of semantic labelling to show the Preservation of Strong Normalization (PSN) property for several calculi of explicit substitution. Preservation of...
The Barendregt Cube with Definitions and Generalised Reduction (1997)
Roel Bloo, Fairouz Kamareddine, Rob Nederpelt, Bob Constable, Herman Geuvers, Stefan Khars, ...
In this paper, we propose to extend the Barendregt Cube by generalising fi-reduction and by adding definition mechanisms. Generalised reduction allows contracting more visible redexes than usual, and...
A Semantics for a fine λ-calculus with de Bruijn indices (1997)
Rob Nederpelt, Herman Geuvers, Jeroen Krabbendam, Erik Poll, Peter Rodenburgh, Fairouz Kamareddine, ...
Most of us who have worked with named variables in the -calculus must have noticed how sticky such variables can be. The problem is, that named variables play a very demanding role in the most basic...
Modular Properties of Algebraic Type Systems (1996)
. We introduce the framework of algebraic type systems, a generalisation of pure type systems with higher order rewriting `a la JouannaudOkada, and initiate a generic study of the modular properties...
Modularity of Strong Normalization in the Algebraic-lambda-cube (1996)
Uperieure S Ormale, N Ecole, The Algebraic--cube, Franco Barbanera, Franco Barbanera, Maribel Fernández, ...
In this paper we present the algebraic-lambda-cube, an extension of Barendregt's lambda-cube with first- and higher-order algebraic rewriting. We show that strong normalization is a modular...
. We introduce a type-theoretical framework in which canonical term rewriting systems can be represented faithfully both from the logical and the computational points of view. The framework is based...
Modular Properties of Algebraic Pure Type Systems (1996)
. We introduce the framework of algebraic pure type systems, a generalisation of pure type systems with higher order rewriting `a la Jouannaud-Okada, and initiate a generic study of the modular...
Explicit Substitution: on the Edge of Strong Normalisation (1995)
We use the Recursive Path Ordering (RPO) technique of semantic labelling to show the Preservation of Strong Normalisation (PSN) property for several calculi of explicit substitution. Preservation of...
A short and flexible proof of Strong Normalization for the Calculus of Constructions (1994)
this paper can still go through (with slightly more technical effort) in case one can distinguish cases according to whether a specific subterm is a type or kind in a fixed context. The other...
Modularity of Strong Normalization and Confluence in the algebraic-lambda-cube (1994)
Franco Barbanera, Maribel Fernández, Herman Geuvers
In this paper we present the algebraic--cube, an extension of Barendregt's -cube with first- and higherorder algebraic rewriting. We show that strong normalization is a modular property of all...
Informal Proceedings Of The 1993 Workshop On Types For Proofs And Programs, Nijmegen (1993)
Clauses : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 375 iii Foreword This document is the preliminary proceedings of the workshop of the Esprit Basic Research...
Logics and Type Systems (1993)
Jan Herman Geuvers, Herman Geuvers, Cover Jean, Bernard Koeman, Den Haag, ...
from the last declaration in \Delta (which is p:'). (oe-E) In fact the ([\Theta]) is not exactly the ([\Theta]) that is found by induction. Possibly some of the free variables in ([\Theta]) are...
The Calculus of Constructions and Higher Order Logic (1992)
The Calculus of Constructions (CC) ([Coquand 1985]) is a typed lambda calculus for higher order intuitionistic logic: proofs of the higher order logic are interpreted as lambda terms and formulas as...
Inductive and Coinductive types with Iteration and Recursion (1992)
We study (extensions of) simply and polymorphically typed lambda calculus from a point of view of how iterative and recursive functions on inductive types are represented. The inductive types can...
The Church-Rosser Property for . . . (1992)
In this paper we investigate the Church-Rosser property (CR) for Pure Type Systems with fij- reduction. For Pure Type Systems with only fi- reduction, CR on well typed terms follows immediately from...