Invited talk: Computational Logic and Continuous Mathematics, Pure and Applied
Rob Arthan (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.

break

Exploring a Quantum Theory with Graph Rewriting and Computer Algebra
Aleks Kissinger.

A Comparison of Equality in Computer Algebra and Correctness in Mathematical Pedagogy
Russell Bradford, James Davenport and Christopher Sangwin.

Lunch

Invited talk:Math Handwriting Recognition in Windows 7 and Its Benefits
Marko Panic

break

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
Ekaterina Shemyakova.

A Groupoid of Data Transformations
Paul Tarau.

break

Algorithms for the Functional Decomposition of Laurent Polynomials
Stephen Watt.

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.

Lunch

Invited Talk:Abstraction-Based Information Technology: A Framework for Open Mechanized Reasoning
Prof. Jacques Calmet (Universität Karlsruhe)

break

Reusing Proofs in a Mathematical Library
Ivan Noyer and Renaud Rioboo.

Reflecting Data: Formally Correct Results for Efficient (and Dirty) Algorithms
Lucas Dixon.