General Information
visiting researcher
| address: | School of Information Science Japan Advanced Institute of Science and Technology 1-1 Asahidai, Nomi, Ishikawa, 923-1292, Japan |
| email: | c-sterna@jaist.ac.jp |
| research group: | Ogawa-Hirokawa Laboratory (room I-51) |
| research interests: |
term rewriting (termination and certification of termination proofs) interactive theorem proving ttt2 IsaFoR/CeTA |
Publications
Papers in Proceedings
Certification of Nontermination Proofs
In Proceedings of the 3rd International Conference on Interactive Theorem Proving (ITP '12),
Lecture Notes in Computer Science, to appear.
Generalized and Formalized Uncurrying
In Proceedings of the 8th International Symposium on Frontiers of Combining Systems (FroCoS '11),
Lecture Notes in Artificial Intelligence 6989, pp. 243–258, 2011.© Springer-Verlag
Termination of Isabelle Functions via Termination of Rewriting
In Proceedings of the 2nd International Conference on Interactive Theorem Proving (ITP '11),
Lecture Notes in Computer Science 6898, pp. 152–167, 2011.© Springer-Verlag
Modular and Certified Semantic Labeling and Unlabeling
In Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA '11),
Leibniz International Proceedings in Informatics 10, pp. 329–344, 2011. Schloss Dagstuhl
Loops under Strategies ... Continued
In Proceedings of the 1st International Workshop on Strategies in Rewriting, Poving, and Programming (IWS '10),
Electronic Proceedings in Theoretical Computer Science 44, pp. 51–65, 2010. 10.4204/EPTCS.44
Signature Extensions Preserve Termination - An Alternative Proof via Dependency Pairs
In Proceedings of the 19th EACSL Annual Conference on Computer Science Logic (CSL '10),
Lecture Notes in Computer Science 6247, pp. 514–528, 2010.© Springer-Verlag
Certified Subterm Criterion and Certified Usable Rules
In Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA '10),
Leibniz International Proceedings in Informatics 6, pp. 325–340, 2010. Schloss Dagstuhl
Finding and Certifying Loops
In Proceedings of the 36th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM '10),
Lecture Notes in Computer Science 5901, pp. 755–766, 2010.© Springer-Verlag
Certification of Termination Proofs using CeTA
In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs '09),
Lecture Notes in Computer Science 5674, pp. 452–468, 2009.© Springer-Verlag
Transforming SAT into Termination of Rewriting
In Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP '08),
Electronic Notes in Theoretical Computer Science 246, pp. 199–214, 2009.© Elsevier B.V.
Tyrolean Termination Tool 2
In Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA '09),
Lecture Notes in Computer Science 5595, pp. 295–304, 2009.© Springer-Verlag
Loops under Strategies
In Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA '09),
Lecture Notes in Computer Science 5595, pp. 17–31, 2009.© Springer-Verlag
Root-Labeling
In Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA '08),
Lecture Notes in Computer Science 5117, pp. 336–350, 2008.© Springer-Verlag
erratum
Thesis
Automatic Certification of Termination Proofs
PhD Thesis, 2010.
Others
Well-Quasi-Orders
In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors, The Archive of Formal Proofs.
April 2012. Formal proof development.
Recording Completion for Finding and Certifying Proofs in Equational Logic
In Proceedings of the 1st International Workshop on Confluence (IWC '12),
to appear.
A Relative Dependency Pair Framework
In Proceedings of the 13rd International Workshop on Termination (WST '12),
pp. 79–83, 2012.
Efficient Mergesort
In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors, The Archive of Formal Proofs.
November 2011. Formal proof development.
Executable Transitive Closures of Finite Relations
In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors, The Archive of Formal Proofs.
March 2011. Formal proof development.
Executable Multivariate Polynomials
In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors, The Archive of Formal Proofs.
August 2010. Formal proof development.
Certification extends Termination Techniques
In Proceedings of the 11st International Workshop on Termination (WST '10),
2010.
Loops under Strategies ... Continued
In Proceedings of the 1st International Workshop on Strategies in Rewriting, Poving, and Programming (IWS '10),
2010.
Executable Matrix Operations on Matrices of Arbitrary Dimensions
In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors, The Archive of Formal Proofs.
June 2010. Formal proof development.
Abstract Rewriting
In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors, The Archive of Formal Proofs.
June 2010. Formal proof development.
CeTA - A Tool for Certified Termination Analysis
In Proceedings of the 10th International Workshop on Termination (WST '09),
2009.
Software
| ttt2 | A termination tool, which automatically generates a termination certificate for a given term rewrite system. |
| IsaFoR/CeTA | IsaFoR is an
Isabelle/HOL
formalization of term rewriting and many facts about termination. CeTA is a verified certifier (for termination certificates) and code-generated from IsaFoR. |