Evelyne Contejean

37 papers A* 2A 7B 5C 1Journal 7Unranked 14

Year	Rank	Type	Title / Venue / Authors
2022	J	`jnl`	Translating Canonical SQL to Imperative Code in Coq. CoRR Véronique Benzaken, Evelyne Contejean, Mohammed Houssem Hachmaoui, Chantal Keller, Louis Mandel, Avraham Shinnar, Jérôme Siméon
2022	J	`jnl`	Translating canonical SQL to imperative code in Coq. Proc. ACM Program. Lang. Véronique Benzaken, Evelyne Contejean, Mohammed Houssem Hachmaoui, Chantal Keller, Louis Mandel, Avraham Shinnar, Jérôme Siméon
2021	B	`conf`	A Coq formalization of data provenance. CPP Véronique Benzaken, Sarah Cohen-Boulakia, Evelyne Contejean, Chantal Keller, Rébecca Zucchini
2019	B	`conf`	A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra. CPP Véronique Benzaken, Evelyne Contejean
2018	B	`conf`	A Coq Formalisation of SQL's Execution Engines. ITP Véronique Benzaken, Evelyne Contejean, Chantal Keller, Eunice Martins
2017	B	`conf`	Certifying Standard and Stratified Datalog Inference Engines in SSReflect. ITP Véronique Benzaken, Evelyne Contejean, Stefania Dumbrava
2014	A	`conf`	A Coq Formalization of the Relational Data Model. ESOP Véronique Benzaken, Evelyne Contejean, Stefania Dumbrava
2014	—	`book`	Facettes de la preuve : Jeux de reflets entre démonstration automatique et preuve assistée. Evelyne Contejean
2012	A	`conf`	A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic. IJCAR François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, Guillaume Melquiond
2012	J	`jnl`	Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation Log. Methods Comput. Sci. Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala
2011	—	`conf`	Automated Certified Proofs with CiME3. RTA Evelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, Xavier Urbain
2011	A	`conf`	Canonized Rewriting and Ground AC Completion Modulo Shostak Theories. TACAS Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala
2010	C	`conf`	A3PAT, an approach for certified automated termination proofs. PEPM Evelyne Contejean, Andrey Paskevich, Xavier Urbain, Pierre Courtieu, Olivier Pons, Julien Forest
2010	—	`conf`	Ground Associative and Commutative Completion Modulo Shostak Theories. LPAR short papers(Yogyakarta) Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala
2007	—	`conf`	CC(X): Semantic Combination of Congruence Closure with Solvable Theories. SMT@CAV Sylvain Conchon, Evelyne Contejean, Johannes Kanig, Stéphane Lescuyer
2007	—	`conf`	Certification of Automated Termination Proofs. FroCoS Evelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, Xavier Urbain
2007	—	`conf`	Modeling Permutations in Coqfor Coccinelle. Rewriting, Computation and Proof Evelyne Contejean
2005	J	`jnl`	Mechanically Proving Termination Using Polynomial Interpretations. J. Autom. Reason. Evelyne Contejean, Claude Marché, Ana Paula Tomás, Xavier Urbain
2005	A	`conf`	Reflecting Proofs in First-Order Logic with Equality. CADE Evelyne Contejean, Pierre Corbineau
2004	—	`conf`	A Certified AC Matching Algorithm. RTA Evelyne Contejean
2001	—	`conf`	Combining Pattern E-Unification Algorithms. RTA Alexandre Boudet, Evelyne Contejean
2000	—	`conf`	Rewriting Techniques in Theoretical Physics. RTA Evelyne Contejean, Antoine Coste, Benjamin Monate
1998	A	`conf`	About the Confluence of Equational Pattern Rewrite Systems. CADE Alexandre Boudet, Evelyne Contejean
1997	A	`conf`	AC-Unification of Higher-Order Patterns. CP Alexandre Boudet, Evelyne Contejean
1997	J	`jnl`	Avoiding Slack Variables in the Solving of Linear Diophantine Equations and Inequations. Theor. Comput. Sci. Farid Ajili, Evelyne Contejean
1997	—	`conf`	Rewrite Systems for Natural, Integral, and Rational Arithmetic. RTA Evelyne Contejean, Claude Marché, Landy Rabehasaina
1996	—	`conf`	AC-Complete Unification and its Application to Theorem Proving. RTA Alexandre Boudet, Evelyne Contejean, Claude Marché
1996	—	`conf`	C RTA Evelyne Contejean, Claude Marché
1995	—	`conf`	Complete Solving of Linear Diophantine Equations and Inequations without Adding Slack Variables. UNIF Farid Ajili, Evelyne Contejean
1995	A	`conf`	Complete Solving of Linear Diophantine Equations and Inequations without Adding Variables. CP Farid Ajili, Evelyne Contejean
1994	—	`conf`	"Syntactic" AC-Unification. CCL Alexandre Boudet, Evelyne Contejean
1994	J	`jnl`	An Efficient Incremental Algorithm for Solving Systems of Linear Diophantine Equations Inf. Comput. Evelyne Contejean, Hervé Devie
1993	A*	`conf`	A Partial Solution for D-Unification Based on a Reduction to AC1-Unification. ICALP Evelyne Contejean
1993	J	`jnl`	Solving *-Problems Modulo Distributivity by a Reduction to AC1-Unification. J. Symb. Comput. Evelyne Contejean
1993	B	`conf`	Solving Linear Diophantine Constraints Incrementally. ICLP Evelyne Contejean
1992	—	`conf`	On ALP Alexandre Boudet, Evelyne Contejean
1990	A*	`conf`	A New AC Unification Algorithm with an Algorithm for Solving Systems of Diophantine Equations LICS Alexandre Boudet, Evelyne Contejean, Hervé Devie