The System SOL version 2020

Makoto Hamana, Kentaro Kikuchi, Date Yao Faustin Dieudonne, Kazuki Fuju

Proceedings of the 9th International Workshop on Confluence (IWC 2020)　81-81　2020/06

Polymorphic computation systems: Theory and practice of confluence with call-by-value Peer-reviewed

Makoto Hamana, Tatsuya Abe, Kentaro Kikuchi

Sci. Comput. Program.　187　102322-102322　2020

DOI： 10.1016/j.scico.2019.102322 　

Inductive Theorem Proving in Non-terminating Rewriting Systems and Its Application to Program Transformation Peer-reviewed

Kentaro Kikuchi, Takahito Aoto, Isao Sasano

Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming, PPDP 2019, Porto, Portugal, October 7-9, 2019.　13:1-13:14　2019

DOI： 10.1145/3354166.3354178 　

The System SOL version 2018

Makoto Hamana, Kentaro Kikuchi

Proceedings of the 7th International Workshop on Confluence (IWC 2018)　70-70　2018/07

ACPH: System Description for CoCo 2017

Kouta Onozawa, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

Proceedings of the 6th International Workshop on Confluence (IWC 2017)　70-70　2017/09/08

Confluence by Strong Commutation with Disjoint Parallel Reduction Peer-reviewed

Kentaro Kikuchi

Participant's Proceedings of the 4th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2017)　2017/09/08

Parallel Closure Theorem for Left-Linear Nominal Rewriting Systems Peer-reviewed

Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

Proceedings of the 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017)　LNAI 10483　115-131　2017

DOI： 10.1007/978-3-319-66167-4_7 　

ISSN： 1611-3349 0302-9743

ACPH: System Description for CoCo 2016

Kouta Onozawa, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

Proceedings of the 5th International Workshop on Confluence (IWC 2016)　76-76　2016/09/08

Nrbox: System Description for CoCo 2016

Takahito Aoto, Kentaro Kikuchi

Proceedings of the 5th International Workshop on Confluence (IWC 2016)　87-87　2016/09/08

A Rule-Based Procedure for Equivariant Nominal Unification Peer-reviewed

Takahito Aoto, Kentaro Kikuchi

Proceedings of the 8th International Workshop on Higher-Order Rewriting (HOR 2016)　2016/06/25

Critical Pair Analysis in Nominal Rewriting Peer-reviewed

Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

Proceedings of the 7th International Symposium on Symbolic Computation in Software Science (SCSS 2016)　EPiC 39　156-168　2016/03/27

DOI： 10.29007/7q54 　

Nominal Confluence Tool Peer-reviewed

Takahito Aoto, Kentaro Kikuchi

Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR 2016)　LNAI 9706　173-182　2016

DOI： 10.1007/978-3-319-40229-1_12 　

ISSN： 1611-3349 0302-9743

Correctness of Context-Moving Transformations for Term Rewriting Systems Peer-reviewed

Koichi Sato, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

Proceedings of the 25th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2015)　LNCS 9527　331-345　2015/12

DOI： 10.1007/978-3-319-27436-2_20 　

ISSN： 0302-9743

ACPH: System Description

Kouta Onozawa, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

Proceedings of the 4th International Workshop on Confluence (IWC 2015)　39-39　2015/08/02

NoCo: System Description for CoCo 2015

Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto

Proceedings of the 4th International Workshop on Confluence (IWC 2015)　48-48　2015/08/02

Context-Moving Transformation for Term Rewriting Systems (Extended Abstract) Peer-reviewed

Koichi Sato, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

Participant's Proceedings of the 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)　3-7　2015/07/02

Confluence of Orthogonal Nominal Rewriting Systems Revisited Peer-reviewed

Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA 2015)　LIPIcs 36　301-317　2015/06

DOI： 10.4230/LIPIcs.RTA.2015.301 　

ISSN： 1868-8969

項書き換えシステムの変換を利用した帰納的定理自動証明 Peer-reviewed

佐藤洸一, 菊池健太郎, 青戸等人, 外山芳人

コンピュータソフトウェア　32　(1)　179-193　2015/02

DOI： 10.11309/jssst.32.1_179 　

Uniform Proofs of Normalisation and Approximation for Intersection Types Peer-reviewed

Kentaro Kikuchi

Proceedings of the 7th Workshop on Intersection Types and Related Systems (ITRS 2014)　EPTCS 177　10-23　2015/02

DOI： 10.4204/EPTCS.177.2 　

Automated inductive theorem proving using transformations of term rewriting systems

Koichi Sato, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

Computer Software　32　(1)　179-193　2015

ISSN： 0289-6540

A Translation of Intersection and Union Types for the λμ-Calculus (short paper) Peer-reviewed

Kentaro Kikuchi, Takafumi Sakurai

Proceedings of the 5th International Workshop on Classical Logic and Computation (CL&C 2014)　2014

A Translation of Intersection and Union Types for the λμ-Calculus Peer-reviewed

