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
15 papers · 2 filters
A TLA+ Proof System
Kaustuv C. Chaudhuri, Damien Doligez, Leslie Lamport +1
We describe an extension to the TLA+ specification language with constructs for writing proofs and a proof environment, called the Proof Manager (PM), to checks those proofs. The l…
Structural abstract interpretation, A formal study using Coq
Yves Bertot
interpreters are tools to compute approximations for behaviors of a program. These approximations can then be used for optimisation or for error detection. In this paper, we show h…
On characterising strong bisimilarity in a fragment of CCS with replication
Daniel Hirschkoff, Damien Pous
We provide a characterisation of strong bisimilarity in a fragment of CCS that contains only prefix, parallel composition, synchronisation and a limited form of replication. The ch…
On the strength of proof-irrelevant type theories
Benjamin Werner
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 underlyi…
Interaction Grammars
Bruno Guillaume, Guy Perrier
Interaction Grammar (IG) is a grammatical formalism based on the notion of polarity. Polarities express the resource sensitivity of natural languages by modelling the distinction b…
Bounded Underapproximations
Pierre Ganty, Rupak Majumdar, Benjamin Monmege
We show a new and constructive proof of the following language-theoretic result: for every context-free language L, there is a bounded context-free language L' included in L which…
Inductive and Coinductive Components of Corecursive Functions in Coq
Yves Bertot, Ekaterina Komendantskaya
In Constructive Type Theory, recursive and corecursive definitions are subject to syntactic restrictions which guarantee termination for recursive functions and productivity for co…
The computability path ordering: the end of a quest
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
In this paper, we first briefly survey automated termination proof methods for higher-order calculi. We then concentrate on the higher-order recursive path ordering, for which we p…
Separability in the Ambient Logic
Daniel Hirschkoff, Etienne Lozes, Davide Sangiorgi
The \it{Ambient Logic} (AL) has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semistruc…
From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures
Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub
We investigate here a new version of the Calculus of Inductive Constructions (CIC) on which the proof assistant Coq is based: the Calculus of Congruent Inductive Constructions, whi…
Wadge Degrees of Infinitary Rational Relations
Olivier Finkel
We show that, from the topological point of view, 2-tape Büchi automata have the same accepting power as Turing machines equipped with a Büchi acceptance condition. The Borel and t…
Experiments in Model-Checking Optimistic Replication Algorithms
Hanifa Boucheneb, Abdessamad Imine
This paper describes a series of model-checking experiments to verify optimistic replication algorithms based on Operational Transformation (OT) approach used for supporting collab…
On the Expressive Power of Multiple Heads in CHR
Cinzia Di Giusto, Maurizio Gabbrielli, Maria Chiara Meo
Constraint Handling Rules (CHR) is a committed-choice declarative language which has been originally designed for writing constraint solvers and which is nowadays a general purpose…
Visibly Tree Automata with Memory and Constraints
Hubert Comon-Lundh, Florent Jacquemard, Nicolas Perrin
Tree automata with one memory have been introduced in 2001. They generalize both pushdown (word) automata and the tree automata with constraints of equality between brothers of Bog…
Linear Logic by Levels and Bounded Time Complexity
Patrick Baillot, Damiano Mazza
We give a new characterization of elementary and deterministic polynomial time computation in linear logic through the proofs-as-programs correspondence. Girard's seminal results,…