205 citations · 525 across the 28 of their papers we have counts for
3 papers · 1 filter
Recycling Proof Patterns in Coq: Case Studies
Jónathan Heras, Ekaterina Komendantskaya
Development of Interactive Theorem Provers has led to the creation of big libraries and varied infrastructures for formal proofs. However, despite (or perhaps due to) their sophist…
Machine Learning in Proof General: Interfacing Interfaces
Ekaterina Komendantskaya, Jónathan Heras, Gudmund Grov
We present ML4PG - a machine learning extension for Proof General. It allows users to gather proof statistics related to shapes of goals, sequences of applied tactics, and proof tr…
Verifying an algorithm computing Discrete Vector Fields for digital imaging
Jónathan Heras, María Poza, Julio Rubio
In this paper, we present a formalization of an algorithm to construct admissible discrete vector fields in the Coq theorem prover taking advantage of the SSReflect library. Discre…