WEDNESDAY 09:00-09:30 Registration (JCMB room 2511) 09:30-10:30 Klaus Grue (invited talk) LogiWeb 10:30-11:00 BREAK (coffee/tea/snacks in room 2510) 11:00-11:30 Freek Wiedijk Obstacles to a global library of formal mathematics 11:30-12:00 Loic Pottier talk/demo on Wikicoqweb: Proofs for freshmen with Coqweb 12:00-12:30 Cezary Kaliszyk Teaching logic using a web interface for Coq 12:30-12:45 Further discussion of morning session 12:45-14:00 LUNCH (Sandwiches etc. in room 2510) 14:00-14:30 Carsten Schuermann Logosphere 14:30-15:00 Pierre Corbineau A prototype system for collaborative proving 15:00-15:30 Herman Geuvers Challenges to a global web-based library of formal mathematics 15:30-16:00 BREAK (coffee/tea/snacks supplied) 16:00-..... Discuss and work on proposal 19:30 Workshop DINNER at Blonde THURSDAY 09:30-10:00 Zhaohui Luo Formal Reasoning with Different Logical Foundations 10:00-10:30 Adam Naumowicz Mizar 10:30-11:00 BREAK (coffee/tea/snacks in room 2510) 11:00-11:30 Aarne Ranta Documenting and Editing Formal Mathematics in Natural Language 11:30-12:00 Hugo Herbelin Evgeny Makarov's abstract and modular formalisation of arithmetic in Coq 12:00-12:30 Alexander Konovalov Providing mathematical Web services with Symbolic Computation Software Composability Protocol 12:30-12:45 Further discussion of morning session 12:45-14:00 LUNCH (Sandwiches etc. in room 2510) 14:00-14:30 Discuss and work on proposal 14:30-15:00 Makarius Wenzel Asynchronous processing of proof documents 15:00-15:30 Lucas Dixon An Implicational Logic for Conjecturing and Distributed Proof Attempts 15:30-16:00 BREAK (coffee/tea/snacks supplied) 16:00-16:30 Christoph Lueth Collaborative Editing with PGIP 16:30-..... Further discussion (perhaps a closing panel discussion: Klaus, Pierre, Aarne, Carsten and Adam?)