Publications in 2014
Machine Learning of Coq Proof Guidance: First Experiments
Cezary Kaliszyk, Lionel Mamane, and Josef Urban
Proceedings of the 6th International Symposium on Symbolic Computation in Software Science (SCSS 2014),
EasyChair Proceedings in Computer Science 30,
pp. 27 – 34,
2014.
Lifting Definition Option
René Thiemann
Archive of Formal Proofs 2014.
XML
Christian Sternagel and René Thiemann
Archive of Formal Proofs 2014.
Certification Monads
Christian Sternagel and René Thiemann
Archive of Formal Proofs 2014.
The Certification Problem Format
Christian Sternagel and René Thiemann
Proceedings of the 11th International Workshop on User Interfaces for Theorem Provers (UITP 2014),
Electronic Proceedings in Theoretical Computer Science 167,
pp. 61 – 72,
2014.
Automatic Constrained Rewriting Induction towards Verifying Procedural Programs
Cynthia Kop and Naoki Nishida
Proceedings of the 12th Asian Symposium on Programming Languages and Systems (APLAS 2014),
Lecture Notes in Computer Science 8858,
pp. 334 – 353,
2014.
Certification of Nontermination Proofs using Strategies and Nonlooping Derivations
Julian Nagele, René Thiemann, and Sarah Winkler
Proceedings of the 6th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2014),
Lecture Notes in Computer Science 8471,
pp. 216 – 232,
2014.
Challenges in Automation of Rewriting
Harald Zankl
Habilitation thesis, University of Innsbruck, 2014.
Polynomial Interpretations over the Natural, Rational and Real Numbers Revisited
Friedrich Neurauter and Aart Middeldorp
Logical Methods in Computer Science 10(3:22),
pp. 1 – 28,
2014.
Haskell’s Show-Class in Isabelle/HOL
Christian Sternagel and René Thiemann
Archive of Formal Proofs 2014.
Proving Termination of Programs Automatically with AProVE
Jürgen Giesl, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, and René Thiemann
Proceedings of the 7th International Joint Conference on Automated Reasoning (IJCAR 2014),
Lecture Notes in Computer Science 8562,
pp. 184 – 191,
2014.
Automating Elementary Interpretations
Harald Zankl, Sarah Winkler, and Aart Middeldorp
Proceedings of the 14th International Workshop on Termination (WST 2014),
pp. 75 – 79,
2014.
A New and Formalized Proof of Abstract Completion
Nao Hirokawa, Aart Middeldorp, and Christian Sternagel
Proceedings of the 5th International Conference on Interactive Theorem Proving (ITP 2014),
Lecture Notes in Computer Science 8558,
pp. 292 – 307,
2014.
Conditional Confluence (System Description)
Thomas Sternagel and Aart Middeldorp
Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014),
Lecture Notes in Computer Science 8560,
pp. 456 – 465,
2014.
Automated Complexity Analysis Based on Context-Sensitive Rewriting
Nao Hirokawa and Georg Moser
Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014),
Lecture Notes in Computer Science 8560,
pp. 257 – 271,
2014.
Amortised Resource Analysis and Typed Polynomial Interpretations
Martin Hofmann and Georg Moser
Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014),
Lecture Notes in Computer Science 8560,
pp. 272 – 286,
2014.
First-Order Formative Rules
Carsten Fuhs and Cynthia Kop
Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014),
Lecture Notes in Computer Science 8560,
pp. 240 – 256,
2014.
Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
Christian Sternagel and René Thiemann
Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014),
Lecture Notes in Computer Science 8560,
pp. 441 – 455,
2014.
Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems
Sebastiaan Joosten, Cezary Kaliszyk, and Josef Urban
Proceedings of the 12th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2014),
Electronic Proceedings in Theoretical Computer Science 152,
pp. 77 – 85,
2014.
Developing Corpus-based Translation Methods between Informal and Formal Mathematics
Cezary Kaliszyk, Josef Urban, Jiří Vyskočil, and Herman Geuvers
Proceedings of the 7th Conference on Intelligent Computer Mathematics (CICM 2014),
Logical Methods in Computer Science 8543,
pp. 435 – 439,
2014.
Towards Knowledge Management for HOL Light
Cezary Kaliszyk and Florian Rabe
Proceedings of the 7th Conference on Intelligent Computer Mathematics (CICM 2014),
Lecture Notes in Computer Science 8543,
pp. 357 – 372,
2014.
Matching Concepts across HOL Libraries
Thibault Gauthier and Cezary Kaliszyk
Proceedings of the 7th Conference on Intelligent Computer Mathematics (CICM 2014),
Lecture Notes in Computer Science 8543,
pp. 267 – 281,
2014.
Learning-Assisted Automated Reasoning with Flyspeck
Cezary Kaliszyk and Josef Urban
Journal of Automated Reasoning 53(2),
pp. 173 – 213,
2014.
Certified Kruskal’s Tree Theorem
Christian Sternagel
Journal of Formalized Reasoning 7(1),
pp. 45 – 62,
2014.
AC-KBO Revisited
Akihisa Yamada, Sarah Winkler, Nao Hirokawa, and Aart Middeldorp
Proceedings of the 12th International Symposium on Functional and Logic Programming (FLOPS 2014),
Lecture Notes in Computer Science 8475,
pp. 319 – 335,
2014.
Modular Complexity Analysis for Term Rewriting
Harald Zankl and Martin Korp
Logical Methods in Computer Science 10(1:19),
pp. 1 – 33,
2014.
Implementing field extensions of the form Q[sqrt(b)]
René Thiemann
Archive of Formal Proofs 2014.
Reachability Analysis with State-Compatible Automata
Bertram Felgenhauer and René Thiemann
Proceedings of the 8th International Conference on Language and Automata Theory and Applications (LATA 2014),
Lecture Notes in Computer Science 8370,
pp. 347 – 359,
2014.
Mutually Recursive Partial Functions
René Thiemann
Archive of Formal Proofs 2014.