Sciweavers

TYPES
2000
Springer
14 years 3 months ago
An Inductive Version of Nash-Williams' Minimal-Bad-Sequence Argument for Higman's Lemma
Higman's lemma has a very elegant, non-constructive proof due to Nash-Williams [NW63] using the so-called minimal-bad-sequence argument. The objective of the present paper is ...
Monika Seisenberger
TYPES
2000
Springer
14 years 3 months ago
A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals
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 (constructiv...
Herman Geuvers, Freek Wiedijk, Jan Zwanenburg
TYPES
2000
Springer
14 years 3 months ago
Constructive Reals in Coq: Axioms and Categoricity
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 (Fundamenta...
Herman Geuvers, Milad Niqui
TYPES
2000
Springer
14 years 3 months ago
A Tour with Constructive Real Numbers
Abstract. The aim of this work is to characterize constructive real numbers through a minimal axiomatization. We introduce, discuss and justify 16 constructive axioms. Then we addr...
Alberto Ciaffaglione, Pietro Di Gianantonio
TYPES
2000
Springer
14 years 3 months ago
Executing Higher Order Logic
We report on the design of a prototyping component for the theorem prover Isabelle/HOL. Specifications consisting of datatypes, recursive functions and inductive definitions are co...
Stefan Berghofer, Tobias Nipkow
TYPES
2000
Springer
14 years 3 months ago
Formalizing the Halting Problem in a Constructive Type Theory
We present a formalization of the halting problem in Agda, a language based on Martin-L
Kristofer Johannisson
TYPES
2000
Springer
14 years 3 months ago
Collection Principles in Dependent Type Theory
We introduce logic-enriched intuitionistic type theories, that extend intuitionistic dependent type theories with primitive judgements to express logic. By adding type theoretic ru...
Peter Aczel, Nicola Gambino