Calculemus.netMeetingsOntario 2009 → Programme

Calculemus 2009: Schedule

16th Symposium on the Integration of
Symbolic Computation and Mechanised Reasoning
6-7 July 2009, Joint with CICM'09, Ontario, Canada.

Monday July 6th:

8:30-9:30
Invited talk: Computational Logic and Continuous Mathematics, Pure and Applied
Rob Arthan (Director of Lemma 1, developer of ProofPower)
9:30-10:00
Combining Coq and Gappa for Certifying Floating-Point Programs
Sylvie Boldo, Jean-Christophe Filliâtre and Guillaume Melquiond.
10:00-10:30
ACL2 verification of simplicial degeneracy programs in the Kenzo system
Francisco-Jesus Martin-Mateos, Julio Rubio and Jose-Luis Ruiz-Reina.
10:30-11:00
break
11:00-11:30
Exploring a Quantum Theory with Graph Rewriting and Computer Algebra
Aleks Kissinger.
11:30-12:00
A Comparison of Equality in Computer Algebra and Correctness in Mathematical Pedagogy
Russell Bradford, James Davenport and Christopher Sangwin.
12:00-3:00
Lunch
3:00-4:00
Invited talk:Math Handwriting Recognition in Windows 7 and Its Benefits
Marko Panic
4:00-4:30
break
4:30-4:45
Computing Ranking and Unranking Functions for BDDs
Paul Tarau and Brenda Luderman.
4:45-5:00
The Naproche System
Daniel Kuehlwein, Marcos Cramer, Peter Koepke and Bernhard Schröder.
5:00-5:30
Reasoning with Generic Cases in the Arithmetic of Abstract Matrices
Alan Sexton, Volker Sorge and Stephen Watt.

Tuesday July 7th:

9:00-9:30
Combined Decision Techniques for the Existential Theory of the Reals
Grant Olney Passmore and Paul Jackson.
9:30-10:00
Invariant Properties of Third-Order Non-Hyperbolic Linear Partial Differential Operators
Ekaterina Shemyakova.
10:00-10:30
A Groupoid of Data Transformations
Paul Tarau.
10:30-11:00
break
11:00-11:30
Algorithms for the Functional Decomposition of Laurent Polynomials
Stephen Watt.
11:30-12:00
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.
12:00-3:00
Lunch
3:00-4:00
Invited Talk:Abstraction-Based Information Technology: A Framework for Open Mechanized Reasoning
Prof. Jacques Calmet (Universität Karlsruhe)
4:00-4:30
break
4:30-4:45
Reusing Proofs in a Mathematical Library
Ivan Noyer and Renaud Rioboo.
4:45-5:00
Reflecting Data: Formally Correct Results for Efficient (and Dirty) Algorithms
Lucas Dixon.
5:00-6:00
Calculemus Business Meeting