Subject to change.
Monday, July 18th 2011
9:00 Welcome
9:30 Invited talk 1
Coffee Break (10:30 – 11:00)
Session 1 (MKM 1): 11:00 – 12:30
- 11:00 Workflows for the Management of Change in Science, Technologies, Engineering and Mathematics
Serge Autexier, Catalin David, Dominik Dietrich, Michael Kohlhase and Vyacheslav Zholudev
- 11:30 WiP: Versioned Links
Andrea Kohlhase and Michael Kohlhase
- 11:45 WiP: A Dynamic Generalized Parser for Common Mathematical Language
Parsing
Kevin Kofler and Arnold Neumaier
- 12:00 Large Formal Wikis: Issues and Solutions
Jesse Alama, Kasper Brink, Lionel Mamane and Josef Urban
Lunch (12:30 – 14:30)
Session 2 (MKM 2): 14:30 – 16:00
- 14:30 Isabelle as Document-oriented Proof Assistant
Makarius Wenzel
- 15:00 Towards Formal Proof Script Refactoring
Iain Whiteside, David Aspinall, Gudmund Grov and Lucas Dixon
- 15:30 WiP: Querying Proofs
David Aspinall, Ewen Denney and Christoph Lüth
- 15:45 WiP: planMP: Collecting Mathematical Practices for MKM
Andrea Kohlhase and Constantin Jucovschi
Tea Break (16:00 – 16:30)
Session 3 (MKM 3): 16:30 – 17:30
- 16:30 Interleaving Strategies
Bastiaan Heeren and Johan Jeuring
- 17:00 Disambiguation of Symbolic Mathematics in the Naproche System
Marcos Cramer, Peter Koepke and Bernhard Schröder
- 17:30 Short break
CICM business meeting (17:40 – 18:30)
Tuesday, July 19th 2011
Session 4a (Projects): 9:00 – 10:30
- 9:00 Formalization of Formal Topology by means of the interactive theorem prover Matita
Andrea Asperti, Maria Emilia Maietti, Claudio Sacerdoti Coen, Giovanni Sambin and Silvio Valentini
- 9:10 MathScheme: Project Description
Jacques Carette, William Farmer and Russell O'Connor
- 9:20 The LATIN Logic Atlas
Mihai Codescu, Fulya Horozal, Michael Kohlhase, Till Mossakowski and Florian Rabe
- 9:30 A Formalization of the C99 Standard in HOL, Isabelle and Coq
Robbert Krebbers and Freek Wiedijk
- 9:40 Mizar-items: Exploring fine-grained dependencies in the Mizar Mathematical Library
Jesse Alama
- 9:50 Learning2Reason
Daniel Kuehlwein, Josef Urban, Evgeni Tsivtsivadze, Tom Heskes and Herman Geuvers
- 10:00 Project EuDML – A First Year Demonstration
Jose Borbinha, Thierry Bouche, Aleksander Nowinski and Petr Sojka
- 10:10 A Symbolic Companion for Interactive Geometric Systems
Francisco Botana
- 10:20 A system for computing and reasoning in Algebraic Topology
Jónathan Heras, Vico Pascual and Julio Rubio
Coffee Break (10:30 – 11:00)
Session 4b (Systems): 11:00 – 12:30
- 11:00 System Description: EgoMath2 as a tool for mathematical searching on Wikipedia.org
Jozef Mišutka and Leo Galamboš
- 11:10 Krextor – An Extensible Framework for Contributing Content Math to the Web of Data
Christoph Lange
- 11:20 The LaTeXML Daemon: Editable Math on the Collaborative Web
Deyan Ginev, Heinrich Stamerjohanns, Bruce R. Miller and Michael Kohlhase
- 11:30 System demonstrations
Lunch (12:30 – 14:30)
Session 4c (Posters): 14:30 – 16:00
Tea Break (16:00 – 16:30)
Session 5 (Calculemus 1): 16:30 – 17:30
- 16:30 A Foundational View on Integration Problems
Michael Kohlhase, Florian Rabe and Claudio Sacerdoti Coen
- 17:00 Enumeration of AG-Groupoids
Andreas Distler, Muhammad Shah and Volker Sorge
- 17:30 Short break
MKM business meeting (17:40 – 18:30)
Wednesday, July 20th 2011
9:30 Invited talk 2
Coffee Break (10:30 – 11:00)
Session 6 (MKM 4): 11:00 – 12:30
- 11:00 Extending OpenMath with Sequences
Fulya Horozal, Michael Kohlhase and Florian Rabe
- 11:00 Combining Source, Content, Presentation, Narration, and Relational Representation
Fulya Horozal, Alin Iacob, Constantin Jucovschi, Florian Rabe and Michael Kohlhase
- 11:30 Licensing the Mizar Mathematical Library
Jesse Alama, Michael Kohlhase, Adam Naumowicz, Piotr Rudnicki, Josef Urban and Lionel Mamane
- 12:00 Indexing and Searching Mathematics in Digital Libraries (Architecture, Design and Scalability Issues)
Petr Sojka and Martin Líška
Lunch (12:30 – 14:30)
DML – OpenMath (14:30 – 16:00)
Tea Break (16:00 – 16:30)
DML – OpenMath (16:30 – 17:30)
Thursday, July 21th 2011
DML (9:00 – 10:30)
Coffee Break (10:30 – 11:00)
DML (11:00 – 12:30)
Lunch (12:30 – 14:30)
Excursion
Friday, July 22th 2011
9:30 Invited talk 3
Coffee Break (10:30 – 11:00)
Session 7 (Calculemus 2): 11:00 – 12:30
- 11:00 Proof assistant decision procedures for formalizing origami
Cezary Kaliszyk and Tetsuo Ida
- 11:30 Retargeting OpenAxiom To Poly/ML: Towards an Integrated PA and CAS System
Gabriel Dos Reis, David Matthews and Yue Li
- 12:00 WiP: Supporting Structured Generic Programming with Automated Deduction
Erik Katzen and Gabriel Dos Reis
- 12:15 WiP: The MathScheme Library: Some Preliminary Experiments
Jacques Carette, William Farmer, Filip Jeremic, Vincent Maccio, Russell O'Connor and Quang Tran
Lunch (12:30 – 14:30)
Session 8 (Calculemus 3); 14:30 – 16:00
- 14:30 Computer certified efficient exact reals in Coq
Bas Spitters and Robbert Krebbers
- 15:00 Incidence simplicial matrices formalized in Coq/SSReflect
Jónathan Heras, María Poza, Maxime Dénès and Laurence Rideau
- 15:30 View of computer algebra data from Coq
Vladimir Komendantsky, Alexander Konovalov and Stephen Linton
Tea Break (16:00 – 16:30)
Session 9 (Calculemus 4): 16:30 – 17:30
- 16:30 Efficient formal verification of bounds of linear programs
Alexey Solovyev and Thomas Hales
- 17:00 Using Theorema in the Formalization of Theoretical Economics
Manfred Kerber, Colin Rowat and Wolfgang Windsteiger
- 17:30 Short break
Calculemus business meeting (17:40 – 18:30)