Abstract is missing.
- Enumeration of AG-GroupoidsAndreas Distler, Muhammad Shah, Volker Sorge. 1-14 [doi]
- Retargeting OpenAxiom to Poly/ML: Towards an Integrated Proof Assistants and Computer Algebra System FrameworkGabriel Dos Reis, David Matthews, Yue Li. 15-29 [doi]
- Incidence Simplicial Matrices Formalized in Coq/SSReflectJónathan Heras, María Poza, Maxime Dénès, Laurence Rideau. 30-44 [doi]
- Proof Assistant Decision Procedures for Formalizing OrigamiCezary Kaliszyk, Tetsuo Ida. 45-57 [doi]
- Using ::::Theorema:::: in the Formalization of Theoretical EconomicsManfred Kerber, Colin Rowat, Wolfgang Windsteiger. 58-73 [doi]
- View of Computer Algebra Data from CoqVladimir Komendantsky, Alexander Konovalov, Steve Linton. 74-89 [doi]
- Computer Certified Efficient Exact Reals in CoqRobbert Krebbers, Bas Spitters. 90-106 [doi]
- A Foundational View on Integration ProblemsFlorian Rabe, Michael Kohlhase, Claudio Sacerdoti Coen. 107-122 [doi]
- Efficient Formal Verification of Bounds of Linear ProgramsAlexey Solovyev, Thomas C. Hales. 123-132 [doi]
- Large Formal Wikis: Issues and SolutionsJesse Alama, Kasper Brink, Lionel Mamane, Josef Urban. 133-148 [doi]
- Licensing the Mizar Mathematical LibraryJesse Alama, Michael Kohlhase, Lionel Mamane, Adam Naumowicz, Piotr Rudnicki, Josef Urban. 149-163 [doi]
- Workflows for the Management of Change in Science, Technologies, Engineering and MathematicsSerge Autexier, Catalin David, Dominik Dietrich, Michael Kohlhase, Vyacheslav Zholudev. 164-179 [doi]
- Parsing and Disambiguation of Symbolic Mathematics in the Naproche SystemMarcos Cramer, Peter Koepke, Bernhard Schröder. 180-195 [doi]
- Interleaving StrategiesBastiaan Heeren, Johan Jeuring. 196-211 [doi]
- Combining Source, Content, Presentation, Narration, and Relational RepresentationFulya Horozal, Alin Iacob, Constantin Jucovschi, Michael Kohlhase, Florian Rabe. 212-227 [doi]
- Indexing and Searching Mathematics in Digital Libraries - Architecture, Design and Scalability IssuesPetr Sojka, Martin Líska. 228-243 [doi]
- Isabelle as Document-Oriented Proof AssistantMakarius Wenzel. 244-259 [doi]
- Towards Formal Proof Script RefactoringIain Whiteside, David Aspinall, Lucas Dixon, Gudmund Grov. 260-275 [doi]
- mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical LibraryJesse Alama. 276-277 [doi]
- Formalization of Formal Topology by Means of the Interactive Theorem Prover MatitaAndrea Asperti, Maria Emilia Maietti, Claudio Sacerdoti Coen, Giovanni Sambin, Silvio Valentini. 278-280 [doi]
- Project EuDML - A First Year DemonstrationJosé Luis Borbinha, Thierry Bouche, Aleksander Nowinski, Petr Sojka. 281-284 [doi]
- A Symbolic Companion for Interactive Geometric SystemsFrancisco Botana. 285-286 [doi]
- MathScheme: Project DescriptionJacques Carette, William M. Farmer, Russell O Connor. 287-288 [doi]
- Project Abstract: Logic Atlas and Integrator (LATIN)Mihai Codescu, Fulya Horozal, Michael Kohlhase, Till Mossakowski, Florian Rabe. 289-291 [doi]
- The LaTeXML Daemon: Editable Math on the Collaborative WebDeyan Ginev, Heinrich Stamerjohanns, Bruce R. Miller, Michael Kohlhase. 292-294 [doi]
- A System for Computing and Reasoning in Algebraic TopologyJónathan Heras, Vico Pascual, Julio Rubio. 295-297 [doi]
- Learning2ReasonDaniel Kühlwein, Josef Urban, Evgeni Tsivtsivadze, Herman Geuvers, Tom Heskes. 298-300 [doi]
- A Formalization of the C99 Standard in HOL, Isabelle and CoqRobbert Krebbers, Freek Wiedijk. 301-303 [doi]
- System Description: EgoMath2 As a Tool for Mathematical Searching on Wikipedia.orgJozef Misutka, Leo Galambos. 307-309 [doi]