We propose a new language for writing programs with dependent types on top of the Coq
proof assistant. This language permits to establish a phase distinction between writing and …

In this paper, we show how Miquel's Implicit Calculus of Constructions (ICC) can be used as
a programming language featuring dependent types. Since this system has an undecidable …

This work is about formalizing models of various type theories of the Calculus of
Constructions family. Here we focus on set theoretical models. The long-term goal is to build …

In order to avoid well-know paradoxes associated with self-referential definitions, higher-
order dependent type theories stratify the theory using a countably infinite hierarchy of …

Cet article prend appui, en en développant les principales orientations, sur un programme
consacré aux «mots de la ville»(la ville en tant qu'entité et les territoires qui la composent). Il …

We investigate how projective plane geometry can be formalized in a proof assistant such as
Coq. Such a formalization increases the reliability of textbook proofs whose details and …

The paper describes the new kernel for the Calculus of Inductive Constructions (CIC)
implemented inside the Matita Interactive Theorem Prover. The design of the new kernel has …

Congruence closure procedures are used extensively in automated reasoning and are a
core component of most satisfiability modulo theories solvers. However, no known …

We present a type theory with some proof-irrelevance built into the conversion rule. We
argue that this feature is useful when type theory is used as the logical formalism underlying …

We present a set-theoretic, proof-irrelevant model for Calculus of Constructions (CC) with
predicative induction and judgmental equality in Zermelo-Fraenkel set theory with an axiom …