terui kazushige 照井一成

… Alternative Names

照井一成テルイカズシゲ

TERUI Kazushige 照井一成

Less

Researcher Number	70353422
Other IDs
External Links
Affiliation (Current)	2025: 京都大学, 数理解析研究所, 准教授
Affiliation (based on the past Project Information) *help	2020 – 2023: 京都大学, 数理解析研究所, 准教授 2009 – 2018: Kyoto University, 数理解析研究所, 准教授 2006: 国立情報学研究所, 情報学プリンシプル研究系, 助教授 2003 – 2005: 国立情報学研究所, 助手 2002 – 2005: 国立情報学研究所, 情報学基礎研究系, 助手
Review Section/Research Field	Principal Investigator Fundamental theory of informatics / Basic Section 60010:Theory of informatics-related / Theory of informatics Except Principal Investigator Science and Engineering / Software / 計算機科学
Keywords	Principal Investigator 線形論理 / ラムダ計算 / 共通型 / エルブランの定理 / 部分構造論理 / 数理論理学 / 計算量 / 線型論理 / 自動定理生成 / 実線形算術 … More / 循環証明系 / 自動定理証明 / 正準拡大 / 稠密化 / 計算可能解析 / 整合空間 / 完備化 / 多相型ラムダ計算 / 素朴集合論 / Lukasiewicz論理 / 不動点定理 / 橋渡し定理 / 抽象代数論理 / 証明ネット / 二階述語論理 / Ω規則 / 順序代数の稠密化 / MacNeille完備化 / 代数的証明論 / フランス:オーストリア:アメリカ / フランス:オーストリア:アメリカ:チェコ / オランダ:オーストリア:アメリカ / 国際研究者交流 / 情報基礎 / 代数的完備化 / 再帰型 / ルディクス / プール回路 / カット除去定理 / シークエント計算 / 相意味論 / 型推論 / 関数型プログラミング … More Except Principal Investigator 宣言的プログラミング / ソフトウェア発展 / proof theory / real-time system / formal verification / formal specification / linear logic / logical method / 証明論 / 実時間システム / 形式検証 / 形式仕様 / 線形論理 / 論理的手法 / Permutative reductions / Strong normalization / Theory of programs / Type theory / Constructive logic / プログラム合成 / 実現可能性解釈 / 余帰納的定義 / 構成的集合 / 置換簡約 / 強正規化可能性 / プログラム理論 / 型理論 / 構成的論理 / 極小負集合 / 極大正集合 / 極小被覆集合 / 極大無矛盾集合 / 極小変更 / 関数型プログラミング / デフォルト論理 Less

Can Computer be a Mathematician? Automated Theorem Proving in Undergraduate MathematicsPrincipal Investigator
- Principal Investigator
  
  照井一成
- Project Period (FY)
  2020 – 2024
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Review Section
  
  Basic Section 60010:Theory of informatics-related
- Research Institution
  Kyoto University
Algebraic Proof Theory for Nonclassical Logics and Intersection Types for Lambda CalculusPrincipal Investigator
- Principal Investigator
  
  Terui Kazushige
- Project Period (FY)
  2013 – 2018
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Research Field
  
  Theory of informatics
- Research Institution
  Kyoto University
Algebraic and coalgebraic proof theoriesPrincipal Investigator
- Principal Investigator
  
  TERUI Kazushige
- Project Period (FY)
  2009 – 2012
- Research Category
  
  Grant-in-Aid for Young Scientists (B)
- Research Field
  
  Fundamental theory of informatics
- Research Institution
  Kyoto University
線形論理に基づく関数型プログラムの計算量の研究Principal Investigator
- Principal Investigator
  
  照井一成
- Project Period (FY)
  2004 – 2006
- Research Category
  
  Grant-in-Aid for Young Scientists (B)
- Research Field
  
  Fundamental theory of informatics
- Research Institution
  National Institute of Informatics
宣言的プログラミングにおけるソフトウェア発展の研究
- Principal Investigator
  
  佐藤健
- Project Period (FY)
  2003
- Research Category
  
  Grant-in-Aid for Scientific Research on Priority Areas