Kentaro Kikuchi, Takafumi Sakurai

Proceedings of the 12th Asian Symposium on Programming Languages and Systems (APLAS 2014)　LNCS 8858　120-139　2014

DOI： 10.1007/978-3-319-12736-1_7 　

ISSN： 0302-9743

eISSN： 1611-3349

Proving Strong Normalisation via Non-deterministic Translations into Klop's Extended λ-Calculus Peer-reviewed

Kentaro Kikuchi

Proceedings of the 22nd Annual Conference of the European Association for Computer Science Logic (CSL 2013)　LIPIcs 23　395-414　2013

DOI： 10.4230/LIPIcs.CSL.2013.395 　

ISSN： 1868-8969

On General Methods for Proving Reduction Properties of Typed Lambda Terms

Kentaro Kikuchi

証明論と論理・計算の構造，京都大学数理解析研究所講究録　1635　33-50　2009

Strong Normalisation of Cut-Elimination that Simulates β-Reduction Peer-reviewed

Kentaro Kikuchi, Stéphane Lengrand

Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2008)　LNCS 4962　380-394　2008

DOI： 10.1007/978-3-540-78499-9_27 　

ISSN： 0302-9743 1611-3349

Call-by-Name Reduction and Cut-Elimination in Classical Logic Peer-reviewed

Kentaro Kikuchi

Annals of Pure and Applied Logic　153　(1-3)　38-65　2008

DOI： 10.1016/j.apal.2008.01.002 　

ISSN： 0168-0072

A Tree-Sequent Calculus for a Natural Predicate Extension of Visser's Propositional Logic Peer-reviewed

Ryo Ishigaki, Kentaro Kikuchi

Logic Journal of the Interest Group in Pure and Applied Logics　15　(2)　149-164　2007

DOI： 10.1093/jigpal/jzm004 　

ISSN： 1367-0751

Simple Proofs of Characterizing Strong Normalization for Explicit Substitution Calculi Peer-reviewed

Kentaro Kikuchi

Proceedings of the 18th International Conference on Rewriting Techniques and Applications (RTA 2007)　LNCS 4533　257-272　2007

DOI： 10.1007/978-3-540-73449-9_20 　

ISSN： 0302-9743

Confluence of Cut-Elimination Procedures for the Intuitionistic Sequent Calculus Peer-reviewed

Kentaro Kikuchi

Proceedings of the 3rd Conference on Computability in Europe (CiE 2007)　LNCS 4497　398-407　2007

DOI： 10.1007/978-3-540-73001-9_41 　

ISSN： 0302-9743 1611-3349

Tree-Sequent Methods for Subintuitionistic Predicate Logics Peer-reviewed

Ryo Ishigaki, Kentaro Kikuchi

Proceedings of the 16th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2007)　LNAI 4548　149-164　2007

DOI： 10.1007/978-3-540-73099-6_13 　

Call-by-Name Reduction and Cut-Elimination in Classical Logic Peer-reviewed

Kentaro Kikuchi

Proceedings of the 1st International Workshop on Classical Logic and Computation (CL&C 2006)　2006

On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus Peer-reviewed

Kentaro Kikuchi

Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2006)　LNAI 4246　120-134　2006

DOI： 10.1007/11916277_9 　

ISSN： 0302-9743

A Direct Proof of Strong Normalization for an Extended Herbelin's Calculus Peer-reviewed

Kentaro Kikuchi

Proceedings of the 7th International Symposium on Functional and Logic Programming (FLOPS 2004)　LNCS 2998　244-259　2004

DOI： 10.1007/978-3-540-24754-8_18 　

ISSN： 0302-9743

A Cut-Free Gentzen Formulation of Basic Propositional Calculus Peer-reviewed

Kentaro Kikuchi, Katsumi Sasaki

Journal of Logic, Language and Information　12　(2)　213-225　2003

DOI： 10.1023/A:1022363219134 　

Dual-Context Sequent Calculus and Strict Implication Peer-reviewed

Kentaro Kikuchi

Mathematical Logic Quarterly　48　(1)　87-92　2002

DOI： 10.1002/1521-3870(200201)48:1<87::AID-MALQ87>3.0.CO;2-N 　

ISSN： 0942-5616

Sequent Calculi for Visser's Propositional Logics Peer-reviewed

Katsumasa Ishii, Ryo Kashima, Kentaro Kikuchi

Notre Dame Journal of Formal Logic　42　(1)　1-22　2001

DOI： 10.1305/ndjfl/1054301352 　

ISSN： 1939-0726 0029-4527

Relationships between Basic Propositional Calculus and Substructural Logics Peer-reviewed

Kentaro Kikuchi

Bulletin of the Section of Logic　30　(1)　15-20　2001

Cut-Free Sequent Calculi for Visser's Propositional Logics

Kentaro Kikuchi

Research Report IS-RR-99-0030F, Japan Advanced Institute of Science and Technology　1999