Publications in 2016
Bar Recursion over Finite Partial Functions
Paulo Oliva and Thomas Powell
Annals of Pure and Applied Logic 2016.
Distance-Integrated Combinatorial Testing
Eun-Hye Choi, Cyrille Artho, Takashi Kitamura, Osamu Mizuno, and Akihisa Yamada
Proceedings of the 27th International Symposium on Software Reliability Engineering (ISSRE 2016),
pp. 93 – 104,
2016.
The Factorization Algorithm of Berlekamp and Zassenhaus
Jose Divasón and Sebastiaan Joosten and René Thiemann and Akihisa Yamada
Archive of Formal Proofs 2016.
Improving Statistical Linguistic Algorithms for Parsing Mathematics
Cezary Kaliszyk, Josef Urban, Jiri Vyskočil
11th International Workshop on the Implementation of Logics,
EPiC 40,
pp. 27-36,
2016.
Greedy Combinatorial Test Case Generation using Unsatisfiable Cores
Akihisa Yamada, Armin Biere, Cyrille Artho, Takashi Kitamura, and Eun-Hye Choi
Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering (ASE 2016),
pp. 614 – 624,
2016.
AC Dependency Pairs Revisited
Akihisa Yamada, Christian Sternagel, René Thiemann, and Keiichirou Kusakari
Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL 2016),
Leibniz International Proceedings in Informatics 62,
pp. 8:1 – 8:16,
2016.
Algebraic Numbers in Isabelle/HOL
René Thiemann and Akihisa Yamada
Proceedings of the 7th International Conference on Interactive Theorem Proving (ITP 2016),
Lecture Notes in Computer Science 9807,
pp. 391 – 408,
2016.
Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems
Julian Nagele and Aart Middeldorp
Proceedings of the 7th International Conference on Interactive Theorem Proving (ITP 2016),
Lecture Notes in Computer Science 9807,
pp. 290 – 306,
2016.
What’s in a Theorem Name?
David Aspinall and Cezary Kaliszyk
Proceedings of the 7th Interactive Theorem Proving (ITP 2016),
Lecture Notes in Computer Science 9807,
pp. 459 – 465,
2016.
No Choice: Reconstruction of First-order ATP Proofs without Skolem Function
Michael Färber, Cezary Kaliszyk
5th Workshop on Practical Aspects of Automated Reasoning,
CEUR-WS 1635,
pp. 24-31,
2016.
TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism
Cezary Kaliszyk, Geoff Sutcliffe, Florian Rabe
5th Workshop on Practical Aspects of Automated Reasoning,
CEUR-WS 1635,
pp. 41-55,
2016.
Gödel’s Functional Interpretation and the Concept of Learning
Thomas Powell
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016),
pp. 136 – 145,
2016.
Normalisation by Random Descent
Vincent van Oostrom and Yoshihito Toyama
Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016),
Leibniz International Proceedings in Informatics 52,
pp. 32:1 – 32:18,
2016.
Interaction Automata and the ia2d Interpreter
Stéphane Gimenez and David Obwaller
Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016),
Leibniz International Proceedings in Informatics 52,
pp. 35:1 – 35:11,
2016.
Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion
Christian Sternagel and Thomas Sternagel
Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016),
Leibniz International Proceedings in Informatics 52,
pp. 29:1-29:16,
2016.
Goal Translation for a Hammer for Coq
Łukasz Czajka and Cezary Kaliszyk
1st International Workshop on Hammers for Type Theories,
EPTCS 210,
pp. 13-20,
2016.
Complexity of Acyclic Term Graph Rewriting
Martin Avanzini and Georg Moser
Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016),
Leibniz International Proceedings in Informatics 52,
pp. 10:1 – 10:18,
2016.
Automating the First-Order Theory of Left-Linear Right-Ground Term Rewrite Systems
Franziska Rapp and Aart Middeldorp
Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016),
Leibniz International Proceedings in Informatics 52,
pp. 36:1 – 36:12,
2016.
A combination framework for complexity
Martin Avanzini and Georg Moser
Information and Computation 248,
pp. 22 – 55,
2016.
Perron-Frobenius Theorem for Spectral Radius Analysis
Jose Divasón and Ondřej Kunčar and René Thiemann and Akihisa Yamada
Archive of Formal Proofs 2016.
TcT: Tyrolean Complexity Tool
Martin Avanzini, Georg Moser and Michael Schaper
Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016),
Lecture Notes in Computer Science 9636,
pp. 407 – 423,
2016.
AC-KBO Revisited
Akihisa Yamada, Sarah Winkler, Nao Hirokawa, and Aart Middeldorp
Theory and Practice of Logic Programming 16(2),
pp. 163 – 188,
2016.
A Learning-Based Fact Selector for Isabelle/HOL
Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban
Journal of Automated Reasoning Volume 53, Number 3,
pp. 219 – 244,
2016.
Hammering towards QED
Jasmin C. Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban
Journal of Formalized Reasoning 9(1),
pp. 101 – 148,
2016.
Polynomial Factorization
René Thiemann and Akihisa Yamada
Archive of Formal Proofs 2016.
Polynomial Interpolation
René Thiemann and Akihisa Yamada
Archive of Formal Proofs 2016.
The Complexity of Interaction
Stéphane Gimenez and Georg Moser
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016),
243 – 255,
2016.
Towards a Mizar Environment for Isabelle: Foundations and Language
Cezary Kaliszyk, Karol Pąk, and Josef Urban
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016),
pp. 58 – 65,
2016.
Formalizing Jordan Normal Forms in Isabelle/HOL
René Thiemann and Akihisa Yamada
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016),
pp. 88 – 99,
2016.
Improving Automation in Interactive Theorem Provers by Efficient Encoding of Lambda-Abstractions
Łukasz Czajka
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016),
pp. 49 – 57,
2016.
Workshop on Hammers for Type Theory 2016
Jasmin Blanchette, Cezary Kaliszyk (eds)
Proceedings First Workshop on Hammers for Type Theory, HaTT 2016,
210,
2016.