- Review Section
  
  Science and Engineering
- Research Institution
  National Institute of Informatics
New development in the matured linear logic research and its applications
- Principal Investigator
  
  OKADA Mituhiro
- Project Period (FY)
  2003 – 2005
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Research Field
  
  Software
- Research Institution
  Keio University
宣言的プログラミングにおけるソフトウェア発展の研究
- Principal Investigator
  
  佐藤健
- Project Period (FY)
  2002
- Research Category
  
  Grant-in-Aid for Scientific Research on Priority Areas
- Review Section
  
  Science and Engineering
- Research Institution
  National Institute of Informatics
Program synthesis using constructive sets and coinductive definitions
- Principal Investigator
  
  TATSUTA Makoto
- Project Period (FY)
  2000 – 2003
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Research Field
  
  計算機科学
- Research Institution
  National Institute of Informatics
  Kyoto University

[Book] コンピュータは数学者になれるのか？数学基礎論から証明とプログラムの理論へ2015
- Author(s)
  照井一成
- Total Pages
  357
- Publisher
  青土社
- Data Source
  KAKENHI-PROJECT-25330013
[Journal Article] MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics2018
- Author(s)
  Kazushige Terui
- Journal Title
  
  27th EACSL Annual Conference on Computer Science Logic (CSL 2018)
  
  Volume: 27 Pages: 1-19
- DOI
  10.4230/LIPICS.CSL.2018.37
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-25330013
[Journal Article] Algebraic proof theory: Hypersequents and hypercompletions2017
- Author(s)
  Agata Ciabattoni, Nikolaos Galatos and Kazushige Terui
- Journal Title
  
  Annals of Pure and Applied Logics
  
  Volume: 168(3) Issue: 3 Pages: 693-737
- DOI
  10.1016/j.apal.2016.10.012
- Peer Reviewed / Acknowledgement Compliant / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-25330013
[Journal Article] Densification of FL chains via residuated frames2016
- Author(s)
  Paolo Baldi and Kazushige Terui
- Journal Title
  
  Algebra Universalis
  
  Volume: 75(2) Issue: 2 Pages: 169-195
- DOI
  10.1007/s00012-016-0372-5
- Peer Reviewed / Acknowledgement Compliant / Open Access / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-25330013
[Journal Article] Strong Normalization for the Parameter-Free Polymorphic Lambda Calculus Based on the Omega-Rule2016
- Author(s)
  Ryota Akiyoshi and Kazushige Terui
- Journal Title
  
  Proceedings of FSCD'16
  
  Volume: --
- DOI
  10.4230/LIPIcs.FSCD.2016.5
- Peer Reviewed / Acknowledgement Compliant / Open Access
- Data Source
  KAKENHI-PROJECT-25330013, KAKENHI-PROJECT-16K16690
[Journal Article] Strong normalization for the parameter-free polymorphic lambda calculus based on the Omega-rule2016
- Author(s)
  Ryota Akiyoshi and Kazushige Terui
- Journal Title
  
  Proceedings of the 1st FSCD
  
  Volume: 1
- Peer Reviewed / Acknowledgement Compliant
- Data Source
  KAKENHI-PROJECT-25330013
[Journal Article] Parsimonious Types and Non-uniform Computation2015
- Author(s)
  Damiano Mazza and Kazushige Terui
- Journal Title
  
  Proceedings of the 42nd ICALP
  
  Volume: LNCS9135 Pages: 350-361
- DOI
  10.1007/978-3-662-47666-6_28
- ISBN
  9783662476659, 9783662476666
- Peer Reviewed / Acknowledgement Compliant / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-25330013
[Journal Article] Parsimonious Types and Non-uniform Computation2015
- Author(s)
  Damiano Mazza and Kazushige Terui
- Journal Title
  
  Proceedings of ICALP 2015
  
  Volume: 42
- Peer Reviewed / Acknowledgement Compliant
- Data Source
  KAKENHI-PROJECT-25330013
[Journal Article] Semantic evaluation, intersection types and complexity of simply typed lambda calculus2012
- Author(s)
  K. Terui
