8. MKM / 16. Calculemus 2009: Grand Bend, Canada

Joint Invited Talks

• Rob Arthan:
  Computational Logic and Continuous Mathematics, Pure and Applied. 1
  
• Dorothea Blostein:
  Math-Literate Computers. 2-13
  
• Jacques Calmet:
  Abstraction-Based Information Technology: A Framework for Open Mechanized Reasoning. 14-26
  
• Georges Gonthier:
  Software Engineering for Mathematics. 27
  

Calculemus Talks

• Patrick D. F. Ion:
  Some Traditional Mathematical Knowledge Management. 28
  
• Marko Panic:
  Math Handwriting Recognition in Windows 7 and Its Benefits. 29-30
  
• David Ruddy:
  Assembling the Digital Mathematics Library. 31
  
• John Fitch:
  CAMAL 40 Years on - Is Small Still Beautiful?. 32-44
  
• Gonzalo A. Aranda-Corral, Joaquín Borrego-Díaz, M. Magdalena Fernández-Lebrón:
  Conservative Retractions of Propositional Logic Theories by Means of Boolean Derivatives: Theoretical Foundations. 45-58
  
• Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond:
  Combining Coq and Gappa for Certifying Floating-Point Programs. 59-74
  
• Russell J. Bradford, James H. Davenport, Christopher J. Sangwin:
  A Comparison of Equality in Computer Algebra and Correctness in Mathematical Pedagogy. 75-89
  
• Aleks Kissinger:
  Exploring a Quantum Theory with Graph Rewriting and Computer Algebra. 90-105
  
• Francisco-Jesús Martín-Mateos, Julio Rubio, José-Luis Ruiz-Reina:
  ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System. 106-121
  
• Grant Olney Passmore, Paul B. Jackson:
  Combined Decision Techniques for the Existential Theory of the Reals. 122-137
  
• Alan P. Sexton, Volker Sorge, Stephen M. Watt:
  Reasoning with Generic Cases in the Arithmetic of Abstract Matrices. 138-153
  
• Ekaterina Shemyakova:
  Invariant Properties of Third-Order Non-hyperbolic Linear Partial Differential Operators. 154-169
  
• Paul Tarau:
  A Groupoid of Isomorphic Data Transformations. 170-185
  
• Stephen M. Watt:
  Algorithms for the Functional Decomposition of Laurent Polynomials. 186-200
  

MKM Talks

• Josef B. Baker, Alan P. Sexton, Volker Sorge:
  A Linear Grammar Approach to Mathematical Formula Recognition from PDF. 201-216
  
• Cristian S. Calude, Christine Müller:
  Formal Proof: Reconciling Correctness and Understanding. 217-232
  
• Jacques Carette, William M. Farmer:
  A Review of Mathematical Knowledge Management. 233-246
  
• Joseph B. Collins:
  OpenMath Content Dictionaries for SI Quantities and Units. 247-262
  
• James H. Davenport, Michael Kohlhase:
  Unifying Math Ontologies: A Tale of Two Standards. 263-278
  
• Jana Giceva, Christoph Lange, Florian Rabe:
  Integrating Web Services into Active Mathematical Documents. 279-293
  
• George Goguadze:
  Representation for Interactive Exercises. 294-309
  
• Davood G. Gozli, Marco Pollanen, Michael Reynolds:
  The Characteristics of Writing Environments for Mathematics: Behavioral Consequences and Implications for Software Design and Usability. 310-324
  
• Bastiaan Heeren, Johan Jeuring:
  Canonical Forms in Interactive Exercise Assistants. 325-340
  
• Andrea Kohlhase, Michael Kohlhase:
  Spreadsheet Interaction with Frames: Exploring a Mathematical Practice. 341-356
  
• Andrea Kohlhase, Michael Kohlhase:
  Compensating the Computational Bias of Spreadsheets with MKM Techniques. 357-372
  
• Robert Lamar, Fairouz Kamareddine, J. B. Wells:
  MathLang Translation to Isabelle Syntax. 373-388
  
• Christoph Lange, Michael Kohlhase:
  A Mathematical Approach to Ontology Authoring and Documentation. 389-404
  
• Lionel Elie Mamane, Herman Geuvers, James McKinna:
  A Logically Saturated Extension of . 405-421
  
• Ramana C. Jandhyala, Mukkai S. Krishnamoorthy, George Nagy, Raghav K. Padmanabhan, Sharad C. Seth, William Silversmith:
  From Tessellations to Table Interpretation. 422-437
  
• Sidi Ould Biha:
  Finite Groups Representation Theory with Coq. 438-452
  
• Aslam Muhammad, Ana María Martínez Enríquez, Gonzalo Escalada-Imaz:
  Collaborative Assistant to Handle MathML Expressions. 453-459
  
• Oleg Golubitsky, Stephen M. Watt:
  Confidence Measures in Recognizing Handwritten Mathematical Symbols. 460-466
  
• Jónathan Heras, Vico Pascual, Julio Rubio:
  Using Open Mathematical Documents to Interface Computer Algebra and Proof Assistant Systems. 467-473
  
• Peter Horn, Dan Roozemond:
  OpenMath in SCIEnce: SCSCP and POPCORN. 474-479
  
• A. D. Rich, David J. Jeffrey:
  A Knowledge Repository for Indefinite Integration Based on Transformation Rules. 480-485
  
• Claudio Sacerdoti Coen, Enrico Tassi:
  Natural Deduction Environment for Matita. 486-491