1.4k citations
- Université Paris-SudFR237 papers
- Centre National de la Recherche ScientifiqueFR177 papers
- Institut national de recherche en sciences et technologies du numériqueFR105 papers
- Université Paris-SaclayFR70 papers
- Centre Inria de SaclayFR53 papers
- University of California, BerkeleyUS34 papers
- Institut d'Astrophysique SpatialeFR30 papers
- Université Paris DiderotFR30 papers
- Sapienza University of RomeIT27 papers
- Université Toulouse III - Paul SabatierFR27 papers
- University of California, DavisUS27 papers
- California Institute of TechnologyUS26 papers
5 papers · 2 filters
The Vectorial -Calculus
Pablo Arrighi, Alejandro Díaz-Caro, Benoît Valiron
We describe a type system for the linear-algebraic -calculus. The type system accounts for the linear-algebraic aspects of this extension of -calculus: it is able to statical…
READ-EVAL-PRINT in Parallel and Asynchronous Proof-checking
Makarius Wenzel
The LCF tradition of interactive theorem proving, which was started by Milner in the 1970-ies, appears to be tied to the classic READ-EVAL-PRINT-LOOP of sequential and synchronous…
Certified Impossibility Results for Byzantine-Tolerant Mobile Robots
Cédric Auger, Zohir Bouzid, Pierre Courtieu +2
We propose a framework to build formal developments for robot networks using the COQ proof assistant, to state and to prove formally various properties. We focus in this paper on i…
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems
Bruno Barras, Lourdes del Carmen González Huesca, Hugo Herbelin +4
This is an overview of the Paral-ITP project, which intents to make the proof assistants Isabelle and Coq fit for the multicore era.
A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
Christoph Lange, Marco B. Caminati, Manfred Kerber +4
Novel auction schemes are constantly being designed. Their design has significant consequences for the allocation of goods and the revenues generated. But how to tell whether a new…