- Journal Title
  
  Proceedings of 23rd International Conference on Rewriting Techniques and Applications (RTA'12)
  
  Pages: 323-338
- DOI
  10.4230/LIPIcs.RTA.2012.323
- Data Source
  KAKENHI-PROJECT-21700014
[Journal Article] Algebraic proof theory for substrutural logics: cut-elimination and completions2012
- Author(s)
  A. Ciabattoni, N. Galatos and K. Terui
- Journal Title
  
  Annals of Pure and Applied Logic
  
  Volume: 163(3) Issue: 3 Pages: 266-290
- DOI
  10.1016/j.apal.2011.09.003
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-21700014
[Journal Article] Semantic evaluation, intersection types and complexity of simply typed lambda calculus2012
- Author(s)
  K.Terui
- Journal Title
  
  Proceedings of the 23^<rd> International Conference on Rewriting Techniques and Applications
  
  Volume: (掲載確定)
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-21700014
[Journal Article] Computational ludics2011
- Author(s)
  K. Terui
- Journal Title
  
  Theoretical Computer Science
  
  Volume: 412(20) Issue: 20 Pages: 2048-2071
- DOI
  10.1016/j.tcs.2010.12.026
- Data Source
  KAKENHI-PROJECT-21700014
[Journal Article] MacNeille completions of FL algebras2011
- Author(s)
  A.Ciabattoni, N.Galatos, K.Terui
- Journal Title
  
  Algebra Universalis
  
  Volume: (掲載確定)
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-21700014
[Journal Article] Disjunction property and complexity of substructural logics2011
- Author(s)
  R. Horcik and K. Terui
- Journal Title
  
  Theoretical Computer Science
  
  Volume: 412(31) Issue: 31 Pages: 3992-4006
- DOI
  10.1016/j.tcs.2011.04.004
- Data Source
  KAKENHI-PROJECT-21700014
[Journal Article] MacNeille completions of FL-algebras2011
- Author(s)
  A.Ciabattoni, N.Galatos, K.Terui
- Journal Title
  
  Algebra Universalis
  
  Volume: 66(4) Issue: 4 Pages: 405-420
- DOI
  10.1007/s00012-011-0160-1
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-21700014
[Journal Article] Infitarycompleteness in ludics2010
- Author(s)
  M. Basaldella and K. Terui
- Journal Title
  
  Proceedings of Logic in Computer Science (LICS'10)
  
  Pages: 294-303
- DOI
  10.1109/lics.2010.47
- Data Source
  KAKENHI-PROJECT-21700014
[Journal Article] From focalization of logic to the logic of focalization2010
- Author(s)
  M.Basaldella, A.Saurin, K.Terui
- Journal Title
  
  Electronic Notes in Theoretical Computer Science
  
  Volume: 265 Pages: 161-176
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-21700014
[Journal Article] On the meaning of logical completeness2010
- Author(s)
  M.Basaldella, K.Terui
- Journal Title
  
  Logical Methods in Computer Science
  
  Volume: 6(4) Pages: 1-35
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-21700014
[Journal Article] On the meaning of logical completeness2010
- Author(s)
  M. Basaldella and K. Terui
- Journal Title
  
  Logical Methods in Computer Science
  
  Volume: 6(4:11) Pages: 1-35
- DOI
  10.2168/lmcs-6(4:11)2010
- Data Source
  KAKENHI-PROJECT-21700014
[Journal Article] Infinitary completeness in ludics2010
- Author(s)
  M.Basaldella, K.Terui
- Journal Title
  
  Proceedings of the 25^<th> Annual IEEE Symposium on Logic in Computer Science (LICS) 25(掲載確定)
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-21700014
[Journal Article] Church=>Scott = Ptime: an application of resource sensitive realizability2010
- Author(s)
  A. Brunel and K. Terui
- Journal Title
  
  Proceedings of Developments in Implicit Computational Complexity (DICE'10)
  
  Volume: 23 Pages: 31-46
- DOI
  10.4204/eptcs.23.3
- Data Source
  KAKENHI-PROJECT-21700014
[Journal Article] Expanding the realm ofsystematic proof theory.2009
- Author(s)
  A. Ciabattoni, L. Strassburger and K. Terui
- Journal Title
  
  Proceedings of Computer Science Logic (CSL'09)
  
  Pages: 163-178
- DOI
  10.1007/978-3-642-04027-6_14
- ISBN
  9783642040269, 9783642040276
- Data Source
  KAKENHI-PROJECT-21700014
[Journal Article] On the meaning of logical completeness2009
- Author(s)
  M. Basaldella and K. Terui
- Journal Title
  
  Proceedings of Typed Lambda Calculus and its Applications (TLCA'09)
  
  Pages: 50-64
- DOI
  10.1007/978-3-642-02273-9_6
- ISBN
  9783642022722, 9783642022739
- Data Source
  KAKENHI-PROJECT-21700014
[Journal Article] Expanding the realm of systematic proof theory2009
- Author(s)
  A.Ciabattoni, L.Strassburger, K.Terui
- Journal Title
  
  Proceedings of the 18^<th> EACSL Conference on Computer Science Logic (CSL) 18
  
  Pages: 163-178
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-21700014
[Journal Article] On the meaning of logical completeness2009
- Author(s)
  M.Basaldella, K.Terui
- Journal Title
  
  Proceedings of the 9^<th> International Conference on Typed Lambda Calculi and Applications (TLCA) 9
  
  Pages: 50-64
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-21700014
[Journal Article] Which Structural Rules Admit Cut Elimination? An Algebraic Criterion.2007
- Author(s)
  K.Terui
- Journal Title
  
  Journal of Symbolic Logic (受理済み)(未定)
- Data Source
  KAKENHI-PROJECT-16700020
[Journal Article] Verification of Ptime reducibility for System F terms : Type inference in Dual Light Affine Logic.2007
- Author(s)
  V.Atassi, P.Baillot, K.Terui
- Journal Title
  
  Logical Methods in Computer science (受理済み)(未定)
- Data Source
  KAKENHI-PROJECT-16700020
[Journal Article] Towards a semantic characterization of cut-elimination2006
- Author(s)
  A.Ciabattoni, K.Terui
- Journal Title
  
  Studia Logica Vol.82
  
  Pages: 95-119
- Data Source
  KAKENHI-PROJECT-16700020
[Journal Article] Verification of Ptime reducibility for System F terms via Dual Light Affine Logic.2006
- Author(s)
  V.Atassi, P.Baillot, K.Terui
- Journal Title
  
  Proceedings of Computer Science Logic 2006 (CSL'06) LNCS 4207
  
  Pages: 150-166
- Data Source
  KAKENHI-PROJECT-16700020
[Journal Article] Towards a semantic characterization of cut-elimination2006
- Author(s)
  A.Ciabattoni, K.Terui
- Journal Title
  
  Studia Logica Vol.82
  
  Pages: 95-119
- Data Source
  KAKENHI-PROJECT-15300008
[Journal Article] Intuitionistic phase semantics is almost classical2006
- Author(s)
  M.Kanovich, M.Okada, K.Terui
- Journal Title
  
  Mathematical Structures in Computer Science Vol.16
  
  Pages: 1-20
- Data Source
  KAKENHI-PROJECT-16700020
[Journal Article] Intuitionistic phase semantics is almost classical2006
- Author(s)
  M.Kanovich, M.Okada, K.Terui
- Journal Title
  
  Mathematical Structure in Computer Science (to appear)
- Description
  「研究成果報告書概要(欧文)」より
- Data Source
  KAKENHI-PROJECT-15300008
[Journal Article] Modular Cut-Elimination : Finding Proofs or Counterexamples.2006
- Author(s)
  A.Ciabattoni, K.Terui
- Journal Title
  
  Proceedings of Logic for Programming and Automated Reasoning 2006 (LPAR'06) LNAI 4246
  
  Pages: 135-149
- Data Source
  KAKENHI-PROJECT-16700020
[Journal Article] Intuitionistic phase semantics is almost classical2006
- Author(s)
  M.Kanovich, M.Okada, K.Terui
- Journal Title
  
  Mathematical Structure in Computer Science 近刊
- Data Source
  KAKENHI-PROJECT-15300008
[Journal Article] A feasible algorithm for typing in Elementary Affine Logic2005
- Author(s)
  P.Baillot, K.Terui
- Journal Title
  
  Proceedings of TLCA 2005 (発表予定)
- Data Source
  KAKENHI-PROJECT-16700020
[Journal Article] Light types for polynomial time computation in lambda-calculus2004
- Author(s)
  P.Baillot, K.Terui
- Journal Title
  
  Proceedings of LICS 2004 19
  
  Pages: 266-275
- Data Source
  KAKENHI-PROJECT-16700020
[Journal Article] Proof Nets and Boolean Circuits2004
- Author(s)
  K.Terui
- Journal Title
  
  Proceedings of LICS 2004 19
  
  Pages: 182-191
- Data Source
  KAKENHI-PROJECT-16700020
[Journal Article] Proof Nets and Boolean Circuits2004
- Author(s)
  Kazushige Terui
- Journal Title
  
  Proceedings of Logic in Computer Science 2004, IEEE 19
  
  Pages: 182-191
- Data Source
  KAKENHI-PROJECT-15300008
[Journal Article] Intuitionistic phase semantics 15 almost classical
- Author(s)
  M.Kanovich, M.Okada, K.Terui
- Journal Title
  
  Mathematical Structure in Computer Science (to appear in 2006)
- Description
  「研究成果報告書概要(和文)」より
- Data Source
  KAKENHI-PROJECT-15300008
[Presentation] Bot in nonclassical logics2018
- Author(s)
  照井一成
- Organizer
  第５３回MLG数理論理学研究集会
- Data Source
  KAKENHI-PROJECT-25330013
[Presentation] Bot in nonclassical logics and proof theory2018
- Author(s)
  Kazushige Terui
- Organizer
  Logic, Language, and Ontology: A workshop in honor of the 70th birthday of Toshiharu Waragai
- Data Source
  KAKENHI-PROJECT-25330013
[Presentation] MacNeille completion and Buchholz' Omega rule2018
- Author(s)
  Kazushige Terui
- Organizer
  Second workshop on mathematical logic and its applications
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-25330013
[Presentation] MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics2018
- Author(s)
  Kazushige Terui
- Organizer
  27th EACSL Annual Conference on Computer Science Logic (CSL 2018)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-25330013
[Presentation] How useful is proof theory for substructural logics?2016
- Author(s)
  Kazushige Terui
- Organizer
  SYSMICS: Syntax meets Semantics
- Place of Presentation
  バルセロナ（スペイン）
- Year and Date
  2016-09-07
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-25330013
[Presentation] Intersection types for real number computation2016
- Author(s)
  Kazushige Terui
- Organizer
  8th Workshop on Intersection Types and Related Systems
- Place of Presentation
  ポルト（ポルトガル）
- Year and Date
  2016-06-26
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-25330013
[Presentation] Substructural logics with fixpoints2016
- Author(s)
  Kazushige Terui
- Organizer
  7th ALCOP: Algebra and Coalgebra meet Proof Theory
- Place of Presentation
  ウィーン（オーストリア）
- Year and Date
  2016-04-09
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-25330013
[Presentation] On predicative fragments of System F2016
- Author(s)
  Kazushige Terui
- Organizer
  Workshop: Linear logic, mathematics and computer science
- Place of Presentation
  リヨン（フランス）
- Year and Date
  2016-11-10
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-25330013
[Presentation] Coherence spaces for computable analysis2015
- Author(s)
  Kei Matsumoto and Kazushige Terui
- Organizer
  20th International Conference on Computability and Complexity in Analysis
- Place of Presentation
  明治大学
- Year and Date
  2015-07-13
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-25330013
[Presentation] Coherence spaces for computable analysis II2015
- Author(s)
  Kei Matsumoto and Kazushige Terui
- Organizer
  Continuity, Computability, Constructivity - From Logic to Algorithms
- Place of Presentation
  Schloss Aspenstein
- Year and Date
  2015-09-14
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-25330013
[Presentation] Proof nets, boolean circuits and parsimonious modality2015
- Author(s)
  Kazushige Terui
- Organizer
  International Workshop “Logic, Philosophy and Computation of Proofs”
- Place of Presentation
  慶応大学
- Year and Date
  2015-11-28
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-25330013
[Presentation] Substructural logics and fixed points2015
- Author(s)
  Kazushige Terui
- Organizer
  Kyoto Nonclassical Logic Workshop
- Place of Presentation
  京都大学
- Year and Date
  2015-11-19
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-25330013
[Presentation] Proof theory for ordered algebra: amalgamation and densification2014
- Author(s)
  Kazushige Terui
- Organizer
  Structures and Deduction (Vienna Summer of Logic)
- Place of Presentation
  Vienna
- Year and Date
  2014-07-12
- Invited
- Data Source
  KAKENHI-PROJECT-25330013
[Presentation] Intersection Types for Normalization and Verification2014
- Author(s)
  Kazushige Terui
- Organizer
  21st Workshop on Logic, Language, Information and Computation
- Place of Presentation
  Valparaiso (Chile)
- Year and Date
  2014-09-02
- Invited
- Data Source
  KAKENHI-PROJECT-25330013
[Presentation] Some topics on hypersequents2014
- Author(s)
  Kazushige Terui
- Organizer
  Chocola Meeting
- Place of Presentation
  Marseille
- Year and Date
  2014-12-04
- Invited
- Data Source
  KAKENHI-PROJECT-25330013
[Presentation] Models of linear logic for higher order real computation2014
- Author(s)
  Kazushige Terui
- Organizer
  Workshop on Higher Order Computation: Types, Complexity, Applications
- Place of Presentation
  Institut Henri Poincare, Paris
- Year and Date
  2014-06-17
- Data Source
  KAKENHI-PROJECT-25330013
[Presentation] On applications of models of linear logic2014
- Author(s)
  Kazushige Terui
- Organizer
  Thematic trimester: Semantics of Proofs and Certified Mathematics
- Place of Presentation
  Institut Henri Poincare, Paris
- Year and Date
  2014-06-26
- Invited
- Data Source
  KAKENHI-PROJECT-25330013
[Presentation] Ludics and interactive completeness2014
- Author(s)
  Kazushige Terui
- Organizer
  Logic and Games (Vienna Summer of Logic)
- Place of Presentation
  Vienna
- Year and Date
  2014-07-15
- Invited
- Data Source
  KAKENHI-PROJECT-25330013
[Presentation] Semantic evaluation, intersection types and complexity of simply typed lambda calculus II2013
- Author(s)
  Kazushige Terui
- Organizer
  4th International Workshop on Developments in Implicit Computational Complexity
- Place of Presentation
  ローマ大学（イタリア）
- Data Source
  KAKENHI-PROJECT-21700014
[Presentation] Semantic evaluation, intersection types and complexity of simply typed lambda calculus2013
- Author(s)
  Kazushige Terui
- Organizer
  3rd Workshop on Proof Theory and Rewriting
- Place of Presentation
  石川県立美術館（石川）
- Data Source
  KAKENHI-PROJECT-21700014
[Presentation] Substructural Logics2013
- Author(s)
  Kazushige Terui
- Organizer
  9th International Tbilisi Summer School in Logic and Language
- Place of Presentation
  Tbilisi State University (Georgia)
- Invited
- Data Source
  KAKENHI-PROJECT-25330013
[Presentation] Semantic evaluation, intersection types and complexity of simply typed lambda calculus2012
- Author(s)
  Kazushige Terui
- Organizer
  23rd International Conference on Rewriting Techniques and Applications
- Place of Presentation
  名古屋大学（愛知）
- Data Source
  KAKENHI-PROJECT-21700014
[Presentation] Herbrand's theorem via hypercanonical extensions2012
- Author(s)
  照井一成
- Organizer
  第４７回MLG数理論理学研究集会
- Place of Presentation
  KKR湯沢ゆきぐに（新潟）
- Data Source
  KAKENHI-PROJECT-21700014
[Presentation] Tutorial on algebraic approaches to substructural logics2011
- Author(s)
  K.Terui
- Organizer
  RIMS研究集会:Algebraic and Coalgebraic Approaches to Non-Classical Logics
- Place of Presentation
  京都大学(京都府)
- Year and Date
  2011-05-16
- Data Source
  KAKENHI-PROJECT-21700014
[Presentation] 線形論理とラムダ計算の計算量.2011
- Author(s)
  照井一成
- Organizer
  第13回プログラミングおよびプログラミング言語ワークショップ(PPL'11)
- Place of Presentation
  札幌
- Year and Date
  2011-03-10
- Data Source
  KAKENHI-PROJECT-21700014
[Presentation] MacNeille-type completions for residuated lattices and sequent-type proof systems for substructural logics2011
- Author(s)
  K.Terui
- Organizer
  Second International Conference on Order, Algebra, and Logics
- Place of Presentation
  Jagiellonian Universityクラクフ(ポーランド)(招待講演)
- Year and Date
  2011-06-08
- Data Source
  KAKENHI-PROJECT-21700014
[Presentation] MacNeille-type completions for residuated lattices and sequent-type proof systems for substructural logics2011
- Author(s)
  K. Terui
- Organizer
  2nd International Conference on Order
- Place of Presentation
  Algebra and Logics, Krakow (Poland)
- Year and Date
  2011-06-08
- Data Source
  KAKENHI-PROJECT-21700014
[Presentation] コントラクションと連続性2011
- Author(s)
  照井一成
- Organizer
  第45回MLG数理論理学研究集会
- Place of Presentation
  KKR湯沢ゆきぐに
- Year and Date
  2011-01-07
- Data Source
  KAKENHI-PROJECT-21700014
[Presentation] 線型論理とラムダ計算の計算量2011
- Author(s)
  照井一成
- Organizer
  第13回プログラミングおよびプログラミング言語ワークショップ
- Place of Presentation
  定山渓ビューホテル(招待講演)
- Year and Date
  2011-03-10
- Data Source
  KAKENHI-PROJECT-21700014
[Presentation] Proof theory and algebra in substructural logics2011
- Author(s)
  K. Terui
- Organizer
  20th International Conference on Automated Reasoning with Analytic Tableaux andRelated Methods (TABLEAUX'11)
- Place of Presentation
  Bern(Switzerland)
- Year and Date
  2011-07-07
- Data Source
  KAKENHI-PROJECT-21700014
[Presentation] Church=>Scott=Ptime : an application of resource sensitive realizability2011
- Author(s)
  K.Terui
- Organizer
  Workshop on Logic and Computation
- Place of Presentation
  金沢能楽美術館
- Year and Date
  2011-02-08
- Data Source
  KAKENHI-PROJECT-21700014
[Presentation] An algebraic approach to proof theory for substructural logics2011
- Author(s)
  K.Terui
- Organizer
  Workshop STRUCTURAL
- Place of Presentation
  PPSパリ(フランス)
- Year and Date
  2011-06-16
- Data Source
  KAKENHI-PROJECT-21700014
[Presentation] The birth of linear logic2010
- Author(s)
  K.Terui
- Organizer
  Algebra and Substructural logics : take 4
- Place of Presentation
  北陸先端技術大学院大学
- Year and Date
  2010-06-10
- Data Source
  KAKENHI-PROJECT-21700014
[Presentation] Ludics and interactive completeness (Invited talk)2010
- Author(s)
  K.Terui
- Organizer
  Games for logic and programming languages V
- Place of Presentation
  Paphos (Cyprus)
- Year and Date
  2010-03-21
- Data Source
  KAKENHI-PROJECT-21700014
[Presentation] Algebraic proof theory for substructural logics II (Invited talk)2009
- Author(s)
  K.Terui
- Organizer
  Topology, Algebra and Categories in Logic
- Place of Presentation
  University of Amsterdamオランダ
- Year and Date
  2009-07-08
- Data Source
  KAKENHI-PROJECT-21700014
[Presentation] Algebraic proof theory for nonclassical logics II2009
- Author(s)
  K. Terui
- Organizer
  Topology,Algebra and Categories in Logic (TACL'09)
- Place of Presentation
  Amsterdam (Netherlands)
- Year and Date
  2009-07-08
- Data Source
  KAKENHI-PROJECT-21700014
[Presentation] Semantic methods in substructural and fuzzy logics2009
- Author(s)
  K. Terui.
- Organizer
  Conferene on Non-Classical Mathematics
- Place of Presentation
  Hejnice (Czech)
- Year and Date
  2009-06-20
- Data Source
  KAKENHI-PROJECT-21700014
[Presentation] Semantic methods in substructural and fuzzy logics (Invited talk)2009
- Author(s)
  K.Terui
- Organizer
  1^<st> Conference on Non-classical Mathematics
- Place of Presentation
  Hejnice (Czech Republic)
- Data Source
  KAKENHI-PROJECT-21700014
[Presentation] Completions of P3' varieties of residuated lattices2009
- Author(s)
  K.Terui
- Organizer
  第43回MLG数理論理学研究集会
- Place of Presentation
  九州産業大学
- Year and Date
  2009-12-13
- Data Source
  KAKENHI-PROJECT-21700014
[Presentation] Herbrand's Theorem via Hypercanonical Extensions
- Author(s)
  Kazushige Terui
- Organizer
  10th International Tbilisi Symposium on Language, Logic and Computation (Workshop on Algebraic Proof Theory)
- Place of Presentation
  Gudauri (Georgia)
- Invited
- Data Source
  KAKENHI-PROJECT-25330013
[Presentation] Some topics on linear logic, processes and hypersequents
- Author(s)
  Kazushige Terui
- Organizer
  Workshop on Proofs as Processes
- Place of Presentation
  石川四高記念文化交流館（石川）
- Data Source
  KAKENHI-PROJECT-25330013
[Presentation] Intersection types for normalization and verification
- Author(s)
  Kazushige Terui
- Organizer
  IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
- Place of Presentation
  IIT Guwahati (India)
- Invited
- Data Source
  KAKENHI-PROJECT-25330013

1. TATSUTA Makoto (80216994)

# of Collaborated Projects: 2 results

# of Collaborated Products: 0 results
2. 佐藤健 (00271635)

# of Collaborated Projects: 2 results

# of Collaborated Products: 0 results
3. 新井紀子 (40264931)

# of Collaborated Projects: 2 results

# of Collaborated Products: 0 results
4. OKADA Mituhiro (30224025)

# of Collaborated Projects: 1 results

# of Collaborated Products: 3 results
5. KOBAYASHI Naoki (00262155)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
6. TAMURA Naoyuki (60207248)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results

terui kazushige 照井 一成

照井 一成 テルイ カズシゲ

TERUI Kazushige 照井 一成

Research Projects

Research Products

Co-Researchers

Can Computer be a Mathematician? Automated Theorem Proving in Undergraduate MathematicsPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Algebraic Proof Theory for Nonclassical Logics and Intersection Types for Lambda CalculusPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Algebraic and coalgebraic proof theoriesPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

線形論理に基づく関数型プログラムの計算量の研究Principal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

宣言的プログラミングにおけるソフトウェア発展の研究

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

New development in the matured linear logic research and its applications

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

宣言的プログラミングにおけるソフトウェア発展の研究

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Program synthesis using constructive sets and coinductive definitions

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

[Book] コンピュータは数学者になれるのか？ 数学基礎論から証明とプログラムの理論へ2015

Author(s)

Total Pages

Publisher

Data Source

[Journal Article] MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics2018

Author(s)

Journal Title

DOI

Data Source

[Journal Article] Algebraic proof theory: Hypersequents and hypercompletions2017

Author(s)

Journal Title

DOI

Data Source

[Journal Article] Densification of FL chains via residuated frames2016

Author(s)

Journal Title

DOI

Data Source

[Journal Article] Strong Normalization for the Parameter-Free Polymorphic Lambda Calculus Based on the Omega-Rule2016

Author(s)

Journal Title

DOI

Data Source

[Journal Article] Strong normalization for the parameter-free polymorphic lambda calculus based on the Omega-rule2016

terui kazushige 照井一成

照井一成テルイカズシゲ

TERUI Kazushige 照井一成

[Book] コンピュータは数学者になれるのか？数学基礎論から証明とプログラムの理論へ2015