8. MKM / 16. Calculemus 2009: Grand Bend, Canada
Jacques Carette, Lucas Dixon, Claudio Sacerdoti Coen, Stephen M. Watt (Eds.): Intelligent Computer Mathematics, 16th Symposium, Calculemus 2009, 8th International Conference, MKM 2009, Held as Part of CICM 2009, Grand Bend, Canada, July 6-12, 2009. Proceedings. Springer 2009 Lecture Notes in Computer Science ISBN 978-3-642-02613-3
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
- Joseph B. Collins: OpenMath Content Dictionaries for SI Quantities and Units. 247-262
- 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
- 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
- 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 lambdaµµ. 405-421
- Ramana Chakradhar 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
- Albert D. Rich, David J. Jeffrey: A Knowledge Repository for Indefinite Integration Based on Transformation Rules. 480-485
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-06-19T203413 by the dblp team