| 2015 | A First Class Boolean Sort in First-Order Theorem Proving and TPTP. Evgenii Kotelnikov, Laura Kovács, Andrei Voronkov |
| 2015 | A Flexiformal Model of Knowledge Dissemination and Aggregation in Mathematics. Mihnea Iancu, Michael Kohlhase |
| 2015 | A Survey on Retrieval of Mathematical Knowledge. Ferruccio Guidi, Claudio Sacerdoti Coen |
| 2015 | Automating Change of Representation for Proofs in Discrete Mathematics. Daniel Raggi, Alan Bundy, Gudmund Grov, Alison Pease |
| 2015 | Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library. Kazuhisa Nakasho, Yasunari Shidama |
| 2015 | Enabling Symbolic and Numerical Computations in HOL Light. Ons Seddiki, Cvetan Dunchev, Sanaz Khan Afshar, Sofiène Tahar |
| 2015 | Formal Logic Definitions for Interchange Languages. Feryal Fulya Horozal, Florian Rabe |
| 2015 | Formalizing Physics: Automation, Presentation and Foundation Issues. Cezary Kaliszyk, Josef Urban, Umair Siddique, Sanaz Khan Afshar, Cvetan Dunchev, Sofiène Tahar |
| 2015 | Generic Literals. Florian Rabe |
| 2015 | Growing the Digital Repository of Mathematical Formulae with Generic Sources. Howard S. Cohl, Moritz Schubotz, Marjorie A. McClain, Bonita V. Saunders, Cherry Y. Zou, Azeem S. Mohammed, Alex A. Danoff |
| 2015 | Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, Volker Sorge |
| 2015 | LeoPARD - A Generic Platform for the Implementation of Higher-Order Reasoners. Max Wisniewski, Alexander Steen, Christoph Benzmüller |
| 2015 | Math Literate Knowledge Management via Induced Material. Mihnea Iancu, Michael Kohlhase |
| 2015 | Math Search for the Masses: Multimodal Search Interfaces and Appearance-Based Retrieval. Richard Zanibbi, Awelemdy Orakwue |
| 2015 | Mining the Archive of Formal Proofs. Jasmin Christian Blanchette, Max W. Haslbeck, Daniel Matichuk, Tobias Nipkow |
| 2015 | Mizar: State-of-the-art and Beyond. Grzegorz Bancerek, Czeslaw Bylinski, Adam Grabowski, Artur Kornilowicz, Roman Matuszewski, Adam Naumowicz, Karol Pak, Josef Urban |
| 2015 | Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof. Luís Cruz-Filipe, Peter Schneider-Kamp |
| 2015 | Performance Evaluation and Optimization of Math-Similarity Search. Qun Zhang, Abdou Youssef |
| 2015 | Ranking/Unranking of Lambda Terms with Compressed de Bruijn Indices. Paul Tarau |
| 2015 | Readable Formalization of Euler's Partition Theorem in Mizar. Karol Pak |
| 2015 | Semantic Enrichment of Mathematics via 'tooltips'. Ross Moore |
| 2015 | Strategies for Parallel Markup. Bruce R. Miller |
| 2015 | Structure Formation in Large Theories. Serge Autexier, Dieter Hutter |
| 2015 | TIP: Tons of Inductive Problems. Koen Claessen, Moa Johansson, Dan Rosén, Nicholas Smallbone |
| 2015 | Tools for MML Environment Analysis. Adam Naumowicz |
| 2015 | Towards Formal Fault Tree Analysis Using Theorem Proving. Waqar Ahmad, Osman Hasan |
| 2015 | Towards the Formalization of Fractional Calculus in Higher-Order Logic. Umair Siddique, Osman Hasan, Sofiène Tahar |
| 2015 | Type Inference for ZFH. Steven Obua, Jacques D. Fleuriot, Phil Scott, David Aspinall |