Aoto T and Kikuchi K (2016), "Nominal Confluence Tool", In Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings. Vol. 9706 of Lecture Notes in Computer Science, pp. 173-182. Springer. |
BibTeX:
@inproceedings{Aoto2016, author = {Takahito Aoto and Kentaro Kikuchi}, editor = {Nicola Olivetti and Ashish Tiwari}, title = {Nominal Confluence Tool}, booktitle = {Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings}, publisher = {Springer}, year = {2016}, volume = {9706}, series = {Lecture Notes in Computer Science}, pages = {173--182}, url = {http://dx.doi.org/10.1007/978-3-319-40229-1_12}, doi = {10.1007/978-3-319-40229-1_12} } |
Suzuki T, Kikuchi K, Aoto T and Toyama Y (2016), "Critical Pair Analysis in Nominal Rewriting", In 7th International Symposium on Symbolic Computation in Software Science, SCSS 2016, Tokyo, Japan, March 28-31, 2016. Vol. 39 of EPiC Series in Computing, pp. 156-168. EasyChair. |
BibTeX:
@inproceedings{Suzuki2016, author = {Takaki Suzuki and Kentaro Kikuchi and Takahito Aoto and Yoshihito Toyama}, editor = {James H. Davenport and Fadoua Ghourabi}, title = {Critical Pair Analysis in Nominal Rewriting}, booktitle = {7th International Symposium on Symbolic Computation in Software Science, SCSS 2016, Tokyo, Japan, March 28-31, 2016}, publisher = {EasyChair}, year = {2016}, volume = {39}, series = {EPiC Series in Computing}, pages = {156--168}, url = {http://www.easychair.org/publications/paper/Critical_Pair_Analysis_in_Nominal_Rewriting} } |
Sato K, Kikuchi K, Aoto T and Toyama Y (2015), "Correctness of Context-Moving Transformations for Term Rewriting Systems", In Logic-Based Program Synthesis and Transformation - 25th International Symposium, LOPSTR 2015, Siena, Italy, July 13-15, 2015. Revised Selected Papers. Vol. 9527 of Lecture Notes in Computer Science, pp. 331-345. Springer.
[BibTeX] [DOI] [URL] [Long version] |
BibTeX:
@inproceedings{Sato2015, author = {Koichi Sato and Kentaro Kikuchi and Takahito Aoto and Yoshihito Toyama}, editor = {Moreno Falaschi}, title = {Correctness of Context-Moving Transformations for Term Rewriting Systems}, booktitle = {Logic-Based Program Synthesis and Transformation - 25th International Symposium, LOPSTR 2015, Siena, Italy, July 13-15, 2015. Revised Selected Papers}, publisher = {Springer}, year = {2015}, volume = {9527}, series = {Lecture Notes in Computer Science}, pages = {331--345}, url = {http://dx.doi.org/10.1007/978-3-319-27436-2_20}, doi = {10.1007/978-3-319-27436-2_20} } |
Sato K, Kikuchi K, Aoto T and Toyama Y (2015), "Automated Inductive Theorem Proving using Transformations of Term Rewriting Systems", Computer Software. Vol. 32(1), pp. 1_179-1_193. Japan Society for Software Science and Technology. |
BibTeX:
@article{Sato2015a, author = {Koichi Sato and Kentaro Kikuchi and Takahito Aoto and Yoshihito Toyama}, title = {Automated Inductive Theorem Proving using Transformations of Term Rewriting Systems}, journal = {Computer Software}, publisher = {Japan Society for Software Science and Technology}, year = {2015}, volume = {32}, number = {1}, pages = {1_179-1_193}, url = {http://ci.nii.ac.jp/naid/130004892317/en/}, doi = {10.11309/jssst.32.1_179} } |
Suzuki T, Kikuchi K, Aoto T and Toyama Y (2015), "Confluence of Orthogonal Nominal Rewriting Systems Revisited", In 26th International Conference on Rewriting Techniques and Applications, RTA 2015, June 29 to July 1, 2015, Warsaw, Poland. Vol. 36 of LIPIcs, pp. 301-317. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. |
BibTeX:
@inproceedings{Suzuki2015, author = {Takaki Suzuki and Kentaro Kikuchi and Takahito Aoto and Yoshihito Toyama}, editor = {Maribel Fernández}, title = {Confluence of Orthogonal Nominal Rewriting Systems Revisited}, booktitle = {26th International Conference on Rewriting Techniques and Applications, RTA 2015, June 29 to July 1, 2015, Warsaw, Poland}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik}, year = {2015}, volume = {36}, series = {LIPIcs}, pages = {301--317}, url = {http://dx.doi.org/10.4230/LIPIcs.RTA.2015.301}, doi = {10.4230/LIPIcs.RTA.2015.301} } |
Kikuchi K (2015), "Uniform Proofs of Normalisation and Approximation for Intersection Types", In Proceedings Seventh Workshop on Intersection Types and Related Systems, ITRS 2014, Vienna, Austria, 18 July 2014. Vol. 177 of EPTCS, pp. 10-23. |
BibTeX:
@inproceedings{Kikuchi2015, author = {Kentaro Kikuchi}, editor = {Jakob Rehof}, title = {Uniform Proofs of Normalisation and Approximation for Intersection Types}, booktitle = {Proceedings Seventh Workshop on Intersection Types and Related Systems, ITRS 2014, Vienna, Austria, 18 July 2014}, year = {2015}, volume = {177}, series = {EPTCS}, pages = {10--23}, url = {http://dx.doi.org/10.4204/EPTCS.177.2}, doi = {10.4204/EPTCS.177.2} } |
Kikuchi K and Sakurai T (2014), "A Translation of Intersection and Union Types for the λμ-Calculus", In Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Proceedings. Vol. 8858 of Lecture Notes in Computer Science, pp. 120-139. Springer.
[BibTeX] [DOI] [URL] [Long version] |
BibTeX:
@inproceedings{Kikuchi2014, author = {Kentaro Kikuchi and Takafumi Sakurai}, editor = {Jacques Garrigue}, title = {A Translation of Intersection and Union Types for the λμ-Calculus}, booktitle = {Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Proceedings}, publisher = {Springer}, year = {2014}, volume = {8858}, series = {Lecture Notes in Computer Science}, pages = {120--139}, url = {http://dx.doi.org/10.1007/978-3-319-12736-1_7}, doi = {10.1007/978-3-319-12736-1_7} } |
Kikuchi K (2013), "Proving Strong Normalisation via Non-deterministic Translations into Klop's Extended λ-Calculus", In Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy. Vol. 23 of LIPIcs, pp. 395-414. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. |
BibTeX:
@inproceedings{Kikuchi2013, author = {Kentaro Kikuchi}, editor = {Simona Ronchi Della Rocca}, title = {Proving Strong Normalisation via Non-deterministic Translations into Klop's Extended λ-Calculus}, booktitle = {Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik}, year = {2013}, volume = {23}, series = {LIPIcs}, pages = {395--414}, url = {http://dx.doi.org/10.4230/LIPIcs.CSL.2013.395}, doi = {10.4230/LIPIcs.CSL.2013.395} } |
Kikuchi K and Lengrand S (2008), "Strong Normalisation of Cut-Elimination That Simulates β-Reduction", In Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29 - April 6, 2008. Proceedings. Vol. 4962 of Lecture Notes in Computer Science, pp. 380-394. Springer.
[BibTeX] [DOI] [URL] [Long version] |
BibTeX:
@inproceedings{Kikuchi2008, author = {Kentaro Kikuchi and Stéphane Lengrand}, editor = {Roberto M. Amadio}, title = {Strong Normalisation of Cut-Elimination That Simulates β-Reduction}, booktitle = {Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29 - April 6, 2008. Proceedings}, publisher = {Springer}, year = {2008}, volume = {4962}, series = {Lecture Notes in Computer Science}, pages = {380--394}, url = {http://dx.doi.org/10.1007/978-3-540-78499-9_27}, doi = {10.1007/978-3-540-78499-9_27} } |
Kikuchi K (2008), "Call-by-Name Reduction and Cut-Elimination in Classical Logic", Annals of Pure and Applied Logic. Vol. 153(1-3), pp. 38-65. |
BibTeX:
@article{Kikuchi2008a, author = {Kentaro Kikuchi}, title = {Call-by-Name Reduction and Cut-Elimination in Classical Logic}, journal = {Annals of Pure and Applied Logic}, year = {2008}, volume = {153}, number = {1-3}, pages = {38--65}, url = {http://dx.doi.org/10.1016/j.apal.2008.01.002}, doi = {10.1016/j.apal.2008.01.002} } |
Ishigaki R and Kikuchi K (2007), "Tree-Sequent Methods for Subintuitionistic Predicate Logics", In Automated Reasoning with Analytic Tableaux and Related Methods, 16th International Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6, 2007, Proceedings. Vol. 4548 of Lecture Notes in Computer Science, pp. 149-164. Springer.
[BibTeX] [DOI] [URL] [Full version] |
BibTeX:
@inproceedings{Ishigaki2007, author = {Ryo Ishigaki and Kentaro Kikuchi}, editor = {Nicola Olivetti}, title = {Tree-Sequent Methods for Subintuitionistic Predicate Logics}, booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods, 16th International Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6, 2007, Proceedings}, publisher = {Springer}, year = {2007}, volume = {4548}, series = {Lecture Notes in Computer Science}, pages = {149--164}, url = {http://dx.doi.org/10.1007/978-3-540-73099-6_13}, doi = {10.1007/978-3-540-73099-6_13} } |
Ishigaki R and Kikuchi K (2007), "A Tree-Sequent Calculus for a Natural Predicate Extension of Visser's Propositional Logic", Logic Journal of the IGPL. Vol. 15(2), pp. 149-164. |
BibTeX:
@article{Ishigaki2007a, author = {Ryo Ishigaki and Kentaro Kikuchi}, title = {A Tree-Sequent Calculus for a Natural Predicate Extension of Visser's Propositional Logic}, journal = {Logic Journal of the IGPL}, year = {2007}, volume = {15}, number = {2}, pages = {149--164}, url = {http://dx.doi.org/10.1093/jigpal/jzm004}, doi = {10.1093/jigpal/jzm004} } |
Kikuchi K (2007), "Confluence of Cut-Elimination Procedures for the Intuitionistic Sequent Calculus", In Computation and Logic in the Real World, Third Conference on Computability in Europe, CiE 2007, Siena, Italy, June 18-23, 2007, Proceedings. Vol. 4497 of Lecture Notes in Computer Science, pp. 398-407. Springer.
[BibTeX] [DOI] [URL] [Full version] |
BibTeX:
@inproceedings{Kikuchi2007, author = {Kentaro Kikuchi}, editor = {S. Barry Cooper and Benedikt Löwe and Andrea Sorbi}, title = {Confluence of Cut-Elimination Procedures for the Intuitionistic Sequent Calculus}, booktitle = {Computation and Logic in the Real World, Third Conference on Computability in Europe, CiE 2007, Siena, Italy, June 18-23, 2007, Proceedings}, publisher = {Springer}, year = {2007}, volume = {4497}, series = {Lecture Notes in Computer Science}, pages = {398--407}, url = {http://dx.doi.org/10.1007/978-3-540-73001-9_41}, doi = {10.1007/978-3-540-73001-9_41} } |
Kikuchi K (2007), "Simple Proofs of Characterizing Strong Normalization for Explicit Substitution Calculi", In Term Rewriting and Applications, 18th International Conference, RTA 2007, Paris, France, June 26-28, 2007, Proceedings. Vol. 4533 of Lecture Notes in Computer Science, pp. 257-272. Springer.
[BibTeX] [DOI] [URL] [Full version] |
BibTeX:
@inproceedings{Kikuchi2007a, author = {Kentaro Kikuchi}, editor = {Franz Baader}, title = {Simple Proofs of Characterizing Strong Normalization for Explicit Substitution Calculi}, booktitle = {Term Rewriting and Applications, 18th International Conference, RTA 2007, Paris, France, June 26-28, 2007, Proceedings}, publisher = {Springer}, year = {2007}, volume = {4533}, series = {Lecture Notes in Computer Science}, pages = {257--272}, url = {http://dx.doi.org/10.1007/978-3-540-73449-9_20}, doi = {10.1007/978-3-540-73449-9_20} } |
Kikuchi K (2006), "On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus", In Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings. Vol. 4246 of Lecture Notes in Computer Science, pp. 120-134. Springer.
[BibTeX] [DOI] [URL] [Full version] |
BibTeX:
@inproceedings{Kikuchi2006, author = {Kentaro Kikuchi}, editor = {Miki Hermann and Andrei Voronkov}, title = {On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings}, publisher = {Springer}, year = {2006}, volume = {4246}, series = {Lecture Notes in Computer Science}, pages = {120--134}, url = {http://dx.doi.org/10.1007/11916277_9}, doi = {10.1007/11916277_9} } |
Kikuchi K (2004), "A Direct Proof of Strong Normalization for an Extended Herbelin's Calculus", In Functional and Logic Programming, 7th International Symposium, FLOPS 2004, Nara, Japan, April 7-9, 2004, Proceedings. Vol. 2998 of Lecture Notes in Computer Science, pp. 244-259. Springer.
[BibTeX] [DOI] [URL] [Full version] |
BibTeX:
@inproceedings{Kikuchi2004, author = {Kentaro Kikuchi}, editor = {Yukiyoshi Kameyama and Peter J. Stuckey}, title = {A Direct Proof of Strong Normalization for an Extended Herbelin's Calculus}, booktitle = {Functional and Logic Programming, 7th International Symposium, FLOPS 2004, Nara, Japan, April 7-9, 2004, Proceedings}, publisher = {Springer}, year = {2004}, volume = {2998}, series = {Lecture Notes in Computer Science}, pages = {244--259}, url = {http://dx.doi.org/10.1007/978-3-540-24754-8_18}, doi = {10.1007/978-3-540-24754-8_18} } |
Kikuchi K and Sasaki K (2003), "A Cut-Free Gentzen Formulation of Basic Propositional Calculus", Journal of Logic, Language and Information. Vol. 12(2), pp. 213-225. |
BibTeX:
@article{Kikuchi2003, author = {Kentaro Kikuchi and Katsumi Sasaki}, title = {A Cut-Free Gentzen Formulation of Basic Propositional Calculus}, journal = {Journal of Logic, Language and Information}, year = {2003}, volume = {12}, number = {2}, pages = {213--225}, url = {http://dx.doi.org/10.1023/A:1022363219134}, doi = {10.1023/A:1022363219134} } |
Kikuchi K (2002), "Dual-Context Sequent Calculus and Strict Implication", Mathematical Logic Quarterly. Vol. 48(1), pp. 87-92. |
BibTeX:
@article{Kikuchi2002, author = {Kentaro Kikuchi}, title = {Dual-Context Sequent Calculus and Strict Implication}, journal = {Mathematical Logic Quarterly}, year = {2002}, volume = {48}, number = {1}, pages = {87--92}, url = {http://dx.doi.org/10.1002/1521-3870(200201)48:1<87::AID-MALQ87>3.0.CO;2-N}, doi = {10.1002/1521-3870(200201)48:1<87::AID-MALQ87>3.0.CO;2-N} } |
Ishii K, Kashima R and Kikuchi K (2001), "Sequent Calculi for Visser's Propositional Logics", Notre Dame Journal of Formal Logic. Vol. 42(1), pp. 1-22. |
BibTeX:
@article{Ishii2001, author = {Katsumasa Ishii and Ryo Kashima and Kentaro Kikuchi}, title = {Sequent Calculi for Visser's Propositional Logics}, journal = {Notre Dame Journal of Formal Logic}, year = {2001}, volume = {42}, number = {1}, pages = {1--22}, url = {http://dx.doi.org/10.1305/ndjfl/1054301352}, doi = {10.1305/ndjfl/1054301352} } |
Kikuchi K (2001), "Relationships between Basic Propositional Calculus and Substructural Logics", Bulletin of the Section of Logic. Vol. 30(1), pp. 15-20.
[BibTeX] |
BibTeX:
@article{Kikuchi2001, author = {Kentaro Kikuchi}, title = {Relationships between Basic Propositional Calculus and Substructural Logics}, journal = {Bulletin of the Section of Logic}, year = {2001}, volume = {30}, number = {1}, pages = {15--20} } |