133 citations
- Université Paris CitéFR26 papers
- Université Paris DiderotFR25 papers
- Centre National de la Recherche ScientifiqueFR19 papers
- Institut national de recherche en sciences et technologies du numériqueFR12 papers
- Sorbonne Paris CitéFR8 papers
- Délégation Paris 7FR4 papers
- École PolytechniqueFR4 papers
- Institut Camille JordanFR3 papers
- Laboratoire d'Informatique de l'École PolytechniqueFR3 papers
- Laboratoire d'Informatique de Paris-NordFR3 papers
- University of OxfordGB3 papers
- Ca' Foscari University of VeniceIT2 papers
97 papers
A Simple Proof That Super-Consistency Implies Cut Elimination
Gilles Dowek, Olivier Hermant
We give a simple and direct proof that super-consistency implies the cut elimination property in deduction modulo. This proof can be seen as a simplification of the proof that supe…
Uniform generation of infinite concurrent runs: the case of trace monoids
Samy Abbes, Vincent Jugé
We introduce an algorithm for the uniform generation of infinite runs in concurrent systems under a partial order probabilistic semantics. We work with trace monoids as concurrency…
On the characterization of models of H*: The semantical aspect
Flavien Breuvart
We give a characterization, with respect to a large class of models of untyped lambda-calculus, of those models that are fully abstract for head-normalization, i.e., whose equation…
A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine
Paul-André Melliès, Noam Zeilberger
Combining insights from the study of type refinement systems and of monoidal closed chiralities, we show how to reconstruct Lawvere's hyperdoctrine of presheaves using a full and f…
Hofstadter's problem for curious readers
Pierre Letouzey
This document summarizes the proofs made during a Coq development inSummer 2015. This development investigates the function G introducedby Hofstadter in his famous "G{ö}del, Escher…
Reversible Barbed Congruence on Configuration Structures
Clément Aubert, Ioana Cristescu
A standard contextual equivalence for process algebras is strong barbed congruence. Configuration structures are a denotational semantics for processes in which one can define equi…