Catherine Dubois

Available identifiers

zbMath Open dubois.catherineMaRDI QIDQ1624591

List of research outcomes

Publication	Date of Publication	Type
Pragmatic isomorphism proofs between Coq representations: application to lambda-term families	2024-11-26	Paper
A semantics of \(\mathbb{K}\) into Dedukti	2024-11-26	Paper
https://portal.mardi4nfdi.de/entity/Q6068929	2023-12-15	Paper
Tests and proofs for custom data generators	2018-11-16	Paper
FoCaLiZe and Dedukti to the rescue for proof interoperability	2018-01-04	Paper
Objects and subtyping in the \(\lambda\)-\(\Pi\)-calculus modulo	2017-07-12	Paper
ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti	2016-12-21	Paper
Tests and Proofs for Enumerative Combinatorics	2016-10-19	Paper
Termination Proofs for Recursive Functions in FoCaLiZe	2016-06-21	Paper
Producing certified functional code from inductive specifications	2013-04-19	Paper
A certified constraint solver over finite domains	2012-11-08	Paper
Tableaux modulo theories using superdeduction. An application to the verification of B proof rules with the Zenon automated theorem prover	2012-09-05	Paper
A first step in the design of a formally verified constraint-based testing tool: FocalTest	2012-07-20	Paper
Verifying B proof rules using deep embedding and automated theorem proving	2011-10-28	Paper
Extracting Purely Functional Contents from Logical Inductive Types	2008-09-02	Paper
Why Would You Trust B?	2008-05-15	Paper
Functional Testing in the Focal Environment	2008-04-24	Paper
https://portal.mardi4nfdi.de/entity/Q4808705	2004-08-12	Paper
https://portal.mardi4nfdi.de/entity/Q2754040	2001-11-11	Paper
Certification of a type inference tool for ML: Damas-Milner within Coq	2000-01-30	Paper

Research outcomes over time

This page was built for person: Catherine Dubois