We present here a new extraction mechanism for the Coq proof assistant [17]. By extraction,
we mean automatic generation of functional code from Coq proofs, in order to produce …

Ensemble is a group communication system that demonstrably achieves a wide range of
goals. It is a general-purpose communication system intended for constructing reliable …

In this paper, we introduce a new type system, the Implicit Calculus of Constructions, which
is a Curry-style variant of the Calculus of Constructions that we extend by adding an …

Recent work on higher-dimensional type theory has explored connections between Martin-
Löf type theory, higher-dimensional category theory, and homotopy theory. These …

This thesis is concerned with the formalization of mathematics in the proof assistant Coq, in
particular the formalization of Bishop's constructive development of Real Analysis. In order to …

We study model checking for a first-order linear-time temporal logic. We present the
computation model: abstract description of state machines (ASMs), in which data and data …

The implicit universe hierarchy implemented in proof assistants such as Coq and Lego,
although really needed, is painful, both for the implementer and the user: it interacts badly …

This manual is a reference manual for version 5 of the Nuprl proof development system. As
the Nuprl system is constantly under development, this manual will always be incomplete. In …

I describe the implementation of two complete decision procedures for integer Presburger
arithmetic in the HOL theorem-proving system. The first procedure is Cooper's algorithm, the …

Reflection is the ability of some entity to describe itself. In a logical context, it is the ability of a
logic to reason about itself. Reflection is, therefore, placed at the core of meta-mathematics …