Christian Sternagel

Akihisa Yamada

Arch. Formal Proofs, 2021

Regular Tree Relations.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2021

2020

A Formalization of Knuth-Bendix Orders.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2020

Certifying the Weighted Path Order (Invited Talk).

[BibT_eX]

[DOI]

Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

2019

Abstract Completion, Formalized.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2019

Reachability Analysis for Termination and Confluence of Rewriting.

[BibT_eX]

[DOI]

Akihisa Yamada

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

nonreach - A Tool for Nonreachability Analysis.

[BibT_eX]

[DOI]

Florian Meßner

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

The Termination and Complexity Competition.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Certified ACKBO.

[BibT_eX]

[DOI]

Alexander Lochmann

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

Certified Equational Reasoning via Ordered Completion.

[BibT_eX]

[DOI]

Sarah Winkler

Proceedings of the Automated Deduction - CADE 27, 2019

2018

TTT2 with Termination Templates for Teaching.

[BibT_eX]

[DOI]

Jonas Schöpf

CoRR, 2018

Certified Ordered Completion.

[BibT_eX]

[DOI]

Sarah Winkler

CoRR, 2018

The remote_build Tool.

[BibT_eX]

[DOI]

CoRR, 2018

First-Order Terms.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2018

A Formally Verified Solver for Homogeneous Linear Diophantine Equations.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

2017

Certified Non-Confluence with ConCon 1.5.

[BibT_eX]

[DOI]

Jasmin Christian Blanchette

CoRR, 2017

Homogeneous Linear Diophantine Equations.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2017

HOLCF-Prelude.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2017

Infinite Runs in Abstract Completion.

[BibT_eX]

[DOI]

Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction, 2017

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic.

[BibT_eX]

[DOI]

Julian Biendarra

Proceedings of the Frontiers of Combining Systems - 11th International Symposium, 2017

Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 26, 2017

2016

A Characterization of Quasi-Decreasingness.

[BibT_eX]

[DOI]

CoRR, 2016

Formalized Confluence of Quasi-Decreasing, Strongly Deterministic Conditional TRSs.

[BibT_eX]

[DOI]

CoRR, 2016

Level-Confluence of 3-CTRSs in Isabelle/HOL.

[BibT_eX]

[DOI]

CoRR, 2016

The Generalized Subterm Criterion in TTT2.

[BibT_eX]

[DOI]

CoRR, 2016

A Short Mechanized Proof of the Church-Rosser Theorem by the Z-property for the λβ-calculus in Nominal Isabelle.

[BibT_eX]

[DOI]

Julian Nagele

Vincent van Oostrom

CoRR, 2016

The Z Property.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2016

Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion.

[BibT_eX]

[DOI]

Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction, 2016

AC Dependency Pairs Revisited.

[BibT_eX]

[DOI]

Proceedings of the 25th EACSL Annual Conference on Computer Science Logic, 2016

2015

Deriving class instances for datatypes.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2015

Certification of Complexity Proofs using CeTA.

[BibT_eX]

[DOI]

Martin Avanzini

Proceedings of the 26th International Conference on Rewriting Techniques and Applications, 2015

Deriving Comparators and Show Functions in Isabelle/HOL.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

2014

Certified Kruskal's Tree Theorem.

[BibT_eX]

[DOI]

J. Formaliz. Reason., 2014

A Framework for Developing Stand-Alone Certifiers.

[BibT_eX]

[DOI]

Proceedings of the Ninth Workshop on Logical and Semantic Frameworks, with Applications, 2014

The Certification Problem Format.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Eleventh Workshop on User Interfaces for Theorem Provers, 2014

Certification Monads.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

XML.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

Haskell's Show-Class in Isabelle/HOL.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

Imperative Insertion Sort.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs.

[BibT_eX]

[DOI]

Proceedings of the Rewriting and Typed Lambda Calculi - Joint International Conference, 2014

A New and Formalized Proof of Abstract Completion.

[BibT_eX]

[DOI]

Nao Hirokawa

Aart Middeldorp

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

2013

Proof Pearl - A Mechanized Proof of GHC's Mergesort.

[BibT_eX]

[DOI]

J. Autom. Reason., 2013

A Haskell Library for Term Rewriting.

[BibT_eX]

[DOI]

Bertram Felgenhauer

Martin Avanzini

CoRR, 2013

Certified HLints with Isabelle/HOLCF-Prelude.

[BibT_eX]

[DOI]

CoRR, 2013

Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion.

[BibT_eX]

[DOI]

Proceedings of the 24th International Conference on Rewriting Techniques and Applications, 2013

2012

Recording Completion for Finding and Certifying Proofs in Equational Logic

[BibT_eX]

[DOI]

CoRR, 2012

A Relative Dependency Pair Framework

[BibT_eX]

[DOI]

CoRR, 2012

Certification extends Termination Techniques

[BibT_eX]

[DOI]

CoRR, 2012

CeTA - A Tool for Certified Termination Analysis

[BibT_eX]

[DOI]

CoRR, 2012

Getting Started with Isabelle/jEdit

[BibT_eX]

[DOI]

CoRR, 2012

A Locale for Minimal Bad Sequences

[BibT_eX]

[DOI]

CoRR, 2012

Well-Quasi-Orders.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2012

Certification of Nontermination Proofs.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

2011

Executable Transitive Closures of Finite Relations.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2011

Efficient Mergesort.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2011

Modular and Certified Semantic Labeling and Unlabeling.

[BibT_eX]

[DOI]

Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, 2011

Termination of Isabelle Functions via Termination of Rewriting.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

Generalized and Formalized Uncurrying.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 8th International Symposium, 2011

2010

Loops under Strategies ... Continued

[BibT_eX]

[DOI]

Proceedings of the Proceedings International Workshop on Strategies in Rewriting, 2010

Executable Multivariate Polynomials.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2010

Executable Matrix Operations on Matrices of Arbitrary Dimensions.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2010

Abstract Rewriting.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2010

Finding and Certifying Loops.

[BibT_eX]

[DOI]

Proceedings of the SOFSEM 2010: Theory and Practice of Computer Science, 2010

Certified Subterm Criterion and Certified Usable Rules.

[BibT_eX]

[DOI]

Proceedings of the 21st International Conference on Rewriting Techniques and Applications, 2010

Signature Extensions Preserve Termination - An Alternative Proof via Dependency Pairs.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 24th International Workshop, 2010

2009

Certification of Termination Proofs Using CeTA.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

Loops under Strategies.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 20th International Conference, 2009

Tyrolean Termination Tool 2.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 20th International Conference, 2009

2008

Transforming SAT into Termination of Rewriting.

[BibT_eX]

[DOI]

Harald Zankl

Aart Middeldorp

Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming, 2008

Root-Labeling.

[BibT_eX]

[DOI]