Publications in 2018

MaedMax: A Maximal Ordered Completion Tool
Sarah Winkler, Georg Moser
Proceedings of the 9th International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence 10900, pp. 472 – 480, 2018.

Confluence Competition 2018
Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani, Harald Zankl
Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 108, pp. 32:1 – 32:5, 2018.

ProTeM: A Proof Term Manipulator (System Description)
Christina Kohl, Aart Middeldorp
Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 108, pp. 31:1 – 31:8, 2018.

Completion for Logically Constrained Rewriting
Sarah Winkler, Aart Middeldorp
Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 108, pp. 30:1 – 30:18, 2018.

A Formalization of the LLL Basis Reduction Algorithm
Jose Divasón, Sebastiaan Joosten, René Thiemann, Akihisa Yamada
Proceedings of the 9th International Conference on Interactive Theorem Proving, Lecture Notes in Computer Science 10895, pp. 160 – 177, 2018.

A Formally Verified Solver for Homogeneous Linear Diophantine Equations
Florian Meßner, Julian Parsert, Jonas Schöpf, Christian Sternagel
9th International Conference on Interactive Theorem Proving, Lecture Notes in Computer Science 10895, pp. 441 – 458, 2018.

Cops and CoCoWeb: Infrastructure for Confluence Tools
Nao Hirokawa, Julian Nagele, Aart Middeldorp
Proceedings of the 9th International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence 10900, pp. 346 – 353, 2018.

FORT 2.0
Franziska Rapp, Aart Middeldorp
Proceedings of the 9th International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence 10900, pp. 81 – 88, 2018.

Mechanizing Confluence: Automated and Certified Analysis of First- and Higher-Order Rewrite Systems
Julian Nagele
PhD thesis, University of Innsbruck, 2017.

Elementary equivalence in Artin groups of finite type
Arpan Kabira, T. V. H. Prathamesh, Rishi Vyas
International Journal of Algebra and Computation 28, pp. 331-344, 2018.

Efficient Certification of Complexity Proofs – Formalizing the Perron-Frobenius Theorem
Jose Divasón, Sebastiaan Joosten, Ondřej Kunčar, René Thiemann, Akihisa Yamada
7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018),   pp. 2-13, 2018.

Formal Microeconomic Foundations and the First Welfare Theorem
Julian Parsert, Cezary Kaliszyk
7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018),   pp. 91-101, 2018.