From the 1 of 2.5k papers with an AI index.
29.3k citations
- Centre National de la Recherche ScientifiqueFR568 papers
- Laboratoire Lorrain de Recherche en Informatique et ses ApplicationsFR170 papers
- Centre Inria de SaclayFR169 papers
- Sorbonne UniversitéFR157 papers
- Université Grenoble AlpesFR110 papers
- École Normale Supérieure - PSLFR108 papers
- Université Paris CitéFR107 papers
- Centre Inria de l'Université de LilleFR90 papers
- Centre Inria de l'Université Grenoble AlpesFR87 papers
- Institut de Recherche en Informatique et Systèmes AléatoiresFR86 papers
- École Normale Supérieure de LyonFR84 papers
- École PolytechniqueFR83 papers
6 papers · 2 filters
Asynchronous processing of Coq documents: from the kernel up to the user interface
Bruno Barras, Carst Tankink, Enrico Tassi
The work described in this paper improves the reactivity of the Coq system by completely redesigning the way it processes a formal document. By subdividing such work into independe…
On the Relative Usefulness of Fireballs
Beniamino Accattoli, Claudio Sacerdoti Coen
In CSL-LICS 2014, Accattoli and Dal Lago showed that there is an implementation of the ordinary (i.e. strong, pure, call-by-name) -calculus into models like RAM machines which i…
Wave-Style Token Machines and Quantum Lambda Calculi
Ugo Dal Lago, Margherita Zorzi
Particle-style token machines are a way to interpret proofs and programs, when the latter are written following the principles of linear logic. In this paper, we show that token ma…
Cut Elimination in Multifocused Linear Logic
Taus Brock-Nannestad, Nicolas Guenot
We study cut elimination for a multifocused variant of full linear logic in the sequent calculus. The multifocused normal form of proofs yields problems that do not appear in a sta…
Deduction modulo theory
Gilles Dowek
This paper is a survey on Deduction modulo theory
Tableaux Modulo Theories Using Superdeduction
Mélanie Jacquel, Karim Berkani, David Delahaye +1
We propose a method that allows us to develop tableaux modulo theories using the principles of superdeduction, among which the theory is used to enrich the deduction system with ne…