CICM
Calculemus
DML
MKM
Systems & Projects
Doctoral Programme
Work in Progress
MathUI
OpenMath
Notion of Proof
ThEdu

You must enable JavaScript to use this site

- General Information
- Call for Papers
- Important Dates
- Local Info & Venue
- Travel Information
- Hotel Information
- Programme Overview
- Day schedule
- All Talks and Events
- Registration
- Programme Committees
- Local Organizers
- Poster CICM 2014

Day Programme Monday

Monday
8:00 - 9:00	Registration
9:00 - 10:00	Mathematical Knowledge ManagementChair: Josef Urban, Room (amphitheatre) Pedro Nunes (1st floor) Jacques Carette, William Farmer and Michael Kohlhase. Realms: A Structure for Consolidating Knowledge about Mathematical Theories (9:00 - 9:30) (DOI) Cezary Kaliszyk and Florian Rabe. Towards Knowledge Management for HOL Light (9:30 - 10:00) (Slides) (DOI)	OpenMath WorkshopRoom (amphitheatre) 2.4 (2nd floor) Lars Hellström. The eval symbol for axiomatising variadic functions (9:00-9:20) Michael Kohlhase. OpenMath Language Extensions (9:20-9:40) Michael Kohlhase. Extension Proposal: Records in Pragmatic OpenMath (9:40-10:00)
10:00 - 10:30	Coffee
10:30 - 12:30	Mathematical Knowledge ManagementChair: Freek Wiedijk/Stephen Watt, Room (amphitheatre) Pedro Nunes (1st floor) Thibault Gauthier and Cezary Kaliszyk. Matching concepts across HOL libraries (10:30-11:00) (DOI) Sana Stojanovic, Julien Narboux, Marc Bezem and Predrag Janicic. A Vernacular for Coherent Logic (11:00-11:30) (DOI) (Invited Talk) Yves Bertot. A naive view of Homotopy Type Theory and its relation to the calculus of constructions (11:30-12:30)	OpenMath WorkshopRoom (amphitheatre) 2.4 (2nd floor) Lars Hellström. Literate Sources for Content Dictionaries: a Progress Report (10:30-10:50) Florian Rabe. MMT Objects (10:50-11:10) (Slides) James Davenport. Defining Mathematical Properties (11:10-11:30) (Slides)
12:30 - 14:30	Lunch
14:30 - 16:00	Mathematical Knowledge ManagementChair: Cezary Kaliszyk, Room (amphitheatre) Pedro Nunes (1st floor) Marco B. Caminati, Manfred Kerber, Christoph Lange and Colin Rowat. Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle? (14:30-15:00) (DOI) Fulya Horozal, Michael Kohlhase and Florian Rabe. Flexary Operators for Formalized Mathematics (15:00-15:30) (Slides) (DOI) Karol Pąk. Automated improving of proof legibility in the Mizar system (15:30-16:00) (DOI)	OpenMath WorkshopRoom (amphitheatre) 2.4 (2nd floor) OpenMath Business Meeting, discussion of proposals (14:30-16:00)
16:00 - 16:30	Coffee
16:30 - 18:00	Work-in-ProgressChair: Stephen Watt, Room (amphitheatre) Pedro Nunes (1st floor) Hans-Gert Graebe, Andreas Nareike and Simon Johannig. The SymbolicData Project -- Towards a Computer Algebra Social Network (16:30-17:00) Robert Pagel and Moritz Schubotz. Mathematical Language Processing Project (17:00-17:30) Reinhard Kahle. Towards the Structure of Mathematical Proof (17:30-18:00)	Doctoral ProgrammeChair: David Wilson, Room (amphitheatre) 2.4 (2nd floor) Ieuan Evans. Mathematical Document Classification via the Pachinko Allocation Model (16:30-17:00) Washington Segundo. Formalizing a named calculus modulo alpha-equivalence (17:00-17:30) Denise Torrão. Algebraic Algorithms for Numerical Semigroups (17:30-18:00)
20:00 -

News
- CICM 2015 will be in Washington DC
- Photos of CICM available here (All photos)
- CICM 2014 is over
- Slides of talks online
- Talks linked to the electronic publications

Privacy policy and legal information

Last modified: March 12 2026 21:47:00 CET