| Joint Invited Talks / 1： |
| Computational Logic and Continuous Mathematics, Pure and Applied / Rob Arthan |
| Math-Literate Computers / Dorothea Blostein |
| Abstraction-Based Information Technology: A Framework for Open Mechanized Reasoning / Jacques Calmet |
| Software Engineering for Mathematics / Georges Gonthier |
| Calculemus Talks / 2： |
| Some Traditional Mathematical Knowledge Management / Patrick D.F. Ion |
| Math Handwriting Recognition in Windows 7 and Its Benefits / Marko Panic |
| Assembling the Digital Mathematics Library / David Ruddy |
| CAMAL 40 Years on - Is Small Still Beautiful? / John Fitch |
| Conservative Retractions of Propositional Logic Theories by Means of Boolean Derivatives: Theoretical Foundations / Gonzalo A. Aranda-Corral ; Joaquín Borrego-Díaz ; M. Magdalena Fernández-Lebrón |
| Combining Coq and Gappa for Certifying Floating-Point Programs / Sylvie Boldo ; Jean-Christophe Filliâtre ; Guillaume Melquiond |
| A Comparison of Equality in Computer Algebra and Correctness in Mathematical Pedagogy / Russell Bradford ; James H. Davenport ; Christopher J. Sangwin |
| Exploring a Quantum Theory with Graph Rewriting and Computer Algebra / Aleks Kissinger |
| ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System / Francisco-Jesus ; Martín-Mateos ; Julio Rubio ; Jose-Luis Ruiz-Reina |
| Combined Decision Techniques for the Existential Theory of the Reals / Grant Olney Passmore ; Paul B. Jackson |
| Reasoning with Generic Cases in the Arithmetic of Abstract Matrices / Alan P. Sexton ; Volker Sorge ; Stephen M. Watt |
| Invariant Properties of Third-Order Non-hyperbolic Linear Partial Differential Operators / Ekaterina Shemyakova |
| A Groupoid of Isomorphic Data Transformations / Paul Tarau |
| Algorithms for the Functional Decomposition of Laurent Polynomials |
| MKM Talks / 3： |
| A Linear Grammar Approach to Mathematical Formula Recognition from PDF / Josef B. Baker |
| Formal Proof: Reconciling Correctness and Understanding / Cristian S. Calude ; Christine Müller |
| A Review of Mathematical Knowledge Management / Jacques Carette ; William M. Farmer |
| OpenMath Content Dictionaries for SI Quantities and Units / Joseph B. Collins |
| Unifying Math Ontologies: A Tale of Two Standards / Michael Kohlhase |
| Integrating Web Services into Active Mathematical Documents / Jana Giceva ; Christoph Lange ; Florian Rabe |
| Representation for Interactive Exercises / George Goguadze |
| The Characteristics of Writing Environments for Mathematics: Behavioral Consequences and Implications for Software Design and Usability / Davood G. Gozli ; Marco Pollanen ; Michael Reynolds |
| Canonical Forms in Interactive Exercise Assistants / Bastiaan Heeren ; Johan Jeuring |
| Spreadsheet Interaction with Frames: Exploring a Mathematical Practice / Andrea Kohlhase |
| Compensating the Computational Bias of Spreadsheets with MKM Techniques |
| MathLang Translation to Isabelle Syntax / Robert Lamar ; Fairouz Kamareddine ; J.B. Wells |
| A Mathematical Approach to Ontology Authoring and Documentation |
| A Logically Saturated Extension of λ&bar;μμ&bar; / Lionel Elie Mamane ; Herman Geuvers ; James McKinna |
| From Tessellations to Table Interpretation / Ramana C. Jandhyala ; Mukkai Krishnamoorthy ; George Nagy ; Raghav Padmanabhan ; Sharad Seth ; William Silversmith |
| Finite Groups Representation Theory with CoQ / Sidi Ould Biha |
| Collaborative Assistant to Handle MathML Expressions / Aslam Muhammad ; Ana Maria Martinez Enriquez ; Gonzalo Escalada-Imaz |
| Confidence Measures in Recognizing Handwritten Mathematical Symbols / Oleg Golubitsky |
| Using Open Mathematical Documents to Interface Computer Algebra and Proof Assistant Systems / Jónathan Heras ; Vico Pascual |
| OpenMath in SCIEnce: SCSCP and POPCORN / Peter Horn ; Dan Roozemond |
| A Knowledge Repository for Indefinite Integration Based on Transformation Rules / A.D. Rich ; D.J. Jeffrey |
| Natural Deduction Environment for Matita / Claudio Sacerdoti Coen ; Enrico Tassi |
| Author Index |
| Joint Invited Talks / 1： |
| Computational Logic and Continuous Mathematics, Pure and Applied / Rob Arthan |
| Math-Literate Computers / Dorothea Blostein |
ＥＢ
