Vincent Siles

Most-cited papers

A Refinement-Based Approach to Computational Algebra in Coq
Maxime Dénès, Anders Mörtberg, Vincent Siles
2012International Conference on Interactive Theorem Proving74 citations Open access
Semantic Scholar
A Decision Procedure for Regular Expression Equivalence in Type Theory
T. Coquand, Vincent Siles
2011Certified Programs and Proofs46 citations
Semantic Scholar
Pure Type System conversion is always typable
Vincent Siles, Hugo Herbelin
2012Journal of functional programming36 citations Open access
Semantic Scholar
Formalized linear algebra over Elementary Divisor Rings in Coq
Guillaume Cano, C. Cohen, Maxime Dénès, Anders Mörtberg +1 more
2016Log. Methods Comput. Sci.22 citations Open access
Semantic Scholar
Towards a Certified Computation of Homology Groups for Digital Images
Jónathan Heras, Maxime Dénès, Gadea Mata, Anders Mörtberg +2 more
2012International Workshop on Computational Topology in Image Context22 citations Open access
Semantic Scholar
Computing persistent homology within Coq/SSReflect
Jónathan Heras, T. Coquand, Anders Mörtberg, Vincent Siles
2012TOCL21 citations Open access
Semantic Scholar
Equality Is Typable in Semi-full Pure Type Systems
Vincent Siles, Hugo Herbelin
20102010 25th Annual IEEE Symposium on Logic in Computer Science16 citations Open access
Semantic Scholar
Modeling and Abstraction of Memory Management in a Hypervisor
Pauline Bolignano, Thomas P. Jensen, Vincent Siles
2016Fundamental Approaches to Software Engineering10 citations Open access
Semantic Scholar
Coherent and Strongly Discrete Rings in Type Theory
T. Coquand, Anders Mörtberg, Vincent Siles
2012Certified Programs and Proofs8 citations
Semantic Scholar
A formal proof of Sasaki-Murao algorithm
T. Coquand, Anders Mörtberg, Vincent Siles
2012Journal of Formalized Reasoning8 citations
Semantic Scholar
Ideas over terms generalization in Coq
Vincent Siles
20080 citations
Semantic Scholar