Counting papers with at most 25 authors, so collaboration author lists do not stand in for the people here.
- Centre National de la Recherche ScientifiqueFR1.7k papers
- Centre Inria de SaclayFR364 papers
- École PolytechniqueFR306 papers
- Laboratoire Lorrain de Recherche en Informatique et ses ApplicationsFR300 papers
- École Normale Supérieure - PSLFR292 papers
- Sorbonne UniversitéFR291 papers
- École Normale Supérieure de LyonFR233 papers
- Centre Inria de l'Université Grenoble AlpesFR216 papers
- Université Paris-SaclayFR208 papers
- Université Grenoble AlpesFR204 papers
- Lyon 1 UniversitéFR191 papers
- Centre Inria d'Université Côte d'AzurFR183 papers
20 papers · 2 filters
On Completeness of Logical Relations for Monadic Types
Slawomir Lasota, David Nowak, Yu Zhang
Software security can be ensured by specifying and verifying security properties of software using formal methods with strong theoretical bases. In particular, programs can be mode…
Proof Nets and the Identity of Proofs
Lutz Strassburger
These are the notes for a 5-lecture-course given at ESSLLI 2006 in Malaga, Spain. The URL of the school is http://esslli2006.lcc.uma.es/ . This version slightly differs from the on…
Formalising Sylow's theorems in Coq
Laurent Thery
This report presents a formalisation of Sylow's theorems done in {\sc Coq}. The formalisation has been done in a couple of weeks on top of Georges Gonthier's {\sc ssreflect} \cite{…
Definitions by rewriting in the Calculus of Constructions
Frédéric Blanqui
This paper presents general syntactic conditions ensuring the strong normalization and the logical consistency of the Calculus of Algebraic Constructions, an extension of the Calcu…
Inductive types in the Calculus of Algebraic Constructions
Frédéric Blanqui
In a previous work, we proved that almost all of the Calculus of Inductive Constructions (CIC), which is the basis of the proof assistant Coq, can be seen as a Calculus of Algebrai…
An Isabelle formalization of protocol-independent secrecy with an application to e-commerce
Frédéric Blanqui
A protocol-independent secrecy theorem is established and applied to several non-trivial protocols. In particular, it is applied to protocols proposed for protecting the computatio…
A type-based termination criterion for dependently-typed higher-order rewrite systems
Frederic Blanqui
Several authors devised type-based termination criteria for ML-like languages allowing non-structural recursive calls. We extend these works to general rewriting and dependent type…
Extending the Calculus of Constructions with Tarski's fix-point theorem
Yves Bertot
We propose to use Tarski's least fixpoint theorem as a basis to define recursive functions in the calculus of inductive constructions. This widens the class of functions that can b…
LTL with the Freeze Quantifier and Register Automata
Stephane Demri, Ranko Lazic
A data word is a sequence of pairs of a letter from a finite alphabet and an element from an infinite set, where the latter can only be compared for equality. To reason about data…
On the freeze quantifier in Constraint LTL: decidability and complexity
Stéphane Demri, Ranko Lazic, David Nowak
Constraint LTL, a generalisation of LTL over Presburger constraints, is often used as a formal language to specify the behavior of operational models with constraints. The freeze q…
The Three Gap Theorem (Steinhauss Conjecture)
Micaela Mayero
We deal with the distribution of N points placed consecutively around the circle by a fixed angle of a. From the proof of Tony van Ravenstein, we propose a detailed proof of the St…
Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems
Frédéric Blanqui, Colin Riba
In a previous work, the first author extended to higher-order rewriting and dependent types the use of size annotations in types, a termination proof technique called type or size…
(HO)RPO Revisited
Frédéric Blanqui
The notion of computability closure has been introduced for proving the termination of the combination of higher-order rewriting and beta-reduction. It is also used for strengtheni…
Higher-Order Termination: from Kruskal to Computability
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
Termination is a major question in both logic and computer science. In logic, termination is at the heart of proof theory where it is usually called strong normalization (of cut el…
A Distribution Law for CCS and a New Congruence Result for the pi-calculus
Daniel Hirschkoff, Damien Pous
We give an axiomatisation of strong bisimilarity on a small fragment of CCS that does not feature the sum operator. This axiomatisation is then used to derive congruence of strong…
From Proof Nets to the Free *-Autonomous Category
Francois Lamarche, Lutz Strassburger
In the first part of this paper we present a theory of proof nets for full multiplicative linear logic, including the two units. It naturally extends the well-known theory of unit-…
Affine functions and series with co-inductive real numbers
Yves Bertot
We extend the work of A. Ciaffaglione and P. Di Gianantonio on mechanical verification of algorithms for exact computation on real numbers, using infinite streams of digits impleme…
Event Systems and Access Control
Dominique Méry, Stephan Merz
We consider the interpretations of notions of access control (permissions, interdictions, obligations, and user rights) as run-time properties of information systems specified as e…
CoInduction in Coq
Yves Bertot
We describe the basic notions of co-induction as they are available in the coq system. As an application, we describe arithmetic properties for simple representations of real numbe…
Coq in a Hurry
Yves Bertot
These notes provide a quick introduction to the Coq system and show how it can be used to define logical concepts and functions and reason about them. It is designed as a tutorial,…