636 citations · 3.7k across the 99 of their papers we have counts for
6 papers · 1 filter
Reliably Reproducing Machine-Checked Proofs with the Coq Platform
Karl Palmskog, Enrico Tassi, Théo Zimmermann
The Coq Platform is a continuously developed distribution of the Coq proof assistant together with commonly used libraries, plugins, and external tools useful in Coq-based formal v…
Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
Elaine Pimentel, Enrico Tassi
Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and comput…
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…
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 Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen +1
The paper describes the refinement algorithm for the Calculus of (Co)Inductive Constructions (CIC) implemented in the interactive theorem prover Matita. The refinement algorithm is…
Smart matching
Andrea Asperti, Enrico Tassi
One of the most annoying aspects in the formalization of mathematics is the need of transforming notions to match a given, existing result. This kind of transformations, often base…