10 citations · 18 across the 10 of their papers we have counts for
11 papers
Comparing EventB, and Why3 Models of Sparse Sets
Maximiliano Cristiá, Catherine Dubois
Many representations for sets are available in programming languages libraries. The paper focuses on sparse sets used, e.g., in some constraint solvers for representing integer var…
Pragmatic isomorphism proofs between Coq representations: application to lambda-term families
Catherine Dubois, Nicolas Magaud, Alain Giorgetti
There are several ways to formally represent families of data, such as lambda terms, in a type theory such as the dependent type theory of Coq. Mathematical representations are ver…
Automatic Synthesis of Random Generators for Numerically Constrained Algebraic Recursive Types
Ghiles Ziat, Vincent Botbol, Matthieu Dien +3
In program verification, constraint-based random testing is a powerful technique which aims at generating random test cases that satisfy functional properties of a program. However…
LibNDT: Towards a Formal Library on Spreadable Properties over Linked Nested Datatypes
Mathieu Montin, Amélie Ledein, Catherine Dubois
Nested datatypes have been widely studied in the past 25 years, both theoretically using category theory, and practically in programming languages such as Haskell. They consist in…
Formally Verified Transformation of Non-binary Constraints into Binary Constraints
Catherine Dubois
It is well known in the Constraint Programming community that any non-binary constraint satisfaction problem (with finite domains) can be transformed into an equivalent binary one.…
Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving
Catherine Dubois, Bruno Woltzenlogel Paleo
This volume of EPTCS contains the proceedings of the Fifth Workshop on Proof Exchange for Theorem Proving (PxTP 2017), held on September 23-24, 2017 as part of the Tableaux, FroCoS…