From the 1 of 2.5k papers with an AI index.
29.3k citations
- Centre National de la Recherche ScientifiqueFR646 papers
- Laboratoire Lorrain de Recherche en Informatique et ses ApplicationsFR180 papers
- Centre Inria de SaclayFR175 papers
- Sorbonne UniversitéFR174 papers
- Université Grenoble AlpesFR119 papers
- Université Paris CitéFR114 papers
- École Normale Supérieure - PSLFR113 papers
- Université Paris-SaclayFR96 papers
- Centre Inria de l'Université Grenoble AlpesFR94 papers
- Institut de Recherche en Informatique et Systèmes AléatoiresFR94 papers
- Centre Inria de l'Université de LilleFR90 papers
- École Normale Supérieure de LyonFR88 papers
11 papers · 2 filters
Proceedings International Workshop on Strategies in Rewriting, Proving, and Programming
Hélène Kirchner, César Muñoz
This volume contains selected papers from the proceedings of the First International Workshop on Strategies in Rewriting, Proving, and Programming (IWS 2010), which was held on Jul…
Verifying Safety Properties With the TLA+ Proof System
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport +1
TLAPS, the TLA+ proof system, is a platform for the development and mechanical verification of TLA+ proofs written in a declarative style requiring little background beyond element…
Formal study of plane Delaunay triangulation
Jean-François Dufourd, Yves Bertot
This article presents the formal proof of correctness for a plane Delaunay triangulation algorithm. It consists in repeating a sequence of edge flippings from an initial triangulat…
Ackermannian and Primitive-Recursive Bounds with Dickson's Lemma
Diego Figueira, Santiago Figueira, Sylvain Schmitz +1
Dickson's Lemma is a simple yet powerful tool widely used in termination proofs, especially when dealing with counters or related data structures. However, most computer scientists…
Classical and Intuitionistic Subexponential Logics are Equally Expressive
Kaustuv Chaudhuri
It is standard to regard the intuitionistic restriction of a classical logic as increasing the expressivity of the logic because the classical logic can be adequately represented i…
The duality of computation under focus
Pierre-Louis Curien, Guillaume Munch-Maccagnoni
We review the close relationship between abstract machines for (call-by-name or call-by-value) lambda-calculi (extended with Felleisen's C) and sequent calculus, reintroducing on t…