default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID8th MKM / 16th Calculemus 2009: Grand Bend, Canada
- Jacques Carette
, Lucas Dixon, Claudio Sacerdoti Coen, Stephen M. Watt:
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. Lecture Notes in Computer Science 5625, Springer 2009, 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 P. Fitch:
CAMAL 40 Years on - Is Small Still Beautiful?. 32-44 - Gonzalo A. Aranda-Corral, Joaquín Borrego-Díaz, María 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 G. 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 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 - Peter Horn, Dan Roozemond:
OpenMath in SCIEnce: SCSCP and POPCORN. 474-479 - Albert 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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-12-05 22:22 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
