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
41 papers · 1 filter
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…
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…
Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant
Théo Zimmermann, Hugo Herbelin
In mathematics, it is common practice to have several constructions for the same objects. Mathematicians will identify them modulo isomorphism and will not worry later on which con…