Computational Logic and Continuous Mathematics, Pure and Applied
(Director of Lemma 1, developer of ProofPower)
Combining Coq and Gappa for Certifying Floating-Point Programs
Sylvie Boldo, Jean-Christophe Filliâtre and Guillaume Melquiond.
ACL2 verification of simplicial degeneracy programs in the Kenzo system
Francisco-Jesus Martin-Mateos, Julio Rubio and Jose-Luis Ruiz-Reina.
Exploring a Quantum Theory with Graph Rewriting and Computer Algebra
A Comparison of Equality in Computer Algebra and Correctness in Mathematical Pedagogy
Russell Bradford, James Davenport and Christopher Sangwin.
Invited talk:Math Handwriting Recognition in Windows 7 and Its Benefits
Computing Ranking and Unranking Functions for BDDs
Paul Tarau and Brenda Luderman.
The Naproche System
Daniel Kuehlwein, Marcos Cramer, Peter Koepke and Bernhard Schröder.
Reasoning with Generic Cases in the Arithmetic of Abstract Matrices
Alan Sexton, Volker Sorge and Stephen Watt.
Combined Decision Techniques for the Existential Theory of the Reals
Grant Olney Passmore and Paul Jackson.
Invariant Properties of Third-Order Non-Hyperbolic Linear Partial Differential Operators
A Groupoid of Data Transformations
Algorithms for the Functional Decomposition of Laurent Polynomials
Conservative retractions of propositional logic theories by means of boolean derivatives. Theoretical foundations
Gonzalo A. Aranda-Corral, Joaquín Borrego-Díaz and M. Magdalena Fernández-Lebrón.
Invited Talk:Abstraction-Based Information Technology: A Framework for Open Mechanized Reasoning
Prof. Jacques Calmet
Reusing Proofs in a Mathematical Library
Ivan Noyer and Renaud Rioboo.
Reflecting Data: Formally Correct Results for Efficient (and Dirty) Algorithms
Calculemus Business Meeting