Conference Programme

Wednesday, 30 July 2008

Session 1: Invited Talk

14:00-15:00: Thierry Coquand:
Type Theory and Linear Algebra

15:00-15:30: Coffee Break

Session 2:

15:30-16:00: César Domínguez:
Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems

16:00-16:30: Santiago Jorge, Victor M. Gulias, Laura M. Castro:
Using Coq to Prove Properties of the Cache Level of a Functional Video-on-Demand Server

16:30-17:00: James Davenport:
Effective Set Membership in Computer Algebra and Beyond

17:30-18:00: Alan P. Sexton, Volker Sorge, Stephen M. Watt:
Towards Abstract Matrix Arithmetic

Thursday, 31 July 2008

Session 3:

11:00-11:30: Sebastian Freundt, Peter Horn, Alexander Konovalov, Steve Linton, Dan Roozemond:
Symbolic Computation Software Composability

11:30-12:00: Fadoua Ghourabi, Tetsuo Ida, Asem Kasem, Hidekazu Takahashi:
Progress Report of Eos Project

12:00-12:30: Salvador Lucas, Raquel Montagut, Rafael Navarro, Miguel A. Salido:
Exploiting linear and geometric programming techniques in termination tools

12:30-14:00: Lunch

Session 4:

14:00-14:30: Behzad Akbarpour, Lawrence Paulson:
MetiTarski: An Automatic Prover for the Elementary Functions

14:30-15:00: Laura Meikle, Jacques Fleuriot:
Combining Isabelle and QEPCAD-B in the Prover's Palette

15:00-15:30: Amine Chaieb:
Parametric linear arithmetic over ordered fields in Isabelle/HOL

15:30-16:00: Coffee Break

Session 5:

16:00-16:30: John Charnley, Simon Colton:
A Global Workspace Framework for Combining Reasoning Systems

16:30-17:00: Alan P.Sexton and Volker Sorge:
Community Maintenance of OpenMath Content Dictionaries

17:00-18:00: Business Meeting

19:00-21:00: AISC/Calculemus Banquet

Friday, 1 August 2008

Session 6: Invited Talk

9:30-10:30: Annie Cuyt:
Validated Evaluation of Special Mathematical Functions

10:30-11:00: Coffee Break

Session 7:

11:00-11:30: Cezary Kaliszyk:
Automating side conditions in formalized partial functions

11:30-12:00: Jacques Carette, William Farmer:
High-Level Theories