Abstract is missing.
- Dependencies in Formal Mathematics: Applications and Extraction for Coq and MizarJesse Alama, Lionel Mamane, Josef Urban. 1-16 [doi]
- Proof, Message and CertificateAndrea Asperti. 17-31 [doi]
- Challenges and Experiences in Managing Large-Scale ProofsTimothy Bourke, Matthias Daum, Gerwin Klein, Rafal Kolanski. 32-48 [doi]
- Semantic Alliance: A Framework for Semantic AlliesCatalin David, Constantin Jucovschi, Andrea Kohlhase, Michael Kohlhase. 49-64 [doi]
- Extending MKM Formats at the Statement LevelFulya Horozal, Michael Kohlhase, Florian Rabe. 65-80 [doi]
- A Streaming Digital Ink Framework for Multi-party CollaborationRui Hu, Vadim Mazalov, Stephen M. Watt. 81-95 [doi]
- Cost-Effective Integration of MKM Semantic Services into Editing EnvironmentsConstantin Jucovschi. 96-110 [doi]
- Understanding the Learners' Actions when Using Mathematics Learning ToolsPaul Libbrecht, Sandra Rebholz, Daniel Herding, Wolfgang Müller, Felix Tscheulin. 111-126 [doi]
- Towards Understanding Triangle Construction ProblemsVesna Marinkovic, Predrag Janicic. 127-142 [doi]
- A Query Language for Formal Mathematical LibrariesFlorian Rabe. 143-158 [doi]
- Abramowitz and Stegun - A Resource for Mathematical Document AnalysisAlan P. Sexton. 159-168 [doi]
- Point-and-Write - Documenting Formal Mathematics by ReferenceCarst Tankink, Christoph Lange 0002, Josef Urban. 169-185 [doi]
- An Essence of SSReflectIain Whiteside, David Aspinall, Gudmund Grov. 186-201 [doi]
- Theory Presentation CombinatorsJacques Carette, Russell O'Connor. 202-215 [doi]
- Verifying an Algorithm Computing Discrete Vector Fields for Digital ImagingJónathan Heras, María Poza, Julio Rubio. 216-230 [doi]
- Towards the Formal Specification and Verification of Maple ProgramsMuhammad Taimoor Khan 0001, Wolfgang Schreiner. 231-247 [doi]
- Formalizing Frankl's Conjecture: FC-FamiliesFilip Maric, Miodrag Zivkovic, Bojan Vuckovic. 248-263 [doi]
- CDCL-Based Abstract State Transition System for Coherent LogicMladen Nikolic, Predrag Janicic. 264-279 [doi]
- Speeding Up Cylindrical Algebraic Decomposition by Gröbner BasesDavid J. Wilson, Russell J. Bradford, James H. Davenport. 280-294 [doi]
- A System for Axiomatic ProgrammingGabriel Dos Reis. 295-309 [doi]
- Reasoning on Schemata of FormulæMnacho Echenim, Nicolas Peltier. 310-325 [doi]
- Management of Change in Declarative LanguagesMihnea Iancu, Florian Rabe. 326-341 [doi]
- MathWebSearch 0.5: Scaling an Open Formula Search EngineMichael Kohlhase, Bogdan Matican, Corneliu-Claudiu Prodescu. 342-357 [doi]
- Real Algebraic Strategies for MetiTarski ProofsGrant Olney Passmore, Lawrence C. Paulson, Leonardo Mendonça de Moura. 358-370 [doi]
- A Combinator Language for Theorem DiscoveryPhil Scott, Jacques D. Fleuriot. 371-385 [doi]
- DynGenPar - A Dynamic Generalized Parser for Common Mathematical LanguageKevin Kofler, Arnold Neumaier. 386-401 [doi]
- Writing on CloudsVadim Mazalov, Stephen M. Watt. 402-416 [doi]
- A Web Interface for MatitaAndrea Asperti, Wilmer Ricciotti. 417-421 [doi]
- MaxTract: Converting PDF to $\mbox\LaTeX$ , MathML and TextJosef B. Baker, Alan P. Sexton, Volker Sorge. 422-426 [doi]
- New Developments in Parsing MizarCzeslaw Bylinski, Jesse Alama. 427-431 [doi]
- Open Geometry Textbook: A Case Study of Knowledge Acquisition via Collective Intelligence - (Project Description)Xiaoyu Chen, Wei Li, Jie Luo, Dongming Wang. 432-437 [doi]
- Project Presentation: Algorithmic Structuring and Compression of Proofs (ASCOP)Stefan Hetzl. 438-442 [doi]
- On Formal Specification of Maple ProgramsMuhammad Taimoor Khan 0001, Wolfgang Schreiner. 443-447 [doi]
- The Planetary Project: Towards eMath3.0Michael Kohlhase. 448-452 [doi]
- Tentative Experiments with Ellipsis in MizarArtur Kornilowicz. 453-457 [doi]
- Reimplementing the Mathematics Subject Classification (MSC) as a Linked Open DatasetChristoph Lange 0002, Patrick Ion, Anastasia Dimou, Charalampos Bratsas, Joseph Corneli, Wolfram Sperber, Michael Kohlhase, Ioannis Antoniou. 458-462 [doi]
- The Distributed Ontology Language (DOL): Ontology Integration and Interoperability Applied to Mathematical FormalizationChristoph Lange 0002, Oliver Kutz, Till Mossakowski, Michael Grüninger. 463-467 [doi]
- Isabelle/jEdit - A Prover IDE within the PIDE FrameworkMakarius Wenzel. 468-471 [doi]