Updated on 2025/07/06

写真a

 
UEDA, Kazunori
 
Affiliation
Faculty of Science and Engineering, School of Fundamental Science and Engineering
Job title
Professor
Degree
工学博士 ( 1986 東京大学 )
Doctor of Engineering
Homepage URL
http://www.ueda.info.waseda.ac.jp/~ueda/index-j.html

Research Experience

  • 2010
    -
    Now

    エジプト日本科学技術大学客員教授

  • 2007
    -
    Now

    Waseda University   Faculty of Science and Engineering

  • 2006
    -
    2016

    National Institute of Informatics

  • 2011
    -
    2012

    東京大学理学部 非常勤講師

  • 2003
    -
    2007

    Waseda University   School of Science and Engineering

  • 1997
    -
    2003

    Waseda University   School of Science and Engineering

  • 2000
    -
    2001

    シンガポール国立大学計算機科学科 客員研究員

  • 1994
    -
    2000

    The University of Tokyo   Faculty of Science

  • 1993
    -
    1997

    Waseda University   School of Science and Engineering

  • 1994
    -
    1995

    Ibaraki University

  • 1983
    -
    1993

    NEC Corporation

  • 1985
    -
    1992

    日本電気株式会社より財団法人新世代コンピュータ技術開発機構に出向

▼display all

Education Background

  • 　
    -
    1983

    University of Tokyo   Graduate School, Division of Engineering  

  • 　
    -
    1978

    University of Tokyo   Faculty of Engineering  

Committee Memberships

  • 2013.04
    -
    2017.12

    New Generation Computing (Ohmsha and Springer)  Associate Editor-In-Chief

  • 2011
    -
    2014

    Asian Association for Foundations of Software (AAFS)  Co-Chair

  • 2001.11
    -
    2013.03

    New Generation Computing (Ohmsha and Springer)  Area Editor (Programming and Architecture分野)

  • 2010
    -
    　

    Eighth Asian Symposium on Programming Languages and Systems (APLAS 2010, Shanghai, China, November-December 2010)  プログラム委員長

  • 2004.04
    -
    2008.03

    コンピュータソフトウェア（日本ソフトウェア科学会機関誌）  編集委員長

  • 2001.01
    -
    2004.12

    Theory and Practice of Logic Programming (Cambridge University Press)  Area Editor (Design and Analysis of Languages and Systems分野)

  • 2000.04
    -
    2002.03

    人工知能学会  理事

  • 2001
    -
    　

    Fifth International Symposium on Functional and Logic Programming (FLOPS 2001, Tokyo, March 7-9, 2001)  プログラム委員長 (Herbert Kuchen 氏と共同)

  • 1998.04
    -
    2000.03

    情報処理学会論文誌：プログラミング  編集委員長

  • 1992.10
    -
    1999.11

    Journal of Logic Programming (North-Holland)  Area Editor (Design and Analysis of Languages and Systems分野)

  • 1997
    -
    　

    並列処理シンポジウム'97 (神戸)  プログラム委員長

  • 1997
    -
    　

    Asian Computing Science Conference (ASIAN'97、Kathmandu, Nepal, December 9-12, 1997)  プログラム委員長 （R.K. Shyamasunder氏と共同）

  • 1991
    -
    　

    International Logic Programming Symposium (ILPS'91, San Diego, U.S.A.)  プログラム委員長 (Vijay Saraswat 氏と共同)

  • 2001.04
    -
    2007.03

    日本ソフトウェア科学会  理事

  • 1998.04
    -
    2000.03

    情報処理学会  プログラミング研究会 主査

▼display all

Professional Memberships

  • 　
    　
    　

    IEEE Computer Society

  • 　
    　
    　

    Association for Computing Machinary

  • 　
    　
    　

    人工知能学会

  • 　
    　
    　

    情報処理学会

  • 　
    　
    　

    日本ソフトウェア科学会

Research Areas

  • Theory of informatics / Software

Research Interests

  • logic and constraint programming

  • Hybrid Systems

  • Concurrency and Parallelism

  • Design and Implementation of Programming Languages

Awards

  • フェロー

    2016   日本ソフトウェア科学会  

  • フェロー

    2015   情報処理学会  

  • 基礎研究賞

    2011   日本ソフトウェア科学会  

  • 日本ソフトウェア科学会第５回論文賞

    2001  

  • 日本ソフトウェア科学会第４回論文賞

    2000  

  • 第７回日本IBM科学賞

    1993  

  • 第３回元岡賞

    1988  

  • 功労賞

    2010   日本ソフトウェア科学会  

  • 人工知能学会2002年度全国大会ベストプレゼンテーション賞

    2003  

  • 日本ソフトウェア科学会第１９回高橋奨励賞

    2002  

  • 情報処理学会第３０回全国大会学術奨励賞

    1985  

  • 日本ソフトウェア科学会第２回高橋奨励賞

    1985  

▼display all

 

Papers

  • Constraint-Based Modeling and Symbolic Simulation of Hybrid Systems with HydLa and HyLaGI.

    Yunosuke Yamada, Masashi Sato, Kazunori Ueda

    Cyber Physical Systems. Model-Based Design. CyPhy 2019, WESE 2019. Lecture Notes in Computer Science   11971   153 - 178  2020.02  [Refereed]

    DOI

    Scopus

  • Smart SE: Smart Systems and Services Innovative Professional Education Program

    Hironori Washizaki, Kenji Tei, Kazunori Ueda, Hayato Yamana, Yoshiaki Fukazawa, Shinichi Honiden, Shoichi Okazaki, Nobukazu Yoshioka, Naoshi Uchihira

    44th IEEE Annual Computers, Software, and Applications Conference(COMPSAC)     1113 - 1114  2020  [Refereed]

    DOI

    Scopus

    2
    Citation
    (Scopus)

  • Declarative Semantics of the Hybrid Constraint Language HydLa.

    Kazunori Ueda, Hiroshi Hosobe, Daisuke Ishii

    CoRR   abs/1910.12272  2019  [Refereed]

  • Introducing Symmetry to Graph Rewriting Systems with Process Abstraction

    Taichi Tomioka, Yutaro Tsunekawa, Kazunori Ueda

    Graph Transformation. ICGT 2019. Lecture Notes in Computer Science   11629   3 - 20  2019  [Refereed]

    DOI

    Scopus

  • Generation of Efficient Obfuscated Code through Just-in-Time Compilation.

    Muhammad Hataba, Ahmed El-Mahdy, Kazunori Ueda

    IEICE Trans. Inf. Syst.   102-D ( 3 ) 645 - 649  2019  [Refereed]

  • Logic/Constraint Programming and Concurrency: The hard-won lessons of the Fifth Generation Computer project.

    Kazunori Ueda

    Sci. Comput. Program.   164   3 - 17  2018  [Refereed]

    Authorship：Lead author

    DOI

    Scopus

    5
    Citation
    (Scopus)

  • Implementation of LMNtal Model Checkers: a Metaprogramming Approach.

    Yutaro Tsunekawa, Taichi Tomioka, Kazunori Ueda

    J. Object Technol.   17 ( 1 ) 1 - 28  2018  [Refereed]

    DOI

    Scopus

    2
    Citation
    (Scopus)

  • Name Binding is Easy with Hypergraphs.

    Alimujiang Yasen, Kazunori Ueda

    IEICE Trans. Inf. Syst.   101-D ( 4 ) 1126 - 1140  2018  [Refereed]

    DOI

    Scopus

    1
    Citation
    (Scopus)

  • Symbolic Analysis of Hybrid Systems Involving Numerous Discrete Changes Using Loop Detection.

    Kenichi Betsuno, Shota Matsumoto, Kazunori Ueda

    Cyber Physical Systems. Design, Modeling, and Evaluation. CyPhy 2016. Lecture Notes in Computer Science   10107   17 - 30  2017.01  [Refereed]

    DOI

    Scopus

    2
    Citation
    (Scopus)

  • Unification of Hypergraph \lambda -Terms.

    Alimujiang Yasen, Kazunori Ueda

    Topics in Theoretical Computer Science. TTCS 2017. Lecture Notes in Computer Science   10608   106 - 124  2017  [Refereed]

    DOI

    Scopus

    1
    Citation
    (Scopus)

  • MEC: Network Optimized Multi-stage Erasure Coding for Scalable Storage Systems.

    Hiroaki Akutsu, Takahiro Yamamoto, Kazunori Ueda, Hideo Saito

    2017 IEEE 22nd Pacific Rim International Symposium on Dependable Computing (PRDC)     292 - 300  2017  [Refereed]

    DOI

    Scopus

    1
    Citation
    (Scopus)

  • Symbolic Simulation of Parametrized Hybrid Systems with Affine Arithmetic

    Shota Matsumoto, Kazunori Ueda

    2016 23rd International Symposium on Temporal Representation and Reasoning (TIME)     4 - 11  2016.10  [Refereed]

    DOI

  • Implementation of LMNtal Model Checkers: a Metaprogramming Approach.

    Yutaro Tsunekawa, Taichi Tomioka, Kazunori Ueda

    First Workshop on Meta-Programming Techniques and Reflection (META'16), Amsterdam    2016.10  [Refereed]

  • Optimized Canonical Labeling Algorithm for Graph Rewriting Systems

    MIYAHARA Kazuhiro, UEDA Kazunori

    Computer Software   33 ( 1 ) 1_126 - 1_149  2016

    　View Summary

    In graph-based model checking, systems are modeled with graph structures which are highly expressive and feature a symmetry reduction mechanism. However, it involves frequent isomorphism checking of graphs generated in the course of model checking. Canonical labeling of graphs, which gives a unique representation to isomorphic graphs, is expected to be an effective method to check isomorphism among many graphs efficiently. It is therefore important to efficiently compute canonical forms of graphs in graph rewriting systems. For this purpose, we propose an optimization technique for McKay's canonical labeling algorithm that reuses information of graph structures that does not change by rewriting. To enable reuse, we reformulated McKay's algorithm to clarify what substructures of graphs are utilized in its execution, and designed an algorithm for successive graph canonicalization that organizes graph information in such a way that recomputation may be minimized. We evaluated the performance of the proposed algorithm, and found that it achieved sublinear time complexity with respect to the number of vertices for many cases of re-canonicalization.

    DOI CiNii

  • グラフ書換え系のための効率的なグラフ正規化手法

    宮原 和大, 上田 和紀

    コンピュータソフトウェア   33 ( 1 ) 126 - 149  2016.01  [Refereed]

  • Logic/Constraint Programming and Concurrency: The Hard-Won Lessons of the Fifth Generation Computer Project

    Kazunori Ueda

    Proc. 13th International Symposium on Functional and Logic Programming (FLOPS 2016)     1 - 11  2016

    DOI

    Scopus

    1
    Citation
    (Scopus)

  • Reliability and Failure Impact Analysis of Distributed Storage Systems with Dynamic Refuging

    Hiroaki AKUTSU, Kazunori UEDA, Takeru CHIBA, Tomohiro KAWAGUCHI, Norio SHIMOZONO

    IEICE Transactions on Information and Systems   E99.D ( 9 ) 2259 - 2268  2016  [Refereed]

    DOI

  • HyLaGI: Symbolic Implementation of a Hybrid Constraint Language HydLa

    Shota Matsumoto, Fumihiko Kono, Teruya Kobayashi, Kazunori Ueda

    Electronic Notes in Theoretical Computer Science   317   109 - 115  2015.11  [Refereed]

    DOI

    Scopus

    3
    Citation
    (Scopus)

  • Reliability Analysis of Highly Redundant Distributed Storage Systems with Dynamic Refuging

    Hiroaki Akutsu, Kazunori Ueda, Takeru Chiba, Tomohiro Kawaguchi, Norio Shimozono

    2015 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing     261 - 268  2015.03  [Refereed]

    DOI

  • Validated Interval Computation of Reachable Sets of Nonlinear Hybrid Systems

    ISHII Daisuke, UEDA Kazunori

    Journal of The Society of Instrument and Control Engineers   53 ( 12 ) 1086 - 1092  2014.12  [Refereed]

    DOI CiNii

  • Towards a Substrate Framework of Computation

    Kazunori Ueda

    Concurrent Objects and Beyond, Lecture Notes in Computer Science   8665   341 - 366  2014  [Refereed]  [Invited]

    Authorship：Lead author

    DOI

    Scopus

    3
    Citation
    (Scopus)

  • Reduction of the Number of States and the Acceleration of LMNtal Parallel Model Checking

    Ryo YASUDA, Taketo YOSHIDA, Kazunori UEDA

    Transactions of the Japanese Society for Artificial Intelligence   29 ( 1 ) 182 - 187  2014.01  [Refereed]

    　View Summary

    SLIM is an LMNtal runtime. LMNtal is a programming and modeling language based on hierarchical graph rewriting. SLIM features automata-based LTL model checking that is one of the methods to solve accepting cycle search problems. Parallel search algorithms OWCTY and MAP used by SLIM generate a large number of states for problems having and accepting cycles. Moreover, they have a problem that performance seriously falls for particular problems. We propose a new algorithm that combines MAP and Nested DFS to remove states for problems including accepting cycles. We experimented the algorithm and confirmed improvements both in performance and scalability.

    DOI CiNii

    Scopus

  • ハイブリッド制約言語HydLaの記号実行シミュレータHyrose 松本 翔太, 上田 和紀

    松本 翔太, 上田 和紀

    コンピュータソフトウェア   30 ( 4 ) 18 - 35  2013.11  [Refereed]

  • ハイブリッド制約言語プログラムのハイブリッドオートマトンへの変換アルゴリズム

    竹口輝, 和田亮, 松本翔太, 細部博史, 上田和紀

    日本ソフトウェア科学会第29回大会論文集   ( 2A-3 ) 1 - 10  2012.08

  • HydLa: A High-Level Language for Hybrid Systems (short paper)

    Kazunori Ueda, Shota Matsumoto, Akira Takeguchi, Hiroshi Hosobe, Daisuke Ishii

    Proceedings of the 2nd Workshop on Logics for System Analysis (LfSA2012) at CAV2012     3 - 17  2012.07  [Refereed]

  • HyperLMNtal: An Extension of a Hierarchical Graph Rewriting Model

    Kazunori Ueda, Seiji Ogawa

    KI - Künstliche Intelligenz   26 ( 1 ) 27 - 36  2012.02  [Refereed]

    DOI

    Scopus

    10
    Citation
    (Scopus)

  • LMNtal実行時処理系の並列モデル検査器への発展

    後町 将人, 堀 泰祐, 上田 和紀

    コンピュータ ソフトウェア   28 ( 4 ) 137 - 157  2011.11  [Refereed]

  • An Interval-Based SAT Modulo ODE Solver for Model Checking Nonlinear Hybrid Systems

    Daisuke Ishii, Kazunori Ueda, Hiroshi Hosobe

    International Journal on Software Tools for Technology Transfer   13 ( 5 ) 449 - 461  2011.10  [Refereed]

  • ハイブリッドシステムモデリング言語HydLaの実装

    松本翔太, 櫻庭翔, 高田賢士郎, 細部博史, 上田和紀

    日本ソフトウェア科学会第28回大会論文集   ( 6.00E-04 ) 1 - 11  2011.09

  • An Execution Algorithm for the Hybrid System Modeling Language HydLa

      28 ( 3 ) 167 - 172  2011.07  [Refereed]

  • ハイブリッドシステムモデリング言語HydLaの数式処理実行系

    高田賢士郎, 渋谷俊, 細部博史, 上田和紀

    情報処理学会第73回全国大会講演論文集     247 - 248  2011.03

  • Declarative semantics of the hybrid constraint language HydLa

    Kazunori Ueda, Hiroshi Hosobe, Daisuke Ishii

    Computer Software   28 ( 1 ) 306 - 311  2011

    　View Summary

    Hybrid systems are dynamical systems with continuous evolution of states and discrete evolution of states and governing equations. We have worked on the design and implementation of HydLa, a constraint-based modeling language for hybrid systems, with a view to the proper handling of uncertanties and the integration of simulation and verification. HydLa's constraint hierarchies facilitate the description of constraints with adequate strength, but its semantical foundations are not obvious due to the interaction of various language constructs. This paper gives the declarative semantics of HydLa and discusses its properties and consequences by means of examples.

  • Speedup of OWCTY Model Checking Algorithm Using Strongly Connected Components

    Toshiki KAWABATA, Fumiyoshi KOBAYASHI, Kazunori UEDA

    Transactions of the Japanese Society for Artificial Intelligence   26 ( 2 ) 341 - 346  2011  [Refereed]

    　View Summary

    Model checking is an exhaustive search method of verification. Automata-based LTL model checking is one of the methods to solve accepting cycle search problems. Model checking is prone to state-space explosion, and we may expect that parallel processing would be a promising approach. However, the optimal sequential algorithm is based on post-order depth-first seach and is difficult to parallelize. Alternative parallel algorithms have been proposed, and OWCTY_reversed is one of them. OWCTY_reversed is known to be a stable and fast algorithm for models that accept some words, but it does not use the characteristics of the automata used in LTL model checking. We propose a new algorithm named SCC-OWCTY that exploits the SCCs (strongly connected components) of property automata. The algorithm removes states that are judged not to form accepting cycles faster than OWCTY_reversed. We experimented and compared the two algorithms using DiVinE, and confirmed improvements both in performance and scalability.

    DOI CiNii

    Scopus

  • ハイブリッド制約言語HydLaの宣言的意味論(レター論文)

    Kazunori Ueda, Hiroshi Hosobe, Daisuke Ishii

    Computer Software   28 ( 1 ) 306 - 311  2011.01  [Refereed]

    Authorship：Lead author

    CiNii

  • 統合開発環境によるLMNtalモデル検査

    綾野 貴之, 堀 泰祐, 岩澤 宏希, 小川 誠司, 上田 和紀

    コンピュータソフトウェア   27 ( 4 ) 197 - 214  2010.11  [Refereed]

  • ハイブリッド制約言語HydLaの宣言的意味論

    上田和紀, 細部博史, 石井大輔

    日本ソフトウェア科学会第27回大会論文集   ( 4A-3 ) 1 - 6  2010.09

  • ハイブリッドシステムモデリング言語HydLa処理系における実行アルゴリズム

    渋谷俊, 高田賢士郎, 上田和紀, 細部博史

    日本ソフトウェア科学会第27回大会論文集   ( 1B-2 ) 1 - 6  2010.09

  • ハイブリッドシステムモデリング言語HydLa処理系の実行アルゴリズムの検討

    渋谷俊, 高田賢士郎, 上田和紀, 細部博史

    第8回ディペンダブルシステムワークショップ(DSW2010)論文集   ( 8月2日 ) 1 - 4  2010.07

  • ハイブリッドシステムモデリング言語HydLaの区間制約に基づく全解シミュレーション実行処理系

    大谷順司, 廣瀬賢一, 石井大輔, 細部博史, 上田和紀

    情報処理学会創立50周年記念(第72回)全国大会論文集     145 - 146  2010.03

  • LMNtal as a hierarchical logic programming language

    Kazunori Ueda

    Theoretical Computer Science   410 ( 46 ) 4784 - 4800  2009.11  [Refereed]

    Authorship：Lead author

    DOI CiNii

    Scopus

    19
    Citation
    (Scopus)

  • An Interval-based SAT Modulo ODE Solver for Model Checking Nonlinear Hybrid Systems

    Daisuke Ishii, Kazunori Ueda, Hiroshi Hosobe

    Proceedings of the Workshop on Verified Software: Theory, Tools, and Experiments (VSTTE2009)   ( 4 ) 1 - 9  2009.11  [Refereed]

  • Interval-based Solving of Hybrid Constraint Systems

    Daisuke Ishii, Kazunori Ueda, Hiroshi Hosobe, Alexandre Goldsztejn

    Proceedings of the 3rd IFAC Conference on Analysis and Design of Hybrid Systems (ADHS2009)     144 - 149  2009.09  [Refereed]

  • 制約階層によるハイブリッドシステムのモデリング手法

    廣瀬賢一, 大谷順司, 石井大輔, 細部博史, 上田和紀

    日本ソフトウェア科学会第26回大会論文集   ( 2D-2 ) 1 - 10  2009.09

  • Simulation of Hybrid Systems based on Hierarchical Interval Constraints (poster)

    Daisuke Ishii, Kazunori Ueda, Hiroshi Hosobe

    Proceedings of the 2nd International Conference on Simulation Tools and Techniques (SIMUTools2009)   ( 37 ) 1 - 2  2009.03  [Refereed]

  • c-sat: A Parallel SAT Solver for Clusters

    Kei Ohmura, Kazunori Ueda

    Theory and Applications of Satisfiability Testing - SAT 2009, Lecture Notes in Computer Science   5584   524 - 537  2009  [Refereed]

    DOI CiNii

    Scopus

    32
    Citation
    (Scopus)

  • Hierarchical Graph Rewriting as a Unifying Tool for Analyzing and Understanding Nondeterministic Systems

    Kazunori Ueda, Takayuki Ayano, Taisuke Hori, Hiroki Iwasawa, Seiji Ogawa

    Theoretical Aspects of Computing - ICTAC 2009, Lecture Notes in Compter Science   5684   349 - 355  2009  [Refereed]

    DOI

    Scopus

    7
    Citation
    (Scopus)

  • 微分制約論理式によるハイブリッドシステムのモデリングと検証

    石井大輔, 上田和紀, 細部博史

    電子情報通信学会コンカレント工学研究会(CST), 信学技報   108 ( 415 ) 67 - 70  2009.01

  • 制約概念に基づくハイブリッドシステムモデリング言語HydLa

    上田和紀, 石井大輔, 細部博史

    第5回システム検証の科学技術シンポジウム(SSV2008)予稿集     1 - 6  2008.11

  • ハイブリッドシステムの高信頼シミュレーションのための区間に基づく制約伝播手法

    石井大輔, 上田和紀, 細部博史

    情報処理学会論文誌：数理モデル化と応用   1 ( 1 ) 149 - 159  2008.09  [Refereed]

  • 区間演算を用いたODE Solverにおける任意精度演算の導入とパラメタ最適化

    廣瀬 賢一, 石井 大輔, 上田 和紀

    情報科学技術フォーラム講演論文集   7 ( 1 ) 75 - 78  2008.08

  • 論理・制約プログラミングと並行計算

    上田 和紀

    コンピュータソフトウェア   25 ( 3 ) 49 - 54  2008.08  [Refereed]

    Authorship：Lead author

  • ハイブリッドシステムの高信頼シミュレーションへの区間ニュートン法の適用

    石井大輔, 上田和紀, 細部博史

    第6回ディペンダブルシステムワークショップ(DSW2008)論文集     101 - 104  2008.07

  • 階層グラフ書換え言語LMNtalの処理系

    村山 敬, 工藤 晋太郎, 櫻井 健, 水野 謙, 加藤 紀夫, 上田 和紀

    コンピュータソフトウェア   25 ( 2 ) 47 - 77  2008.05  [Refereed]

  • Encoding Distributed Process Calculi into LMNtal

    Kazunori Ueda

    Electronic Notes in Theoretical Computer Science   209   187 - 200  2008.04  [Refereed]

    Authorship：Lead author

    DOI

    Scopus

    10
    Citation
    (Scopus)

  • ハイブリッドシステムの高信頼性シミュレーションのための区間に基づく制約伝播手法

    石井大輔, 上田和紀, 細部博史

    情報処理学会研究報告：数理モデル化と問題解決(MPS)   68   133 - 136  2008.03

  • 数式処理・quantifier eliminationを用いたハイブリッドシステムのZeno状態の導出手法

    大野 善之, 石井 大輔, 上田 和紀

    人工知能学会全国大会論文集 1D1-3    2008

  • 階層グラフ書換えモデルに基づく統合プログラミング言語LMNtal

    乾敦行, 工藤晋太郎, 原耕司, 水野謙, 加藤紀夫, 上田和紀

    コンピュータソフトウェア   25 ( 1 ) 124 - 150  2008.01  [Refereed]

    CiNii

  • ハイブリッド並行制約プログラミングにおける分岐を含む軌道の区間包囲の求解手法

    石井大輔, 上田和紀, 細部博史

    日本ソフトウェア科学会第24回大会論文集   ( 6C-1 ) 1 - 6  2007.09

  • A Branching Approach to the Interval-based Evaluation of Ask Constraints in Hybrid CCP

    Daisuke Ishii, Kazunori Ueda, Hiroshi Hosobe

    Proc. CP 2007 Doctoral Programme, the 13th Int. Conf. on Principles and Practice of Constraint Programming (CP2007)     49 - 54  2007.09

  • SATソルバMiniSatの並列化とそのチューニング手法

    大村圭, 渋谷健介, 稲垣良一, 上田和紀

    情報処理学会研究報告   2007 ( 80 ) 31 - 36  2007.08

    　View Summary

    This paper describes parallelization of the SAT solver MiniSat based on lemma sharing and its tuning techniques. When an SAT solver finds that a specific branch of the search space does not have a solution, it learns new clauses called lemmas. Lemmas are very useful for pruning search space. However, since sharing lemmas between PEs can take enormous communication cost, developing efficient learning and communication techniques is very important. Using parameters obtained by various experiments on lemma sharing, our parallel MiniSAT solved many more SAT competition problems than the original MiniSAT on a PC cluster with 24 PEs.

    CiNii

  • モデル検査器SPINにおける状態空間の性質の調査

    渋谷健介, 上田和紀

    第5回ディペンダブルシステムワークショップ(DSW2007)論文集     9 - 12  2007.07

  • 数式処理に基づくハイブリッドシステムにおけるZenonessの判定手法

    大野善之, 石井大輔, 上田和紀

    第5回ディペンダブルシステムワークショップ論文集     53 - 56  2007.07

  • An Interval-based Approximation Method for Discrete Changes in Hybrid cc

    Daisuke Ishii, Kazunori Ueda, Hroshi Hosobe

    Trends in Constraint Programming     245 - 255  2007.05  [Refereed]

  • 階層グラフ可視化ツール"UNYO-UNYO"(うにょうにょ)の設計と実装

    中野敦, 上田和紀

    第9回プログラミングおよびプログラミング言語ワークショップ (PPL2007)    2007.03

  • 純粋λ計算の階層グラフ書換えへのエンコーディング

    上田和紀

    第9回プログラミングおよびプログラミング言語ワークショップ (PPL2007)     221 - 232  2007.03

  • Hierarchical graph rewriting as a unifying model of concurrency

    Kazunori Ueda

    LIX Colloquium on Emerging Trends in Concurrency Theory    2006.11  [Invited]

  • 後継関数を持つリスト型非線形再帰プログラムに対する再帰除去法

    市川祐輔, 上田和紀

    情報科学技術レターズ   6   9 - 12  2006.09  [Refereed]

  • 分散プロセス計算のLMNtalへのエンコーディング

    上田和紀

    日本ソフトウェア科学会第23回大会論文集     1A - 4  2006.09

  • Hybrid cc における区間計算に基づいた離散変化処理方式

    石井大輔, 上田和紀, 細部博史

    日本ソフトウェア科学会第23回大会論文集     1A - 1  2006.09

  • An Interval-based Approximation Method for Discrete Changes in Hybrid cc

    Daisuke Ishii, Kazunori Ueda, Hiroshi Hosobe

    Third International Workshop on Interval Analysis, Constraint Propagation and Applications (IntCP'06)     38 - 51  2006.09  [Refereed]

  • Constraint-Based Concurrency and Beyond

    Kazunori Ueda

    Electronic Notes in Theoretical Computer Science   162   327 - 331  2006.09

  • LMNtal as a Unifying Declarative Language

    Kazunori Ueda, Norio Kato, Koji Hara, Ken Mizuno

    Third Workshop on Constraint Handling Rules (CHR 2006)     1 - 15  2006.07  [Invited]

  • Logic Programming and Concurrency: a Personal Perspective

    Kazunori Ueda

    The ALP NewsLetter   19 ( 2 )  2006.05  [Invited]

  • アセンブリプログラムの構造を利用したキャッシュヒント自動付加

    稲垣良一, 上田和紀

    先進的計算基盤システムシンポジウム (SACSIS2006)     59 - 66  2006.05

  • 階層グラフ書き換え言語LMNtal処理系とその応用例

    乾敦行, 原耕司, 水野謙, 上田和紀

    第8回プログラミングおよびプログラミング言語ワークショップ (PPL2006)     119 - 133  2006.03

  • 非決定的LMNtalとその検証への応用

    水野謙, 上田和紀

    第8回プログラミングおよびプログラミング言語ワークショップ (PPL2006)    2006.03

  • OCamlによるLMNtal実行時処理系 OCaMNtalの実装

    工藤晋太郎, 乾敦行, 櫻井健, 上田和紀

    第8回プログラミングおよびプログラミング言語ワークショップ (PPL2006)    2006.03

  • LMNtal as a unifying declarative language: Live demonstration

    Kazunori Ueda, Norio Kato, Koji Hara, Ken Mizuno

    LOGIC PROGRAMMING, PROCEEDINGS   4079   457 - 458  2006  [Refereed]

  • LMNtalコンパイラにおける並び替えとグループ化を用いた命令列の最適化

    櫻井健, 加藤紀夫, 水野謙, 上田和紀

    第4回情報科学技術フォーラム (FIT2005)   A-014 ( 第一分冊 ) 33 - 36  2005.09

  • JP ドメインにおける茶筌を用いた中国語ページの抽出

    魏小比, 内藤一兵衛, 上田和紀

    第4回情報科学技術フォーラム (FIT2005)   ( 第二分冊 ) 179 - 182  2005.09

  • 数式処理システムMathematica上における再帰除去システム

    市川祐輔, 二村良彦, 上田和紀

    第4回情報科学技術フォーラム (FIT2005)   A-022 ( 第一分冊 ) 53 - 54  2005.09

  • キャッシュヒント自動付加を用いたソフトウェア高速化

    稲垣良一, 上田和紀

    第4回情報科学技術フォーラム (FIT2005)   B-030 ( 第一分冊 ) 161 - 162  2005.09

  • LMNtal処理系におけるグラフ構造の複製・破棄および比較機能の設計と実装

    工藤晋太郎, 上田和紀, 加藤紀夫

    情報科学技術レターズ   LA-003   9 - 12  2005.09  [Refereed]

  • 階層グラフ書換え言語LMNtal処理系における非同期実行の実現

    水野謙, 加藤紀夫, 原耕司, 上田和紀

    日本ソフトウエア科学会第22回大会講演論文集     3A - 4  2005.09

  • Constraint-Based Concurrency and Beyond

    Kazunori Ueda

    Proc. Workshop on Algebraic Process Calculi, The First Twenty Years     227 - 230  2005.08  [Invited]

  • 確率モデル遺伝的アルゴリズムEHBSAにおける戦略、パラメータの調査

    酒井大輔, 上田和紀

    人工知能学会全国大会(第19回)論文集     2F1 - 02  2005.06

  • Itanium2プロセッサにおけるキャッシュヒント自動付加手法

    稲垣良一, 上田和紀

    先進的計算基盤シンポジウム SACSIS2005     218 - 219  2005.05

  • 21世紀COEプロジェクト「プロダクティブICTアカデミア」

    上田和紀, 大石進一, 甲藤二郎, 中島達夫, 村岡洋一, 山名早人

    情報処理   46 ( 4 ) 410 - 416  2005.04

  • 並列論理型言語のコンパイル技法

    上田和紀

    情報処理学会第67回全国大会特別セッション(6)    2005.03

  • LMNtalを用いた分散処理の実現

    中島求, 加藤紀夫, 水野謙, 上田和紀

    第8回 プログラミングおよび応用のシステムに関するワークショップ (SPA2005)    2005.03

  • 小規模制御系向けLMNtal処理系の設計と実装

    矢島伸吾, 加藤紀夫, 上田和紀

    第7回プログラミングおよびプログラミング言語ワークショップ (PPL2005)     41 - 41  2005.03

  • 階層グラフ書き換えによるプロトコル検証

    圷弘明, 加藤紀夫, 上田和紀

    第7回プログラミングおよびプログラミング言語ワークショップ (PPL2005)     41 - 41  2005.03

  • プログラムと対称性

    上田和紀

    夏のプログラミングシンポジウム「アッと驚くプログラミング」報告集     69 - 74  2005.01

  • 20世紀の名著名論 - C. A. R. Hoare: Communicating Sequential Processes

    上田和紀

    情報処理   46 ( 1 ) 66 - 66  2005.01

  • 言語モデルLMNtalの操作的意味論の設計

    加藤紀夫, 水野謙, 上田和紀

    日本ソフトウェア科学会第21回大会論文集     153 - 163  2004.09

  • LMNtal分散処理系の設計と実装

    中島求, 加藤紀夫, 水野謙, 上田和紀

    日本ソフトウェア科学会第21回大会論文集     149 - 153  2004.09

  • LMNtal処理系および他言語インタフェースの設計と実装

    原耕司, 水野謙, 矢島伸吾, 永田貴彦, 中島求, 加藤紀夫, 上田和紀

    情報処理学会第50回プログラミング研究会 (SWoPP2004)    2004.07

  • SATソルバzchaffのMPIによる並列化

    大橋智昭, 稲垣良一, 上田和紀

    情報処理学会研究報告 2004-HPC99-5 (SWoPP2004)     25 - 30  2004.07

  • 階層グラフ書換え言語における並行プロセスの型推論

    加藤紀夫, 上田和紀

    情報処理学会第50回プログラミング研究会 (SWoPP2004)    2004.07

  • SMPクラスタにおける効率的なMPI集団通信関数の実装

    稲垣良一, 上田和紀

    先進的計算基盤システムシンポジウム SACSIS2003     171 - 172  2004.05

  • SATソルバzchaffのMPIによる並列化

    大橋智昭, 上田和紀

    先進的計算基盤シンポジウム SACSIS2004   LNCS 3365, Springer-Verlag   147 - 148  2004.05

  • The Language Model LMNtal

    UEDA Kazunori, KATO Norio, Kazunori Ueda, Norio Kato, Dept. of Computer Science Waseda University:CREST Japan Science and Technology Corporation., Dept. of Computer Science Waseda University

    Computer Software   21 ( 2 ) 126 - 142  2004.03

    DOI CiNii

    Scopus

    1
    Citation
    (Scopus)

  • 制約に基づくアニメーション作成環境 Grifon

    石井大輔, 中村好一, 大野太郎, 若槻聡一郎, 上田和紀

    情報処理学会第66回全国大会     1J - 2  2004.03

  • 制約に基づくアニメーション作成環境 Grifon におけるデータ構造の階層化

    中村好一, 石井大輔, 大野太郎, 若槻総一郎, 上田和紀

    情報処理学会第66回全国大会     1J - 1  2004.03

  • LMNtalルールコンパイラにおける内部命令の設計

    水野謙, 永田貴彦, 加藤紀夫, 上田和紀

    情報処理学会第66回全国大会     5G - 2  2004.03

  • LMNtalにおけるルールセット不変性の検査

    圷弘明, 加藤紀夫, 上田和紀

    第6回プログラミングおよびプログラミング言語ワークショップ (PPL2004)     211 - 216  2004.03

  • 並行言語モデルLMNtalにおけるプロセス構造の解析

    加藤紀夫, 上田和紀

    第6回プログラミングおよびプログラミング言語ワークショップ (PPL2004)     217 - 222  2004.03

  • 言語モデルLMNtal

    上田和紀, 加藤紀夫

    コンピュータソフトウェア   21 ( 2 ) 44 - 60  2004.03  [Refereed]

    CiNii

  • LMNtal: A language model with links and membranes

    K Ueda, N Kato

    Proc. Fifth Int. Workshop on Membrane Computing (WMC 2004), Lecture Notes in Computer Science   3365   110 - 125  2004  [Refereed]  [Invited]

    　View Summary

    LMNtal (pronounced "elemental") is a simple language model based on graph rewriting that uses logical variables to represent links and membranes to represent hierarchies. The two major goals of LMNtal are (i) to unify various computational models based on multiset rewriting and (ii) to serve as the basis of a truly general-purpose language covering various platforms ranging from wide-area to embedded computation. Another important contribution of the model is that it greatly facilitates programming with dynamic data structures.

  • The language model LMNtal

    K Ueda, N Kato

    Logic Programming. ICLP 2003. Lecture Notes in Computer Science   2916   517 - 518  2003.12  [Refereed]

    Authorship：Lead author

  • Teaching (Constraint) Logic Programming

    Kazunori Ueda

    Panel at Nineteenth Int. Conf. on Logic Programming (ICLP'03)   http://www.cs.kuleuven.ac.be/~dtai/projects/ALP/ newsletter/nav/short.html  2003.12  [Invited]

  • LMNtalプロセスの振舞いの定式化

    加藤紀夫, 上田和紀

    日本ソフトウェア科学会第20回大会論文集   16-20   16 - 20  2003.09

  • LMNtalプロトタイプ処理系の設計と実装

    矢島伸吾, 永田貴彦, 加藤紀夫, 上田和紀

    日本ソフトウェア科学会第20回大会論文集   21-25   21 - 25  2003.09

    CiNii

  • 人工知能学会2002年度全国大会ベストプレゼンテーション賞

    網代育大, 上田和紀

    人工知能学会   (発表題目「反復深化A*探索によるもっともらしいプログラムの効率的生成」)  2003.04

  • KLIC処理系におけるUNIXプロセス間通信を利用した例外処理の実装

    金木佑介, 加藤紀夫, 上田和紀

    第6回プログラミングおよび応用のシステムに関するワークショップ (SPA2003)   http://spa.jssst.or.jp/2003/program/  2003.03

  • LMNtalプロトタイプ処理系の設計と実装

    日本ソフトウェア科学会第20回大会論文集   21-25  2003

  • LMNtalプロセスの振舞いの定式化

    日本ソフトウェア科学会第20回大会論文集   16-20  2003

  • KLIC処理系におけるUNIXプロセス間通信を利用した例外処理の実装

    第6回プログラミングおよび応用のシステムに関するワークショップ (SPA2003)、日本ソフトウェア科学会    2003

  • Programming with Logical Links: Design of the LMNtal language

    Kazunori Ueda, Norio Kato

    Proc. 3rd Asian Workshop on Programming Languages and Systems (APLAS 2002)   pp.115-126   115 - 126  2002.11

  • 分散言語処理系DKLIC の設計と実装

    高山啓, 松村量, 高木祐介, 加藤紀夫, 上田和紀

    日本ソフトウェア科学会第19回大会論文集     5F - 1  2002.09

  • モード制約の漸近的一様補強による並行論理プログラムのoccurs-check解析

    加藤紀夫, 上田和紀

    日本ソフトウェア科学会第19回大会論文集     5F - 2  2002.09

  • GHCからLMNtalへ

    上田和紀

    情報処理学会 2002年度 夏のプログラミングシンポジウム   http://www.ipsj.or.jp/prosym/sprosym/program/LMNtal-prosym.pdf  2002.09

  • 20世紀の名著名論 - J. A. Robinson: A Machine-Oriented Logic Based on the Resolution Principle

    上田和紀

    情報処理   43 ( 7 ) 792 - 792  2002.07

  • 反復深化A*探索によるもっともらしいプログラムの効率的な生成

    網代育大, 上田和紀

    人工知能学会全国大会(第17回)論文集   1E3-02   1E3 - 02  2002.06

  • 反復深化A*探索によるもっともらしいプログラムの効率的な生成

    人工知能学会全国大会(第17回)論文集   1E3-02  2002

  • Programming with Logical Links

    日本ソフトウェア科学会第19回大会論文集    2002

  • モード制約の漸近的一様補強による並行論理プログラムのoccurs-check解析

    日本ソフトウェア科学会第19回大会論文集    2002

  • Programming with Logical Links: Design of the LMNtal language

    Proc. 3rd Asian Workshop on Programming Languages and Systems (APLAS 2002)   pp.115-126  2002

  • Sequentiality analysis for concurrent logic programs

    N Kato, K Ueda

    6TH WORLD MULTICONFERENCE ON SYSTEMICS, CYBERNETICS AND INFORMATICS, VOL XI, PROCEEDINGS   Vol.11, pp.329-336   329 - 336  2002

    　View Summary

    We present a bottom-up method of extracting those fragments of concurrent logic programs that can be executed sequentially, and we also propose a framework of optimizing compilation of concurrent logic programs that uses sequential intermediate code generated with the method. The method is directed by the inference of certain properties on sequentiality, called interfaces, of concurrent processes. We formalize them in terms of the operational semantics, which enables us to formally justify the inference laws on interfaces used in the analysis.
    The specialization of concurrent processes is critical for an optimizing compiler, for it can reduce the runtime overhead of process management and of data manipulation substantially. The inference laws on interfaces ensure the compositional generation of the sequential specialized code that enables such optimization. Moreover, a formal definition of the intermediate code will prove the correctness of some implementation-level optimization techniques, including tag elimination and update-in-place optimization, that cannot be formally proved by source-level analysis.
    Although the formalism of interfaces exploits the constraint-based communication feature of the language, our method can be applied, in principle, to the extraction of sequentiality in other fine-grained concurrent languages.

  • A pure meta-interpreter for flat GHC, a concurrent constraint language

    K Ueda

    COMPUTATIONAL LOGIC: LOGIC PROGRAMMING AND BEYOND, PT I   2407   138 - 161  2002  [Refereed]  [Invited]

    　View Summary

    This paper discusses the construction of a meta-interpreter, of Flat GHC, one of the simplest and earliest concurrent constraint languages.
    Meta-interpretation has a long history in logic programming, and has been applied extensively to building programming systems, adding functionalities, modifying operational semantics and evaluation strategies, and so on. Our objective, in contrast, is to design the pair of (i) a representation of programs suitable for code mobility and (ii) a pure interpreter (or virtual machine) of the represented code, bearing networked applications of concurrent constraint programming in mind. This is more challenging than it might seem; indeed, meta-interpreters of many programming languages achieved their objectives by adding small primitives into the languages and exploiting their functionalities. A meta-interpreter in a pure, simple concurrent language is useful because it is fully amenable to theoretical support including partial evaluation. After a number of trials and errors, we have arrived at treecode, a ground-term representation of Flat GHC programs that can be easily interpreted,, transmitted over the network, and converted back to the original syntax. The paper describes how the interpreter works, where the subtleties lie,, and what its design implies. It also describes how the interpreter, given the treecode of a program, is partially evaluated to the original program by the unfold/fold transformation system for Flat GHC.

  • Kima: An automated error correction system for concurrent logic programs

    Yasuhiro Ajiro, Kazunori Ueda

    Automated Software Engineering   9 ( 1 ) 67 - 94  2002.01  [Refereed]

    　View Summary

    We have implemented Kima, an automated error correction system for concurrent logic programs. Kima corrects near-misses such as wrong variable occurrences in the absence of explicit declarations of program properties. Strong moding/typing and constraint-based analysis are turning out to play fundamental roles in debugging concurrent logic programs as well as in establishing the consistency of communication protocols and data types. Mode/type analysis of Moded Flat GHC is a constraint satisfaction problem with many simple mode/type constraints, and can be solved efficiently. We proposed a simple and efficient technique which, given a non-well-moded/typed program, diagnoses the "reasons" of inconsistency by finding minimal inconsistent subsets of mode/type constraints. Since each constraint keeps track of the symbol occurrence in the program, a minimal subset also tells possible sources of program errors. Kima realizes automated correction by replacing symbol occurrences around the possible sources and recalculating modes and types of the rewritten programs systematically. As long as bugs are near-misses, Kima proposes a rather small number of alternatives that include an intended program. Search space is kept small because the minimal subset confines possible sources of errors in advance. This paper presents the basic algorithm and various optimization techniques implemented in Kima, and then discusses its effectiveness based on quantitative experiments.

    DOI

    Scopus

    9
    Citation
    (Scopus)

  • Sequentiality analysis for concurrent logic programs

    N Kato, K Ueda

    6TH WORLD MULTICONFERENCE ON SYSTEMICS, CYBERNETICS AND INFORMATICS, VOL XI, PROCEEDINGS   Vol.11, pp.329-336   329 - 336  2002  [Refereed]

    　View Summary

    We present a bottom-up method of extracting those fragments of concurrent logic programs that can be executed sequentially, and we also propose a framework of optimizing compilation of concurrent logic programs that uses sequential intermediate code generated with the method. The method is directed by the inference of certain properties on sequentiality, called interfaces, of concurrent processes. We formalize them in terms of the operational semantics, which enables us to formally justify the inference laws on interfaces used in the analysis.
    The specialization of concurrent processes is critical for an optimizing compiler, for it can reduce the runtime overhead of process management and of data manipulation substantially. The inference laws on interfaces ensure the compositional generation of the sequential specialized code that enables such optimization. Moreover, a formal definition of the intermediate code will prove the correctness of some implementation-level optimization techniques, including tag elimination and update-in-place optimization, that cannot be formally proved by source-level analysis.
    Although the formalism of interfaces exploits the constraint-based communication feature of the language, our method can be applied, in principle, to the extraction of sequentiality in other fine-grained concurrent languages.

  • Programming with Logical Links

    上田和紀, 加藤紀夫

    日本ソフトウェア科学会第19回大会論文集     3A - 1  2002

  • Optimizing Compilation of Concurrent Logic Programs Directed by Interface Analysis

    Proc. Second Asian Workshop on Programming Languages and Systems   pp.237-250  2001.12

  • Resource-Passing Concurrent Programming

    Proc. Second Asian Workshop on Programming Languages and Systems, KAIST, Daejeon, Korea   pp.313-328  2001.12

  • 人工知能とソフトウェア文化

    人工知能学会誌/人工知能学会   16;6  2001.11

  • インタフェースに基づく並行論理プログラム最適化コンパイラの構成法

    情報処理学会第36回プログラミング研究会    2001.10

  • Resource-Passing Concurrent Programming

    Proc. Fourth Int. Symp. on Theoretical Aspects of Computer Software, Kobayashi, N. and Pierce, B. (Eds.), Springer-Verlag   LNCS 2215, pp.95-126  2001.10  [Refereed]  [Invited]

  • 計算連続体に基づくソフトウェア実現法の提案

    日本ソフトウェア科学会第18回大会講演論文集/日本ソフトウェア科学会    2001.09  [Refereed]

  • インタフェースに基づく並行論理プログラム最適化コンパイラの構成法

    日本ソフトウェア科学会第18回大会講演論文集/日本ソフトウェア科学会    2001.09

  • 制約の局所性に基づく並行論理プログラム自動修正系 Kima の最適化

    日本ソフトウェア科学会第18回大会講演論文集/日本ソフトウェア科学会    2001.09

  • 計算連続体に基づくソフトウェア実現法の提案

    日本ソフトウェア科学会第18回大会講演論文集/日本ソフトウェア科学会    2001.09

  • 日本ソフトウェア科学会第18回大会講演論文集

    日本ソフトウェア科学会    2001.09

  • MPIによるGIMP並列化

    並列処理シンポジウム (JSPP2001) 論文集,情報処理学会   pp.123-124  2001.06

  • 日本ソフトウェア科学会第5回論文賞(論文題目“自己調整二分木の並列操作”)

    日本ソフトウェア科学会    2001.05

  • dklic: KL1による分散KL1言語処理系の実装

    第4回プログラミングおよび応用のシステムに関するワークショップ (SPA2001),日本ソフトウェア科学会    2001.03

  • 並列KLIC処理系上での配列演算の最適化

    情報処理学会論文誌:プログラミング   42;SIG 3(PRO 10), pp.1-13  2001.03  [Refereed]

  • 並行論理プログラムにおける逐次実行部分の抽出方法論

    第3回プログラミングおよびプログラミング言語ワークショップ (PPL2001),日本ソフトウェア科学会   pp.2-13  2001.03

  • 並列KLIC処理系上での配列演算の最適化

    情報処理学会論文誌:プログラミング   42;SIG 3(PRO 10), pp.1-13  2001.03

  • TECO

    bit/共立出版   33;2, pp.48-54  2001.02

  • Resource-Passing Concurrent Programming

    Proc. Second Asian Workshop on Programming Languages and Systems   pp.313-328  2001

  • A Close Look at Constraint-Based Concurrency

    Proc. 17th Int. Conf. on Logic Programming, Philippe Codognet (ed.), Springer-Verlag   LNCS 2237, p.9  2001  [Invited]

  • Functional and Logic Programming-5th International Symposium on Functional and Logic Programming (FLOPS 2001)

    Springer-Verlag   Lecture Notes in Computer Science 2024  2001

  • シンガポール国立大学

    人工知能学会誌   16;1, pp.169-170  2001.01

  • Crosoeは成功するか? - 私はCrusoeを使いたい

    情報処理   41;9  2000.09

  • Kima -- an Automated Error Correction System for Concurrent Logic Programs

    Proc. Fourth International Workshop on Automated Debugging (AADEBUG 2000)   http://www.irisa.fr/lande/ducasse/ aadebug2000/proceedings.html  2000.09  [Refereed]

  • 並行論理プログラムのプログラム空間に関する考察

    2000年度人工知能学会全国大会(第14回)論文集   pp.449-452  2000.07

  • Linearity Analysis of Concurrent Logic Programs

    K Ueda

    Proc. International Workshop on Parallel and Distributed Computing for Symbolic and Irregular Applications, Ito, T. and Yuasa, T. (eds.), World Scientific   pp.253-270   253 - 270  2000.05

    　View Summary

    Automatic memory management and the hiding of the notion of pointers are the prominent features of symbolic processing languages. They make programming easy and guarantee the safety of memory references. For the memory management of linked data structures, copying garbage collection is most widely used because of its simplicity and desirable properties. However, if certain properties about runtime storage allocation and the behavior of pointers can be obtaind by static analysis, a compiler may be able to generate object code closer to that of procedural programs. In the fields of parallel, distributed and real-time computation, it is highly desirable to be able to identify data structures in a program that can be managed without using garbage collection. To this end, this paper proposes a framework of linearity analysis for a concurrent logic language Moded Flat GHC, and proves its basic property. The purpose of linearity analysis is to distinguish between fragments of data structures that may be referenced by two or more pointers and those that cannot be referenced by two or more pointers. Data structures with only one reader are amenable to compile-time garbage collection or local reuse. The proposed framework of linearity analysis is constraint-based and involves both equality and implicational constraints. It has been implemented as part of klint v2, a static analyzer for KL1 programs.

  • 第五世代核言語ができるまで

    第3回システムおよびプログラミングの応用に関するワークショップ (SPA2000)    2000.03  [Invited]

  • 共有オブジェクト空間を用いた分散プログラミング支援ミドルウェア SOR (Shared Object Repository) とその応用例の紹介

    情報処理学会第60回全国大会講演論文集(1)   1ZB-05, pp.313-314  2000.03

  • 並行論理プログラム自動修正系 kima における誤り検出率の向上とその効果

    情報処理学会第60回全国大会講演論文集(1)   2V-06, pp.283-284  2000.03

  • 並行論理プログラムの静的 Occur-checker の設計と実装

    情報処理学会第60回全国大会講演論文集(1)   2V-05, pp.281-282  2000.03

  • Java 仮想機械上で動作する分散 KL1 言語処理系の実装

    情報処理学会第60回全国大会講演論文集(1)   2H-01, pp.13-14  2000.03

  • 存在価値のある研究会を目指して—プログラミング研究会の試み—

    情報処理学会第60回全国大会記念セッション・イベント報告集   pp.127-130  2000.03

  • 並行論理型言語における同期ポイントの移動の安全性について

    情報処理学会論文誌:プログラミング   41 ( SIG 2(PRO 6) ) 13 - 28  2000.03  [Refereed]

  • Kima - an Automated Error Correction System for Concurrent Logic Programs.

    Yasuhiro Ajiro, Kazunori Ueda

    Computer Software   18 ( 0 ) 122 - 137  2000  [Refereed]

    DOI

    Scopus

    1
    Citation
    (Scopus)

  • 共有オブジェクト空間を用いた分散プログラミング支援ミドルウェアSOR(Shared Object Repository)とその応用例の紹介

    情報処理学会第60回全国大会講演論文集(1)   /,1ZB-05,313-314  2000

  • 並行論理プログラム自動修正系kimaにおける誤り検出率の向上とその効果

    情報処理学会第60回全国大会講演論文集(1)   /,2V-06,283-284  2000

  • 並行論理プログラムの静的Occur-checkerの設計と実装

    情報処理学会第60回全国大会講演論文集(1)   /,2V-05,281-282  2000

  • Java仮想機械上で動作する分散KL1言語処理系の実装

    情報処理学会第60回全国大会講演論文集(1)   /,2H-01,13-14  2000

  • Linearity Analysis of Concurrent Logic Programs

    Proc. International Workshop on Optimization and Implementation of Declarative Programs (WOID'99), abstract also in Electronic Notes in Theoretical Computer Science 30(2)   http://www.dsse.ecs.soton.ac.uk/ techreports/  1999.11

  • 自己調整二分木の並列操作

    コンピュータソフトウェア   16 ( 5 ) 78 - 83  1999.09  [Refereed]

    Authorship：Lead author

  • 全文検索システムVernoのアーキテクチャの設計

    第2回インターネットテクノロジワークショップ (WIT'99) 論文集   pp.163-170  1999.08

  • 分散KL1言語処理系の設計と実装

    並列処理シンポジウム(JSPP'99)論文集   p.207  1999.06

  • KLIC並列処理系における配列演算の最適化

    並列処理シンポジウム(JSPP'99)論文集   p.208  1999.06

  • Concurrent Logic/Constraint Programming: The Next 10 Years

    The Logic Programming Paradigm: A 25-Year Perspective, K. R. Apt, V. W. Marek, M. Truszczynski, and D. S. Warren (eds.), Springer-Verlag   pp.53-71  1999.04  [Refereed]  [Invited]

  • KLIC へのデータ並列処理機能の導入について

    情報処理学会第58回全国大会講演論文集/情報処理学会   4N-02  1999.03

  • 汎用並列組合せ最適化パッケージの構想

    情報処理学会第58回全国大会講演論文集/情報処理学会   3K-02  1999.03

  • WWW全文検索システムVernoのアーキテクチャ

    情報処理学会第58回全国大会講演論文集/情報処理学会   4T-07  1999.03

  • オブジェクト共有空間を利用した分散プログラミング支援フレームワークSOR

    第2回プログラミングおよび応用のシステムに関するワークショップ(SPA'99)/日本ソフトウェア科学会   http://www.softlab.is.tsukuba.ac.jp/ spa99proc/  1999.03

  • WWW全文検索システムVernoのアーキテクチャ

    情報処理学会第58回全国大会講演論文集/情報処理学会   4T-07  1999.03  [Refereed]

  • WWW全文検索システムVernoのデータベース

    情報処理学会第58回全国大会講演論文集/情報処理学会   4T-06  1999.03

  • 並行論理プログラムの参照数解析

    情報処理学会論文誌:プログラミング/情報処理学会   40;SIG1(PRO2),p.60  1999.02

  • Linearity Analysis of Concurrent Logic Programs

    Electronic Notes in Theoretical Computer Science   30;2  1999

    Authorship：Lead author

  • 全文検索システムVernoのアーキテクチャの設計

    第2回インターネットテクノロジワークショップ(WIT'99)論文集/日本ソフトウェア科学会   /,163-170  1999

  • WWW全文検索システムVernoのデータベース

    情報処理学会第58回全国大会講演論文集/情報処理学会   4T-06  1999

  • KLICへのデータ並列処理機能の導入について

    情報処理学会第58回全国大会講演論文集/情報処理学会   4N-02  1999

  • 汎用並列組合せ最適化パッケージの構想

    情報処理学会第58回全国大会講演論文集/情報処理学会   3K-02  1999

  • オブジェクト共有空間を利用した分散プログラミング支援フレームワークSOR

    第2回プログラミングおよび応用のシステムに関するワークショップ(SPA'99)/日本ソフトウェア科学会   http://www.softlab.is.tsukuba.ac.jp/ spa99proc/  1999

  • ハードウェアの進歩とソフトウェアの進歩

    bit別冊「はじめての並列プログラミング」/共立出版   p.100  1998.05

  • Bookガイド - プログラミング言語編

    bit/共立出版   30;4, pp.56-64  1998.04

  • 分散型WWW全文収集ロボットIron33

    情報処理学会第56回全国大会論文集    1998.03

  • 学習型WWW全文検索エンジンVerno

    情報処理学会第56回全国大会論文集    1998.03

  • 自己調整二分木の並列操作

    日本ソフトウェア科学会第15回大会論文集     173 - 176  1998

    Authorship：Lead author

  • Error-correcting source code

    Y Ajiro, K Ueda, K Cho

    Principles and Practice of Constraint Programming - CP98, Lecture Notes in Computer Science   1520   40 - 54  1998  [Refereed]

    　View Summary

    We study how constraint-based static analysis can be applied to the automated and systematic debugging of program errors.
    Strongly moding and constraint-based mode analysis are turning to play fundamental roles in debugging concurrent logic/constraint programs as well as in establishing the consistency of communication protocols and in optimization. Mode analysis of Moded Flat GHC is a constraint satisfaction problem with many simple mode constraints, and can be solved efficiently by unification over feature graphs. We have proposed a simple and efficient technique which, given a non-well-moded program, diagnoses the "reasons" of inconsistency by finding minimal inconsistent subsets of mode constraints. Since each constraint keeps track of the symbol occurrence in the program that imposed the constraint, a minimal subset also tells possible sources of program errors. The technique is quite general and can be used with other constraint-based frameworks such as strong typing.
    Based on the above idea, we study the possibility of automated debugging an the absence of mode/type declarations. The mode constraints are usually imposed redundantly, and the constraints that are considered correct can be used for correcting wrong symbol occurrences found by the diagnosis. As long as bugs are near-misses, the automated debugger can propose a rather small number of alternatives that include the intended program. Search space is kept small because constraints effectively prune many irrelevant alternatives. The paper demonstrates the technique by way of examples.

  • 静的解析と制約充足によるプログラム自動デバッグ

    コンピュータソフトウェア   15 ( 1 ) 54 - 58  1998.01  [Refereed]

  • Optimizing KLIC Generic Objects by Static Analysis

    Kazunori Ueda, Ryoji Tsuchiyama

    Proc. 11th Int. Conf. on Applications of Prolog/Prolog Association of Japan     27 - 33  1998

    Authorship：Lead author

    CiNii

  • Constraint-Based Automated Debugging

    Dagstuhl Seminar (9741) on Concurrent Constraint Programming: The Next Ten Years, Schloss Dagstuhl, Germany    1997.10

  • 静的解析と制約充足によるプログラム自動デバッグ

    日本ソフトウェア科学会第14回大会論文集   pp.533-536  1997.10

  • 見込み計算を用いたニュースリーダの応答性改善法

    情報処理学会論文誌   38;6,pp.1235-1243  1997.06  [Refereed]

  • 制約に基づく解析による並行論理プログラムの自動デバッグ

    人工知能学会全国大会論文集   pp.205-208  1997.06

  • Diagnosis of Concurrent Logic Programs

    Dagstuhl Seminar (9704) on High-Level Concurrent Languages (Schloss Dagstuhl, Germany)    1997.01

  • 制約概念に基づくプログラム解析・診断・デバッグ-並行論理型言語への適用

    日本ソフトウェア科学会大会論文集/日本ソフトウェア科学会    1996.09

  • Diagnosing Non-Well-Moded Concurrent Logic Programs

    Proc. 1996 Joint Conference and Symposium on Logic Programming (Michael Maher (Ed.))/The MIT Press   215-229  1996.09  [Refereed]

  • 並列計算機システムFOLON上へのPVMの移植と評価

    情報処理学会研究報告/情報処理学会   96;80 (96-ARC-119)  1996.08

  • 並行論理プログラムのモード解析手法を用いた静的診断

    人工知能学会全国大会論文集/人工知能学会    1996.06

  • モード誤りをもつ並行論理プログラムの静的デバッグ手法

    1996年並列処理シンポジウム論文集/情報処理学会    1996.06  [Refereed]

  • Experiences with Strong Moding in Concurrent Logic/Constraint Programming

    K Ueda

    Proc. International Workshop on Parallel Symbolic Languages and Systems (T. Ito, R. H. Halstead, C. Queinnec (Eds.)), Lecture Notes in Computer Science 1068/Springer-Verlag   1068   134 - 153  1996.04

    　View Summary

    Strong moding is turning out to play fundamental roles in concurrent logic programming (or in general, concurrent constraint programming) as strong typing does but in different respects. ''Principal modes'' can most naturally be represented as feature graphs and can be formed by unification. We built a mode analyzer, implementing mode graphs and their operations by means of concurrent processes and streams (rather than records and pointers). This is a non-trivial programming experience crith complicated process structures and has provided us with several insights into the relationship between programming with dynamic data structures and programming with dynamic process structures. The mode analyzer was then applied to the analyzer itself to study the characteristics of the mode constraints it imposed and of the form of large mode graphs. Finally, we show how our framework based on principal moding can be extended to deal with (1) random-access data structures, (2) mode polymorphism (3) higher-order constructs, and (4) various non-Herbrand constraint systems.

  • 並列計算機システムFOLONの通信ライブラリの設計と評価

    情報処理学会研究報告/情報処理学会   96;23 (93-ARC-117)  1996.03

  • プログラムを書こう,プログラムを読もう

    bit/共立出版   28;1  1996.01

  • 見込み計算を用いたネットワークニュースリーダの応答性改善法

    インタラクティブ・システムとソフトウェアIII(田中二郎編)/近代科学社    1995.11

  • Experiences with Strong Moding in Concurrent Logic/Constraint Programming

    International Workshop on Parallel Symbolic Languages andSystems (PSLS'95, Beaune, France)    1995.10

  • Strong Moding in Concurrent Logic/Constraint Programming

    Twelfth International Conference on Logic Programming (ICLP'95, Kanagawa, Japan)    1995.06  [Invited]

  • I/O Mode Analysis in Concurrent Logic Programming

    Kazunori Ueda

    Theory and Practice of Parallel Programming (Ito, T. and Yonezawa, A., eds.), Lecture Notes in Computer Science 907/Springer-Verlag   907   356 - 368  1995.05

    　View Summary

    This paper briefly reviews concurrent logic programming and the I/O mode system designed for the concurrent logic language Flat GHC. The mode system plays fundamental roles both in programming and implementation in almost the same way as type systems do but in different respects. It provides us with the information on how data are generated and consumed and thus the view of “data as resources”. It statically detects bugs resulting from ill-formed dataflow and advocates the “programming as wiring” paradigm. Well-modedness guarantees the safety of unification, the basic operation in concurrent logic programming. Information on the numbers of access paths to data can be obtained by slightly extending the framework, which can be used for compile-time garbage collection and the destructive update of structures.

    DOI

    Scopus

    4
    Citation
    (Scopus)

  • The Mode System of Moded Flat GHC

    Kazunori Ueda

    Guy E. Blelloch, K. Mani Chandy and Suresh Jagannathan (eds. ), Specification of Parallel Algorithms, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 18, American Mathematical Society     259 - 274  1994

  • Moded Flat GHC and Its Message-Oriented Implementation Technique

    Kazunori Ueda, Masao Morita

    New Generation Computing   13 ( 1 ) 3 - 43  1994  [Refereed]

    Authorship：Lead author

    　View Summary

    Concurrent processes can be used both for programming computation and for programming storage. Previous implementations of Flat GHC, however, have been tuned for computation-intensive programs, and perform poorly for storage-intensive programs (such as programs implementing reconfigurable data structures using processes and streams) and demand-driven programs. This paper proposes an optimization technique for programs in which processes are almost always suspended. The technique compiles unification for data transfer into message passing. Instead of reducing the number of process switching operations, the technique optimizes the cost of each process switching operation and reduces the number of cons operations for data buffering.
    The technique is based on a mode system which is powerful enough to analyze bidirectional communication and streams of streams. The mode system is based on mode constraints imposed by individual clauses rather than on global dataflow analysis, enabling separate analysis of program modules. The introduction of a mode system into Flat GHC effectively subsets Flat GHC; the resulting language is called Moded Flat GHC. Moded Flat GHC programs enjoy two important properties under certain conditions: (1) reduction of a goal clause retains the well-modedness of the clause, and (2) when execution terminates, all the variables in an initial goal clause will be bound to ground terms. Practically, the computational complexity of all-at-once mode analysis can be made almost linear with respect to the size n of the program and the complexity of the data structures used, and the complexity of separate analysis is higher only by O(log n) times.

  • Design and Evolution of the Concurrent Programming Language GHC

    早稲田大学理工学部紀要   57   1 - 16  1994  [Refereed]  [Invited]

  • Moded Flat GHC for Data-Parallel Programming

    Proc. FGCS'94 Workshop on Parallel Logic Programming, ICOT, Tokyo   27-35  1994  [Refereed]

    Authorship：Lead author

  • Message-Oriented Parallel Implementation of Moded Flat GHC

    K. Ueda, M. Morita

    New Generation Computing   11 ( 3-4 ) 323 - 341  1993  [Refereed]

    Authorship：Lead author

    　View Summary

    We proposed in Ref 5) a new, message-oriented implementation technique for Moded Flat GHC that compiled unification for data transfer into message passing. The technique was based on constraint-based program analysis, and significantly improved the performance of programs that used goals and streams to implement reconfigurable data structures. In this paper we discuss how the technique can be parallelized. We focus on a method for shared-memory multiprocessors, called the shared-goal method, though a different method could be used for distributed-memory multiprocessors. Unlike other parallel implementations of concurrent logic languages which we call process-oriented, the unit of parallel execution is not an individual goal but a chain of message sends caused successively by an initial message send. Parallelism comes from the existence of different chains of message sends that can be executed independently or in a pipelined manner. Mutual exclusion based on busy waiting and on message buffering controls access to individual, shared goals. Typical goals allow last-send optimization, the message-oriented counterpart of last-call optimization. We have built an experimental implementation on Sequent Symmetry. In spite of the simple scheduling currently adopted, preliminary evaluation shows good parallel speedup and good absolute performance for concurrent operations on binary process trees.

  • The Fifth Generation Project : Personal Perspectives

    Commun. ACM   36/3,65-76  1993  [Refereed]  [Invited]

  • 第五世代コンピュータ技術の開花と結実に向けて

    ICOTジャーナル   34/,40-68  1993

  • 理論と実際のギャップ:並列プログラミング

    情報処理   34/7,845-847  1993

  • 理論は実践を導けるか,実践は理論を生かせるか?

    情報処理   33/3,272-289  1992

  • Message-Oriented Parallel Implementation of Moded Flat GHC

    K. Ueda, M. Morita

    FIFTH GENERATION COMPUTER SYSTEMS 1992, VOLS 1 AND 2     799 - 808  1992  [Refereed]

    Authorship：Lead author

  • 並列論理型言語上の制約充足方式の比較

    YOKOO MAKOTO, UEDA KAZUNORI

    情報処理学会論文誌   32 ( 3 ) 296 - 303  1991  [Refereed]

    CiNii

  • Design of the Kernel Language for the Parallel Inference Machine

    K. Ueda, T. Chikayama

    Computer Journal   33 ( 6 ) 494 - 500  1990.12  [Refereed]

    　View Summary

    We review the design of the concurrent logic language GHC, the basis of the kernel language for the Parallel Inference Machine being developed in the Japanese Fifth Generation Computer Systems project, and the design of the parallel language KL1, the actual kernel language being implemented and used. The key idea in the design of these languages is the separation of concurrency and parallelism. Clarification of concepts of this kind seems to play an important role in bridging the gap between parallel inference systems and knowledge information processing in a coherent manner. In particular, design of a new kernel language has always encouraged us to re-examine and reorganise various existing notions related to programming and to invent new ones.

  • Designing a Concurrent Programming Language

    Proceedings of an International Conference organized by the IPSJ to Commemorate the 30th Anniversary (Into-Japan'90), Information Processing Society of Japan   87-94  1990  [Invited]

  • A New Implementation Technique for Flat GHC

    K. Ueda, M. Morita

    Logic Programming: Proceedings of the Seventh International Conference     3 - 17  1990  [Refereed]

    Authorship：Lead author

  • Theory and Practice of Concurrent Systems

    ICOT Journal, Institute for New Generation Computer Techmology, Tokyo   2-42  1989

  • 並列論理型言語GHCとそのプログラミング技術

    人工知能学会誌   4/3,258-264  1989

  • Parallelism in Logic Programming

    Kazunori Ueda

    Information Processing 89, Ritter, G. X. (ed. ), North-Holland     957 - 964  1989  [Refereed]  [Invited]

    Authorship：Lead author

  • Theory and Practice of Concurrent Systems

    ICOT Journal, Institute for New Generation Computer Techmology, Tokyo   /23,2-42  1989

  • 並列プログラミングとGHC

    bit   20 ( 10 ) 83 - 98  1988.10

  • Guarded Horn Clauses: A Parallel Logic Programming Language with the Concept of a Guard

    Kazunori Ueda

    Programming of Future Generation Computers, Nivat, M. and Fuchi, K. (eds. ), North-Holland, Amsterdam     441 - 456  1988.08

  • GHC - A Language for a New Age of Parallel Programming

    K. Furukawa, K. Ueda

    Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1988. Lecture Notes in Computer Science   338   364 - 376  1988  [Refereed]  [Invited]

  • Theory and Practice of Concurrent Systems : The Role of Kernel Language in the FGCS Project

    Proc. Int. Conf. on Fifth Generation Computer Systems 1988, ICOT   165-166  1988  [Invited]

  • Transformation Rules for GHC Programs

    Kazunori Ueda, Koichi Furukawa

    Proc. Int. Conf. on Fifth Generation Computer Systems 1988, ICOT, Tokyo   582-591  1988  [Refereed]

  • Guarded Horn Clauses(用語解説)

    人工知能学会誌   3/1,119  1988

  • Concurrent Prolog : Collected Papers (Volume1)

    The MIT Press, Cambridge, Mass. ,   /,140-156  1987

  • 並列プログラミング言語GHCの設計思想

    bit   19 ( 12 ) 4 - 14  1987

  • 並列プログラミングへのアプローチ

    上田 和紀

    通信工業   27/3,10-16  1987

  • Making Exhaustive Search Programs Deterministic

    K. Ueda

    New Generation Computing   5 ( 1 ) 29 - 44  1987  [Refereed]

  • Making Exhaustive Search Programs Deterministic, Part II

    Kazunori Ueda

    Proc. Fourth Int. Conf. on Logic Programming, The MIT Press, Cambridge, Mass.   356-375  1987  [Refereed]

  • 並列プログラミング

    情報処理   27 ( 9 ) 995 - 1004  1986.09  [Invited]  [Domestic journal]

    Authorship：Lead author, Corresponding author

  • Introduction to Guarded Horn Clauses

    Kazunori Ueda

    NEC Research and Development   84   6 - 13  1986

  • Guarded Horn Clauses

    Kazunori Ueda

    Logic Programming '85. LP 1985. Lecture Notes in Computer Science   221   168 - 179  1986  [Refereed]

    　View Summary

    A set of Horn clauses, augmented with a ‘guard’ mechanism, is shown to be a simple and yet powerful parallel logic programming language.

    DOI

    Scopus

    56
    Citation
    (Scopus)

  • Guarded Horn Clauses and Experiences with Parallel Logic Programming

    Tanaka, Jiro, Ueda, Kazunori, Miyazaki, Toshihiko, Takeuchi, Akikazu, Matsumoto, Yuji, Furukawa, Koichi

    1986 Proc. Fall Joint Computer Conferences, IEEE Computer Society   948-954  1986

  • Guarded Horn Clauses

    Kazunori Ueda

    D.Eng. Thesis, University of Tokyo    1986

  • Making Exhaustive Search Programs Deterministic

    Kazunori Ueda

    Third International Conference on Logic Programming. ICLP 1986. Lecture Notes in Computer Science   225   270 - 282  1986  [Refereed]

    Authorship：Lead author

    DOI

    Scopus

    7
    Citation
    (Scopus)

  • Concurrent Prolog Compiler on Top of Prolog

    Proc. 1985 Symp. on Logic Programming, IEEE Computger Society   119-126  1985  [Refereed]

  • Mandala : A Logic Based Knowledge Programming System

    Koichi Furukawa, Akikazu Takeuchi, Susumu Kunifuji, Hideki Yasukawa, Masaru Ohki, Kazunori Ueda

    Proc. Int. Conf. on Fifth Generation Computer Systems ICOT, Tokyo     613 - 622  1984  [Refereed]

    　View Summary

    Mandala is a programming system aimed for developing knowledge information processing systems in logic programming framework. It is not only a knowledge programming system but also a basis for a knowledge base management system. The nature of this duality comes directly from two-facedness of logic programming, that is, both procedural and declarative interpretation. Mandala provides users with parallel execution environment, allowing them to describe multiple-processes. On this parallel execution environment, cooperative problem solving systems can be constructed, in which more than one problem solver can be active in parallel. Mandala realizes object oriented programming using a process mechanism in KL1, thus manipulating dynamically changing states. Objects in Mandala can be seen as problem solvers which have inference engines and knowledge base.

  • What Is a Variable in Prolog?

    Nakashima, H, Tomura, S, Ueda, K

    Proc. Int. Conf. on Fifth Generation Computer Systems 1984, ICOT, Tokyo     327 - 332  1984  [Refereed]

  • Efficient Stream/Array Processing in Logic Programming Languages

    Kazunori Ueda, Takashi Chikayama

    Proc. Int. Conf. on Fifth Generation Computer Systems 1984, ICOT, Tokyo     317 - 326  1984  [Refereed]

  • 述語論理型言語における副作用によらない入出力と文字列操作

    NAKASHIMA HIDEYUKI, UEDA KAZUNORI, TOMURA SATORU

    情報処理学会論文誌   24 ( 6 ) 745 - 753  1983  [Refereed]

    CiNii

  • Binary Decision Treeによる多重分光画像の高速処理

    計測自動制御学会論文集   5/4,486-491  1979  [Refereed]

▼display all

Books and Other Publications

  • AI事典 第3版

    ( Part： Contributor, 1.2「第五世代コンピュータ」(pp.4-5))

    近代科学社  2019.12

  • 人工知能学大事典

    ( Part： Contributor, 5-12「論理プログラミング」(pp.243-244))

    共立出版  2017.07

  • Programming Languages and Systems 8th Asian Symposium, APLAS 2010

    Kazunori Ueda (ed.)

    Lecture Notes in Computer Science 6461, Springer-Verlag  2010

  • 人工知能学事典

    人工知能学会編

    共立出版  2005.12

  • Functional and Logic Programming-5th International Symposium on Functional and Logic Programming, FLOPS 2001

    Lecture Notes in Computer Science 2024, Springer-Verlag  2001

  • Advances in Computing Science: ASIAN '97

    Lecture Notes in Computer Science 1345, Springer-Verlag  1997

  • 並列処理シンポジウムJSPP'97論文集

    情報処理学会  1997

  • 楽しいプログラミング：記号の世界

    中島秀之, 上田和紀

    岩波書店  1992

  • Logic Programming : Proceedings of the 1991 International Symposium

    The MIT Press  1991

  • 続・新しいプログラミング・パラダイム

    井田哲雄, 田中二郎編, 上田和紀他共著( Part： Joint author, 第1章 "並行プログラミングとGHC" (pp.1-34))

    1990.11

  • 知的コンピュータシステム事典

    ( Part： Contributor, 2.1.4(1) 「Concurrencyと並列性」)

    産業調査会 事典出版センター  1989.08

  • 並列論理型言語GHCとその応用

    淵一博監修, 古川康一, 溝口文雄共編, 古川康一, 竹内彰一, 上田和紀, 他, 名共著( Part： Joint author, 第3章 "GHCの基本" (pp.33-66)，第5章 "GHCによる全解探索" (pp.93-115)，付録 "GHCのProlog上の処理系" (pp.217-270))

    1987.09

  • プログラム言語 Ada: 基準文法書解説

    上田 和紀( Part： Joint author, pp.87-128)

    bit 臨時増刊，共立出版  1981.10

▼display all

Works

  • 制約概念に基づくハイブリッドシステムモデリング言語HydLa

    Software 

    2010
    -
    Now

  • LMNtal: モデル検査機能と可視化環境を備えた階層グラフ書換え言語処理系

    Software 

    2002
    -
    Now

Presentations

  • 言語をつくる

     [Invited]

    日本ソフトウェア科学会第35回大会 (August 29-31, 2018, 大阪大学) 

    Presentation date： 2018.08

  • Logic/Constraint Programming and Concurrency: The Hard-Won Lessons of the Fifth Generation Computer Project

     [Invited]

    Thirteenth International Symposium on Functional and Logic Programming (FLOPS 2016, March 4-6, 2016, Kochi, Japan) 

    Presentation date： 2016.03

  • Hierarchical graph rewriting as a unifying model and language of concurrency

     [Invited]

    LIX Colloquium on Emerging Trends in Concurrency Theory (November 2006, Ecole Polytechnique de Paris, France) 

    Presentation date： 2006.11

  • LMNtal: a unifying declarative language

     [Invited]

    Third Workshop on Constraint Handling Rules (CHR 2006, July 2006, Venice, Italy) 

    Presentation date： 2006.07

  • Constraint-Based Concurrency and Beyond

     [Invited]

    Algebraic Process Calculi: The First Twenty Five Years and Beyond (August 1-5, 2005, Bertinoro, Italy) 

    Presentation date： 2005

  • LMNtal: a language model with links and membranes

     [Invited]

    Fifth Workshop on Membrane Computing (WMC5, June 2004, Milano, Italy) 

    Presentation date： 2004.06

  • Resource-Passing Concurrent Programming (advanced tutorial)

     [Invited]

    Seventeenth International Conference on Logic Programming (ICLP'01, Novermber-December 2001, Paphos, Cyprus) 

    Presentation date： 2001.11

  • Resource-Passing Concurrent Programming

     [Invited]

    Fourth International Symposium on Theoretical Aspects of Computer Software (TACS 2001, October 2001, Sendai, Japan) 

    Presentation date： 2001.10

  • Strong Moding in Concurrent Logic/Constraint Programming (advanced tutorial)

     [Invited]

    Twelfth International Conference on Logic Programming (ICLP'95, June 1995, Kanagawa, Japan) 

    Presentation date： 1995.06

  • Designing a Concurrent Programming Language

     [Invited]

    International Conference organized by the IPSJ to Commemorate the 30th Anniversary (InfoJapan'90, October 1990, Tokyo, Japan) 

    Presentation date： 1990.10

  • Paralleism in Logic Programming

     [Invited]

    IFIP 11th World Computer Congress 

    Presentation date： 1989.08

  • Theory and Practice of Concurrent Systems (panel)

    Ehud Shapiro, William J. Dally, Geoffrey C. Fox, Carl Hewitt, Robin Milner, Kazunori Ueda, David H.D. Warren  [Invited]

    International Conference on Fifth Generation Computer Systems 1988 (FGCS'88, November 1988, Tokyo, Japan) 

    Presentation date： 1988.11

  • Concurrent Logic Programming Languages (tutorial)

     [Invited]

    Fourth International Conference on Logic Programming (ICLP'87, May 1987, Melborne, Australia) 

    Presentation date： 1987

  • Guarded Horn Clauses

     [Invited]

    Workshop on Foundations of Logic and Functional Programming (December 1986, Trento, Italy) 

    Presentation date： 1986.12

  • Teaching (Constraint) Logic Programming

    G. Gupta, M.V. Hermenegildo, U. Nillson, P. Stuckey, K. Ueda  [Invited]

    Ninteenth International Conference on Logic Programming (ICLP'03, December 2003, Mumbai, India) 

    Presentation date： 2003.12

  • The Future of Logic Programming (panel)

    International Logic Programming Symposium (ILPS'91, San Diego, U.S.A.) 

    Presentation date： 1991.11

▼display all

Research Projects

  • 強力なデータ構造と並行性をもつ高水準言語の解析・実装技法の多面的開拓

    日本学術振興会  科学研究費助成事業

    Project Year :

    2023.04
    -
    2026.03
     

    上田 和紀, 山本 直輝

  • 先進的プログラム構築方法論に支えられた高機能な3D印刷造形技術の開拓

    科学研究費挑戦的研究（萌芽）

    Project Year :

    2018.06
    -
    2021.03
     

    　View Summary

    初年度は，熱可塑性樹脂を用いた積層型3D印刷による高機能造形物実現のための基礎固めを目標に，以下の研究開発（一部準備作業を含む）を実施した。<BR>(1) 3Dプリンタ，樹脂素材，スライサの特性理解: 開発する技術の再現性の担保のためには，ハードウェア，材料，ソフトウェアの三者それぞれについて利用経験を積み，特性ないし癖を把握してノウハウを蓄積することが重要である。そこで，現有の3Dプリンタ１機種３台に加えて２機種４台を新たに導入し組み立てるとともに，数種類のスライサソフトウェアと多様な材料で多くの印刷実験を行った。またこれを通じて，素材および造形物の強度，サポート材なしの印刷におけるブリッジ耐性やオーバーハング耐性などについての検討を進めた。これを通じて，目標として掲げていた「適切な部材組合せに必要な0.05mm前後の寸法精度の安定確保」の見通しを得た。(2) 機能部品の設計技術: 3D印刷の部品化概念の開拓の第一歩として，梁のような細長い部品を強固に相互接続する方法の実験的検討を進めた。日本の伝統建築に見られる継手の中から，主に追掛け大栓継ぎと尻掛け継ぎの超小型版について試作を重ね，断面が3mm×6mm程度の部材でも十分強固に接続できる見通しを得た。また，3D積層印刷による弾性機能実現にとって有利な形状とは言えないコイルばねの印刷について，実用性確認のための基礎実験を重ねた。<BR>研究代表者自身による上記の実験に加え，機械工学を専門とする研究協力者および大学院生との定期的な会合を設け，通常の積層にとどまらないさまざまな技法について検討および情報交換を行った。また3D印刷の展示会の参加等を通じて最新技術の調査を行った。７月からの研究は実験設備の導入，組み立て，整備から始まったため，実質的な研究期間は限られていたが，その中で機械と材料についての知見とノウハウの蓄積を進めることを最優先に研究を進めた。現場的な観点からの経験は深まったが，これを工学につなげるのはこれからである。<BR>当初想定していなかった知見として，既存の数種類のスライサソフトウェアの機能とその限界を知ることができた。つまり，通常のスライサは多様なパラメタ設定が可能であるが，3Dプリンタの制御を自由にプログラムすることはできない。このことから，高度な3D印刷のためのソフトウェア開発は，印刷物表現の標準形式であるSTLではなく，3Dプリンタの制御言語であるGコードをインタフェースとして進める必要があるとの知見を得た。当初の研究計画のとおり，機能部品の設計技術よび部品の組合せ技術を中心とした研究開発を進めるが，以下の点に留意する。<BR>1. 第一年度に得られた上記の知見に基づき，ソフトウェアについては，低レイヤすなわちGコードレベルの技術の調査および開拓を優先させる。2. 2次元印刷をZ軸方向にヘッドを単調移動させながら繰り返すという従来手法とらわれずに，真の3次元印刷技術の可能性の探求に着手する。3. ソフトウェア技術の開拓を行いつつ，得られた知見のデータベースの作成にも取り組む

  • プログラミング言語技術との融合による高水準モデリング言語の進化と展開

    科学研究費基盤研究（Ｂ）

    Project Year :

    2018.04
    -
    2021.03
     

    　View Summary

    プログラミング言語技術との融合による高水準モデリング言語とその処理系の進化を目標に，グラフ構造を扱うLMNtalおよび実数を扱うHydLaの二つのモデリング言語について以下の研究開発を実施した。<BR>グラフ書換え言語LMNtalについて，以下の新言語機能の設計と実装を行った。(1)全称量化子を伴うグラフパターンマッチングの意味論を定め，仮想機械での実装を実現し例題記述を行った。(2)λ計算の簡約を簡潔に記述するための新たなグラフ型を提案し実装した。(3)モデル検査における並行プロセスの自動抽象化技法能を提案し，正当性を証明し実装を行った。また正当性証明のためにLMNtalの操作的意味論の検討と整備を行った。(4)LMNtalグラフの既存の型概念を検討して再定式化を行った。(5)グラフのための内包表記の検討を進めた。(6)非決定実行インタプリタの記述を可能にするAPIを定めて公開した。LMNtal実行・検証系については，集中作業合宿を実施してC++化による可読性・保守性の改善作業を行うとともに，LMNtalモデル検査器の要素技術となるグラフ差分を利用した効率的グラフ正規化技法の処理系への組み込みを進めた。<BR>制約概念に基づくハイブリッドシステムモデリング言語HydLaについては，言語機能と実装技法について以下の研究開発を行った。(1)変数および制約階層の動的生成のための記法を定めて実装を行った。(2)シミュレーション中の制約処理過程を動的に解析して再利用する技法の開発を行った。(3)モデル抽象化技法を実行性能改善に応用する技法を開拓した。(4)記号パラメタをもつ非線形常微分方程式の精度保証近似解法の開発と評価を行った。(5)微分代数方程式の求解性能向上方法の検討を進めた。(6)集中検討合宿を行って，オープンソース制約エンジンの有力候補となるSageMathの評価検討を行った。研究開発のコアとなる二つのモデリング言語の言語機能と実装技法について，多岐にわたる要素技術の開拓を進めることができた。これには，年度末時点では設計の詰めの段階で初回の学会発表を行ったばかりのものも一部含まれるが，多くは試験実装を経て評価・改良中，またはGithubで公開中の処理系の主たるブランチにすでに反映済みである。<BR>研究分担者および連携研究者との交流も進め，フランス・ナント大学の制約プログラミング研究グループとも相互訪問を行った。プログラミングおよびモデリング言語の研究開発における理論と実践の強い連携という基本方針に基づいて，育ってきた要素技術を発展させてGithubから公開中のモデリング言語実行・検証系に統合する作業を推進する。<BR>LMNtalとその処理系については，(1)言語機能としてほぼ確立できた高階概念の本格実装および応用の展開，(2)グラフのための強力な型体系の，グラフの型検査からグラフ書換え規則の型検査への発展，(3)全称量化グラフパターンにマッチしたグラフの書き換えのための構文，意味論，実装の整備，などを進める。<BR>HydLaとその処理系については，特に(1)処理系の基礎をなす操作的意味論と言語仕様の根幹をなす宣言的意味論の整合性の検討，(2)プログラムの等価性のより深い検討およびそれを支える精密な意味論の整備，(3)プログラム変換技法の開発とその実行最適化への応用，(4)制約エンジンの求解能力および性能向上，などを進める

  • General-purpose high-level language with the notion of real numbers and time

    Project Year :

    2015.04
    -
    2018.03
     

    　View Summary

    Towards the foundations for computing and programming of cyber-physical systems, we studied language constructs and semantics of general-purpose high-level programming languages that allow us to represent and handle continuous quantities and the notion of time. Our working hypothesis was that those languages should be concurrent programming languages featuring concurrency and communication and, at the same time, be constraint programming languages featuring continuous quantities and uncertainties. Through detailed study of existing languages, we clarified many of theoretical foundations and necessary language constructs, including (i) constraint hierarchies and its semantics, (ii) the notion of time, (iii) data domain, and (iv) description of dynamically evolving concurrent systems

  • Deepening the implemenation technology of high-level modeling language implementations integrated with verifiers

    Project Year :

    2014.04
    -
    2017.03
     

    　View Summary

    The goal of this research was to deepen the implementation technology of high-level modeling languages that support highly abstract and general data representation such as real numbers and graph structures. To achieve reliable simulation of hybrid systems that make both continuous and discrete changes, we developed various techniques including a method for integrating numerical computation with guaranteed accuracy and symbolic computation, and greatly improved the solution capability and performance of the symbolic simulator of the constraint-based modeling language HydLa. For the runtime system of the graph-rewriting modeling language LMNtal, a number of new techniques were developed, e.g., for expressive hypergraph rewriting and efficient parallel model checking, and the system was evolved into a more powerful verification tool. The developed implementations were made publicly available as open-source software

  • Evolutionary development of a model checker compiler using verification technology and non-standard type systems

    Project Year :

    2012.04
    -
    2015.03
     

    　View Summary

    Modeling and verification of various systems are expected to be important applications of non-procedural high-level languages. The Principal Investigator has long worked on the design and implementation of a modeling language based on graph rewriting that supports ordinary execution and model checking in a unified framework, but the evolution and verification of its compiler has been recognized as a challenging issue. In this study, we formalized and verified graph rewriting operations performed by the abstract machine that is the interface between the compiler and the runtime, and made a step towards the verification of a graph rewriting compiler. Also, we established novel type systems for the graph rewriting language that will help the analysis, understanding and compiler optimization of models. One of them handles microscopic connectivity of graphs and hypergraphs, while the other handles the global shape of graphs

  • Implementations of high-level modeling languages that integrate high-performance verifiers

    Project Year :

    2011.04
    -
    2014.03
     

    　View Summary

    Modeling and verification technologies of natural, symbolic and cyber-physical systems are becoming increasingly important. The aim of this research was to demonstrate the viability of high-level modeling languages based on mathematical notions such as graphs, sets, equations and inequations whose generality goes far beyond Computer Science. To achieve this goal, we constructed two publicly available language implementations that integrate runtime systems and verifiers. One of them is an implementation of the graph rewriting language LMNtal, which has now evolved into a parallel model checker with hypergraph rewriting capabilities; the other is an implementation of the hybrid constraint language HydLa, which has evolved into a non-deterministic symbolic execution system for hybrid systems with uncertainties

  • Study of SAT-based constraint optimization problem solving and its parallel distributed processing

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research

    Project Year :

    2008
    -
    2012
     

    TAMURA Naoyuki, BANBARA Mutsunori, HIRAYAMA Katsutoshi, INOUE Katsumi, IWANUMA Koji, NABESHIMA Hidetomo, YAMAMOTO Yoshitaka, YOKOO Makoto, HASEGAWA Ryuzo, FUJITA Hiroshi, KISHIMURA Miyuki, UEDA Kazunori

    　View Summary

    We conducted the research on SAT technologies for Constraint Satisfaction and Optimization Problems and their parallel/distributed implementations, and published 105 refereed papers and made 67 presentations. In addition, world's leading softwares were developed including a SAT-based CSP/COP solver Sugar which won at the 2008 and 2009 CSP Solver Competitions in global constraint categories, a CDCL type SAT solver GlueMiniSat which won at the 2011 SAT Competition in Applications UNSAT category, and a partial Max-SAT solver QMaxSAT which won at the 2010 and 2011 Max-SAT evaluation in Application category

  • High-level hybrid constraint modeling language and its reliable implementation

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research

    Project Year :

    2008
    -
    2011
     

    UEDA Kazunori, ISHII Daisuke, HOSOBE Hiroshi

    　View Summary

    We have designed a high-level modeling language HydLa for the reliable simulation and verification of hybrid systems that involve both continuous and discrete changes, and established its declarative semantics and an execution algorithm. Features of HydLa include (i) declarative description employing well-established mathematical and logical notations, (ii) the use of constraints to represent and handle uncertain information, and (iii) constraint hierarchies to allow concise description. We have also established an interval-based solution algorithm of discrete changes to guarantee the correctness of simulation and verification in the existence of uncertain information, and built a prototype integrated implementation equipped with main features of HydLa

  • Highly Scalable Software Construction Basis for Information Explosion Era

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research

    Project Year :

    2006
    -
    2011
     

    CHIKAYAMA Takashi, YUASA Taiichi, UEDA Kazunori, TAURA Kenjiro, ENDO Toshio, YOKOYAMA Daisaku, UMATANI Seiji

    　View Summary

    To cope with the explosive increase of data amount, frameworks for flexible description of software for widely distributed highly parallel information systems are required. For this purpose, programming languages, middleware systems, and veri-fication systems for highly complicated software have been investigated, and such systems have been proposed, designed, implemented and evaluated the performance. Represent-ative resultant software systems are made open to public

  • 計算機科学における離散と連続に関する調査と新しい展開

    科学研究費基盤研究（Ｃ）

    Project Year :

    2006
    -
    2007
     

    　View Summary

    特定領域研究を申請するために3回の会議を開催した。5月27日には名古屋で「自然計算における離散と連続」、7月15日には東京で「自然計算における理論と実証」、9月2日には東京で「申請に向けて」、である。特定領域研究「自然計算--構成的アプローチの実証とその理論--」を11月に無事に申請した。さらに、今後のこの分野を概観するための第4回会議を3月24日に東京で開催した。本基盤研究(C)の成果の第1は特定領域研究「自然計算--構成的アプローチの実証とその理論--」の企画・申請である。次に、基盤研究(C)を申請した段階では、自然計算を理解する問題を離散と連続の間の問題であると矮小に捕らえていたのだが、特定領域研究の申請段階では、ハイブリッド的確率的多体的システムに対する計算論として自然計算を理解するようになった。これが、基盤(C)の調査研究としての側面の具体的な成果である。現存しないハイブリッド的確率的多体的システムの計算論の必要性を、構成的材料工学と合成生物学に対する応用と新しい理論情報科学分野の開拓という両面から訴えたのが特定領域研究「自然計算--構成的アプローチの実証とその理論--」である。離散性と連続性の問題であるハイブリッド性の他に、自然の持つ揺らぎと超分散性を自然計算の基本要素であると理解し、これらの性質を持つシステム上の計算論の構築とその応用を研究分野として申請した

  • 構造的分子計算理論-自律的計算系の解析と設計のための基礎理論

    科学研究費特定領域研究

    Project Year :

    2006
    -
    2007
     

    　View Summary

    (1)膜計算モデルにおける新しい計算モデルの提案:神経細胞系をモデルとして,膜計算の新しいモデル「Spiking Neural P-Systems」を提案し,受理器と生成器の両タイプにおいてその計算能力の万能性を示した。
    (2)平衡状態の効率の良い計算手法の開発:入力分子のサイズに比して会合の結果生成される分子複合体の個数が組合せ論的な爆発をするような反応系に対して,平衡状態を計算するための一般論を構築した。平衡状態計算を系全体の自由エネルギーの最小化問題として定式化し,変数の個数を著しく削減する新しいアルゴリズムを開発した。
    (3)細胞並列計算に向けたバクテリアセルオートマトンの実装:細胞を用いたセルオートマトンの実現に向けての第一歩として,細胞内分子反応メカニズムを用いて自律的でプログラム可能なバクテリアコンピュータを開発した。これは世界で初めてバクテリアを用いて計算が実行できたことを証明するものである。
    (4)抽象化学反応計算モデルの研究:微分方程式系などでは解析が困難な少数分子の化学反応系の振る舞いについて計算機実験と数理的解析により検討し,特にBelousov-Zhabotinsk (BZ)反応の数理モデルであるBrruselatorとOregonatorについて,分子数が少数になることによる不安定性について解析した。
    (5)分子計算シミュレータ:階層構造と接続構造の両方を扱う階層グラフ書換えモデルLMNtalの表現力検証のために,代表的計算モデルのエンコード法の確立と実装を行った。Ambient計算のエンコードにおいては自己調整に基づく分散名前管理方式を実現した。純粋λ計算のエンコードにおいては,膜を活用することで従来手法よりもはるかに簡潔な方法を実現した。

  • Putting Scalable and Unifying Programming Language Model LMNtal into Practical Use

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research

    Project Year :

    2004
    -
    2007
     

    UEDA Kazunori, KATO Norio

    　View Summary

    LMNtal is a language model developed by the grantees to unify various computational models featuring multiset rewriting, concurrency and mobility in a concise setting. The purpose of the project has been to grow LMNtal from a hierarchical graph rewriting model to a practical programming language by designing necessary language constructs, establishing implementation techniques, building a full-fledged LMNtal system, and making it widely available.The main results of the project are as follows :(a) Establishing LMNtal as a programming language-we have studied and designed how to incorporate basic datatypes and operations, a module system, and foreign-language interface into hierarchical graph rewriting, and built a diverse range of libraries using them.(b) Establishing implementation techniques and building a full-fledged system-we have built a compiler from LMNtal into dedicated intermediate code and a runtime system that runs the intermediate code. In particular, we have designed and implemented asynchronous execution scheme that uses multiple tasks, an optimizer for individual tasks, and a translator from intermediate code into Java. We have also designed and implemented a visualizer featuring automatic graph drawing.(c) Verifying the expressive power-in order to see if LMNtal is powerful enough to express fundamental concepts in computation, we have encoded diverse computational models including the pi-calculus, the ambient calculus, the lambda calculus and CHR(Constraint Handling Rules), and ran them on our LMNtal system.The LMNtal system we have developed consists of about 50,000 lines of code, and is available via http://www.ueda.info.waseda.ac.jp/lmtal/

  • 構造的分子計算理論-自律的計算系の解析と設計のための基礎理論

    科学研究費特定領域研究

    Project Year :

    2002
    -
    2006
     

  • Software Development based on Continuous Computing Resources

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research

    Project Year :

    2001
    -
    2006
     

    YUASA Taiichi, CHIKAYAMA Takashi, UEDA Kazunori, MORI Shinichiro, YASUGI Masahiro, KOMIYA Tsuneyasu

    　View Summary

    In order to make it possible to construct complexity analysis models and software systems that can cope with both extent and locality of computer systems, we have been working to revisit, unify and develop existing computation concepts from various points of view, based on the notion of Continuous Computing Resources. The major outcomes of this project are the following.1. Complexity Analysis based on Continuous Computing Resource: We proposed a computation model that can uniformly and concisely express various concepts of computation from the memory hierarchy of a single computer to network delay among computers. We showed that complexity analysis results based on this model reflect real computation more precisely than previous models. In order to make it easier to understand the behavior of sophisticated parallel algorithms, we designed a virtual machine of the model and implemented language systems including simulators and visualizers.2. Concurrent Language Model LMNtal: We designed LMNTal (pronounced as "elemental"), a scalable language model for concurrent computation based on hierarchical graph reduction. On this model, we have established techniques for process structure analysis and implemented this model as realistic and useful programming languages. Since hierarchical graph reduction includes a variety of computation models such as multi-set rewriting models and self-organizing models, it is expected that our results will be useful as a bridge between existing computation models.3. Language Implementation based on Locality: We showed that runtime efficiency of programming language systems can be remarkably improved by focusing on locality. A typical example is the locality improvement by the use of copying garbage collection based on "hierarchical clustering of data objects". This technique is proposed by further improving the existing technique where live objects are copied in depth-first order, with a small stack area and additionally with a queue that is used in case of stack overflow. This technique improves not only the locality in the virtual memory, but also the locality in the CPU cache, and thus allows high performance implementations on real computer systems

  • Wide-Area and Distributed Computation Paradigm Based on Concurrent Logic Programming

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research

    Project Year :

    1999
    -
    2002
     

    UEDA Kazunori

    　View Summary

    Concurrent logic languages provide natural mechanisms for describing concurrent computation by introducing dataflow synchronization on single-assignment variables. Previous work on concurrent logic programming focused on efficient parallel computation. Our research, in contrast, focused on distributed, wide-area computation and studied (1) declarative programming under non-uniform computational environments and (2) static analysis for safe distributed programs. Our results can be summarized as follows :1. Seamless distributed implementation - We designed and implemented network-transparent distributed logical variables (single-assignment channels) to transparently interconnect KL1 programs running on non-uniform computational nodes using sockets. We also designed naming service used for the naming and resolution of distributed logical variables. An exception handling mechanism was also designed and implemented.2. Resource management under distributed environments - We designed and implemented a linear type system for concurrent logic programs that statically analyzes data sharing by logical variables. Furthemore, we proposed a novel view of concurrent computation in terms of resource passing, and designed a capability type system that unifies and generalizes mode systems and linearity systems.3. Interpreter technology for code mobility - We designed an intermediate code, called treecode, to realize code mobility between non-uniform nodes, and described its interpreter using Flat GHC

  • Research on Methodologies for Constructing Evolutionary Software

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research

    Project Year :

    1997
    -
    2000
     

    MIYAMOTO Eiichi, TAMAI Tetsuo, UEDA Kazunori, ARAKI Keijiro, TOGASHI Atsushi, FUTATSUGI Kokichi

    　View Summary

    1. We have developed a communication model which does not point particular receivers, which has enabled to evolve software in open and distributed systems efficiently.2. We measured source programs of objects, and extracted evolutional patterns in which line and method numbers in classes obey the negative diadic distribution.3. We made specifications into modules using the Algebraic specification language CafeOBJ, and then constructed the overall specification by synthesizing them. We also classified composite patterns into reusable one.4. By case studies, we analyzed the processes of model formation and construction and description of formal specification, reviewed features and meaning of formal specification description in evolutional processes of the description of system specifications.5. Based on strong mode systems in concurrent logic programming, we identified slight errors without specifications, and proposed a framework which corrects errors automatically.6. We defined system requirements based on propositon and predicate, proposed a method to convert them into formal specification, and proved its soundness and completeness.7. We developed a language to describe multi-agent systems which work in the environment of multi-processes and multi-threads and have migration facilities.8. We proposed "programming on cell" and "active programming" based π calculus and developed an exensible Java LSI processor to implement efficient programs.9. We analyzed the features of distributed data structures from the several different views and developed an efficient implementation for them

  • Architecture and Software for Real-time Access to Global Information

    Project Year :

    1997
    -
    2000
     

  • Applications of Strong Moding in Concurrent Logic Programming

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research

    Project Year :

    1995
    -
    1998
     

    UEDA Kazunori

    　View Summary

    The outstanding features of concurrent logic programming languages such as GHC (Guarded Horn Clauses) are the extreme simplicity of its communication and synchronization mechanisms and its flexibility in describing concurrency. To make the languages really practical, however, static analysis needs to play key roles both in programming and optimization.The head investigator had worked on the theoretical aspects of the static mode system (strong moding) for GHC and designed the algorithms for mode analysis. In this project, we worked on the practical aspects of strong moding and demonstrated its effectiveness from the following respects :1. Implementation of a mode analyzer - We implemented the mode analyzer klint for the concurrent logic language KL1 using KL1 itself as an implementation language. The system was revised several times until it could process large, real-life programs.2. Descriptive power under strong moding - We demonstrated, through the analysis of various real-life Eli programs, that concurrent logic languages with strong moding are as practical and expressive as those without strong moding.3. Program diagnosis based on strong moding - Strong moding turned out to be extremely useful for the static detection of program errors. We designed and implemented a set of algorithms for analyzing the errors of non-well-moded programs efficiently. Furthermore, we proposed a method of automated error correction and showed that it worked quite well for small program errors.4. Optimization based on strong moding - We demonstrated that, by using type and linearity information in addition to mode information, many of runtime operations such as tag checking could be eliminated, leading to performance not too different from that obtained by procedural programs

  • Integrated Parallel Processing

    Project Year :

    1996
    -
    1997
     

▼display all

Misc

▼display all

 

Syllabus

▼display all

 

Overseas Activities

  • 並行制約プログラミングに基づく広域分散計算パラダイムの構築

    2000.09
    -
    2001.02

    シンガポール   シンガポール国立大学

Sub-affiliation

  • Faculty of Science and Engineering   Graduate School of Fundamental Science and Engineering

Research Institute

  • 2024
    -
    2026

    Waseda Research Institute for Science and Engineering   Concurrent Researcher

Internal Special Research Projects

  • 強力なデータ構造と並行性をもつ高水準言語の表現力強化

    2024   山本直輝

    　View Summary

    本研究では，高い汎用性をもちながら通常のプログラミング言語が直接サポートしないグラフ構造を扱う高水準言語として研究開発を推進しているLMNtal言語の機能深化に取り組み，以下の成果を得た．1. プログラミング言語において重要な役割を演じるグラフ型の概念の新たな定式化を行った．特に，グラフ構造の一部（部分グラフ）に対して型を付与するための差分型概念を定義し，それが効率的な静的型検査を可能にすることを示すとともに，ユーザ定義可能な強力なグラフパターンマッチングに応用できることを示した．2. モデリング言語の観点からは，既存のLMNtalのグラフマッチング機能を格段に強化すべく，(i) マッチングを抑止する否定条件，および (ii) 不特定多数のサブグラフに対する同時パターンマッチングと書換えを可能にする量化パターンの概念を統合的に扱うための構文と意味論を定義した．また，定義した意味論を実現するためのLMNtal仮想機械命令の設計と実装を行い，並行計算や量子計算を含む複数の例題を用いて，記述力確認と処理系上での動作確認を行った．3. さらに，グラフ書換え概念が論理学，特に線形論理のProof Netsと密接な関係を持つことに着目して，既存のLMNtalがもつ膜概念とProof NetsがもつBox概念の関係を綿密に検討した．これを通じて，LMNtalの既存の膜操作機能の拡張を言語仕様および実装に対して行い，線形論理の重要な断片であるMELL (Multiplicative Exponential Linear Logic) の証明およびカット除去操作がLMNtalで簡潔にエンコードできることを示した．以上の研究開発を通じて，LMNtal言語と複数の隣接分野とのつながりを格段に強化することができた．

  • 強力なデータ構造と並行性をもつ高水準言語の解析・実装技法の開拓

    2023  

    　View Summary

    本研究では，高い汎用性をもちながら通常の高水準言語が直接サポートしないグラフ構造を扱うプログラミング言語・モデリング言語のための新たな解析・実装技術の開拓に取り組んだ．対象言語として，階層グラフ書換え言語LMNtal，およびLMNtalのデータ構造をハイパーグラフに拡張したHyperLMNtalをとりあげた．解析技術については，通常の代数的データ型の範疇を超えるグラフ型の枠組みに対して，型の概念設計および解析の両面から検討を進めた．型の概念設計においては，グラフの書換え規則の型安全性検査を大幅に軽量化する型の差分概念を提案し，型の差分に基づく解析手法の構築を進めた．また，与えられたグラフが型の生成文法から生成できるかどうかの判定にtoken passingの考え方を導入するとともに，tokenの概念を拡張することで，threaded treeのような複雑なグラフ構造の解析が効率良くできることを示した．実装技術については，まず，木構造よりも低い結合度をもつ非連結グラフ構造も重要な用途をもつことから，非連結構造の書換えの実装最適化に取り組んだ．非連結構造の典型応用はタプルの多重集合の書換えだが，連結グラフのように辺を辿る探索ができないため探索に工夫が必要である．そこで，単調非減少な書換えルールに対して効率的に動作しかつC++等に変換可能なタプル書換えアルゴリズムを提案・評価した．索引構造をはじめとするさまざまな工夫によって，計測例題に対して1000倍以上の高速化に成功した．また，再帰的生成規則で定義したグラフパターンのマッチング機能を備えたCSLMNtal言語について，プログラムの実行過程で繰り返されるパターンマッチングを素朴に実装した場合に発生する重複作業を削減するマッチングアルゴリズムを設計し，実際に計算量が改善されることを確認した．

  • 汎用かつ強力なデータ構造と実行機能をもつ高水準言語の基礎研究

    2022   山本直輝

    　View Summary

    複雑な接続関係とその変化をグラフ構造とその書換え作業として表現する能力は，プログラミング言語とモデリング言語の双方にとって重要である．しかしこれまでの言語では，リストや木構造よりも複雑な構造の簡潔な表現と安全な操作，それらを支える型体系の開拓が不十分であった．本研究では，グラフ書換え言語LMNtalのためのグラフ型概念およびグラフ型検査の枠組みを構築して，その性質を多角的に検討した．最大の特徴は，グラフの型を表現する生成文法をLMNtalの書換え規則の形で表現する点にある．構築した型検査アルゴリズムを実装して，さまざまなグラフ構造に対する実際的な操作の型検査が可能であることを示した．

  • 高水準モデリング言語の高機能な実行・検証系

    2022  

    　View Summary

    プログラミングにおいてグラフ構造は強力で一般性の高いデータ構造である．グラフ構造は命令型言語ではヒープ上のポインタ構造に対する破壊的代入として扱われるが，その正当性検証は容易でない．一方，純粋関数型言語で一般のグラフ構造を扱う方法は未確立であった．そこで本研究では，新たな純粋関数型言語λGTの設計を行い，概念実証のための処理系を構築した．λGTはグラフをimmutableな第一級データ構造として表現し，グラフ変換計算モデルに基づくパターンマッチングによって分解合成を行う．λGTの構文と意味論を厳密に定義するとともに，λGTの型体系としてFGTを設計して型付け規則を与えた．

  • 高水準モデリング言語の特性を活かす高機能な実行・検証系

    2021  

    　View Summary

    研究代表者らは，LMNtalおよびHydLaという二つのモデリング言語の研究開発を推進している．LMNtalはグラフ（ネットワーク）構造の変化を扱う計算モデル，HydLaは連続変化と離散変化の双方を許す実数関数を制約式で定義する計算モデルに基づいており，それぞれ多くの独自機能を備えている．また，いずれの処理系も，モデルのシミュレーションだけでなくモデル検査器（検証系）の機能を備えている点を大きな特徴とする．本研究ではこれらの言語と処理系の有用性をさらに高めるべく，LMNtalについては静的および動的な型の概念の設計と実装，ハイパーグラフを扱うための形式意味論の整備などを行った．HydLaについては検証系としての機能を高めるためのハイブリッドオートマトンモデルの導出の研究を進展させた．

  • 高水準モデリング言語の高機能な実行・検証系

    2021  

    　View Summary

    研究代表者らは，LMNtalおよびHydLaという二つのモデリング言語の研究開発を推進している．LMNtalはグラフ（ネットワーク）構造の変化を扱う計算モデル，HydLaは連続変化と離散変化の双方を許す実数関数を制約式で定義する計算モデルに基づいており，それぞれ多くの独自機能を備えている．また，いずれの処理系も，モデルのシミュレーションだけでなくモデル検査器（検証系）の機能を備えている点を大きな特徴とする．本研究ではこれらの言語と処理系の有用性をさらに高めるべく，LMNtalについては静的および動的な型の概念の設計と実装，ハイパーグラフを扱うための形式意味論の整備などを行った．HydLaについては検証系としての機能を高めるためのハイブリッドオートマトンモデルの導出の研究を進展させた．

  • モデリング言語とその実装への高水準プログラミング言語概念の導入

    2017  

    　View Summary

    研究代表者はグラフと実数という汎用性の高いデータを扱うモデリング言語の設計と実装に取り組み，モデリング言語LMNtalとHydLaの実行系と検証系を開発・公開してきた．本研究では，高階概念，抽象化，メタプログラミングなど，プログラミング言語分野での有用性が広く認められている概念をモデリング言語に導入するための技術課題に設計から実装まで取り組み，高信頼ソフトウェアのためのより高水準なモデリング環境の実現を目指した．成果として，グラフ書換え言語LMNtalにおいては高階関数の表現と操作，ハイブリッド制約言語HydLaにおいては変数や制約の動的生成などのさまざまな拡張を達成した．

  • ハイブリッド制約モデリング言語の高信頼実装技術

    2007   石井　大輔

    　View Summary

    ハイブリッド制約モデリング言語とは，時間の経過に伴って状態が連続変化したり，状態や方程式系自体が離散変化したりするハイブリッドシステムを，制約 (constraints) 概念に基づいて記述・シミュレーション・検証するための高水準言語である．1990年代に先駆となる言語 Hybrid CC が提案実装されていたが，言語機能と実行結果の信頼性の両面で研究の進展が待たれていた．本研究は，新たなハイブリッド制約モデリング言語 Hydra の確立に向けて，その設計論と，計算結果の正しさを保証する高信頼実装の要素技術を開拓することを目標に実施した．本年度の成果は以下のようにまとめることができる．1. 既存のハイブリッド制約言語である Hybrid CC の記述実験および検討を通 じて，Hydra が備えるべき機能，特に記号的離散状態の表現について踏み 込んだ検討を行った．2. 高信頼実装のためには，求解過程において離散的に切り替わる方程式系の 区間演算技術が必須となる．区間演算においては，離散変化条件の成否が 一般に非決定的となるため，成否が決定的になるような小区間への分割を 行いつつ区間演算を進めるアルゴリズムを提案し，その有効性を確認した．3. ハイブリッドシステムにおける重要かつ厄介な性質として，有限時間内に 無限回の離散的状態変化を起こす Zeno 挙動がある．そこで，与えられた システムがZeno 挙動をもつかどうかの自動検証手法を開発した．Zeno 挙 動に関する推論は数値計算では困難であり，数式処理と限定記号除去によ る解析方式を提案してその有効性を確認した．4. ハイブリッドシステムの検証に伝統的に使われてきたハイブリッドオート マトンとハイブリッド制約モデリング言語との関係づけのために、ハイブ リッド制約プログラムからハイブリッドオートマトンへの自動変換技法を 開発して実装した．5. 既存の制約ソルバ，区間演算，多倍長演算ライブラリを高信頼実装の部品 として活用するための調査・実験・準備を行った．区間演算を用いた常微 分方程式ソルバVNODE-LPに多倍長演算を組込み，求解精度向上における有 効性を多数の例題で調査するとともに，非線形制約求解系Elisaを用いた幾 何モデリングにおける制約不足の問題に対処するためのパターン分割手法 を提案・実験した．

  • リンクつき階層多重集合に基づく統合プログラミング言語モデルLMNtal

    2004   加藤　紀夫

    　View Summary

    本研究では、統合言語モデルLMNtal実用化の基盤を固めるために下記の研究を遂行して多様な成果を得た。1. プラットフォーム処理系の整備と拡充研究開発のプラットフォームとなるLMNtal逐次処理系をJavaで実装、公開し、バージョンアップを重ねてきた。分散処理系への拡張を念頭に置いて、膜ごとの計算を非同期に実行するための排他制御や協調動作の方式設計および実装を行った。また可視化機能や他言語インタフェース機能の拡充、プロセス文脈機能の強化、生成コードの改善などの各種改良も行った。処理系の規模はおよそ2万行におよぶ。2. 言語設計の洗練LMNtalが分散計算を的確にモデル化する言語モデルとなるように、従来の操作的意味論の一部を見直した。コネクタ（二つのグラフ構造を接続するための言語要素）に関して、どのような操作を構造合同（可逆）と見なし、どのような操作を遷移関係（非可逆）と見なすべきかを考察し、従来の言語仕様の問題点を発見し修正した。3. LMNtalプログラムに対する型体系の設計LMNtalプログラムが形成するプロセス構造を扱うための型体系を設計し、型安全性の証明を行った。この型体系は、膜に出現する可能性のあるアトム（グラフのノード）の種類やリンクのつながり方を定式化するものである。本研究を通じて、実用的な解析のためには、膜に名前を付けて膜の静的な役割を識別することが有効であるとの知見を得た。4. 分散処理系および小規模制御系向け処理系膜に実行位置情報を付加する機能を導入し、通信・キャッシュ・ロック・終了処理等の機構を逐次処理系に付加することにより、LMNtal分散処理系の試作を行った。また、組込み応用に向けて、センサやアクチュエータをLMNtalのアトムとの対応づける方式を考案し、ロボットコントローラ実機上で動作するLMNtalサブセットの実行系を構築して自律移動ロボットの制御を実現した。

  • 並行論理プログラミングに基づく広域分散計算パラダイムの構築

    1998  

    　View Summary

    並行論理プログラミング言語は、論理プログラミングパラダイムに情報の流れを制御するための同期機構を導入し、並行処理記述のための言語としたものである。なかでも研究提案者の提案した並行論理プログラミング言語GHC(Guarded Horn Clauses)は、簡潔な通信・同期機構をもちながら、構成が動的に変化する並行プロセス系を自然に記述できる柔軟性も併せもつ。　これまでの並行論理プログラミングの研究開発は、主として並列計算機上での高速実行を目標としてきた。一方、コンピュータネットワークの急速な普及と共に、広域分散計算環境で稼働する効率的で安全な分散型アプリケーションを容易に構築するための方法論の確立が急務となっている。そこで本研究では、並行論理プログラミングに基づく広域分散計算パラダイムの確立を目標として、下記の検討を行なった。　宣言型言語とそのプログラミングのもつ簡明さをできるだけ保ちつつ、広域分散計算の記述と非均質計算環境下での実行を可能にする方法の検討。　広域分散環境で稼働する言語処理系に求められる静的プログラム解析技術の確立、およびプログラム解析技術に基づく安全な広域分散ソフトウェア構築方法論の検討。　特に本研究では、広域分散実装のための静的解析技法の確立に重点を置き、並行論理プログラムの参照数解析の体系の提案と理論的整備を行なった。参照数解析とは、複数の参照ポインタをもちうるデータ構造と、単一の参照ポインタしかもたないデータ構造とを、静的プログラム解析によって区別するものである。単一参照のデータ構造に対してはコンパイル時ゴミ集め、記憶域の局所的再利用(local reuse)、データ送信のメッセージパッシングへのコンパイルなどが可能となり、広域分散実装が大幅に単純化、効率化される。本研究ではこの参照数解析の理論的枠組を提案し、解析の安全性を証明した。またこれを、KL1言語用静的解析系klint第２版の機能の一つとして実装し、有効性を確認した。　記号処理言語は動的データ構造の柔軟な作成管理を特徴とするが、分散計算環境における実装は困難とされてきた。これに対して本研究では、記号処理プログラムからも十分な静的解析情報が得られることを示すことができた。簡潔な並行言語を拡張して広域分散計算に適用することによって、単純で検証の容易な広域分散処理記述言語を得ることが期待される。

  • 見込み計算によるインタラクティブ・ソフトウェアの応答性改善法

    1996  

    　View Summary

    　計算機の会話的利用の機会と重要性は最近ますます高まりつつあり、マルチメディア化も大きく進展している。しかし、ほとんどのインタラクティブ・ソフトウェアは、基本的に従来の決定的逐次プログラミング・パラダイムの下に記述されており、計算機性能の著しい向上にもかかわらず、利用者入力に対する応答性能が十分確保されていないことが多い。　そこで本研究では、見込み計算(speculative computation)技法を中心に、利用者タスクとシステムタスクとの並行・並列処理、漸増的計算、実時間処理などの手法を援用することによって、インタラクティブ・ソフトウェアの応答性能を抜本的に改善する方法について検討を進めた。　ネットワークニュースリーダを題材とした実験の結果、利用者の挙動を適切に予測して、コマンド入力後に必要となる処理を可能な限り見込み計算しておくことにより、応答性が大幅に改善できることが実証できた。見込み計算は、フロントエンドのニュースリーダとバックエンドのキャッシュシステムの双方で、各利用者および利用者集団全体の記事購読特性に基づいて行なっている。　さらに本研究では、ニュースリーダでの良好な結果を、WWW記事のキャッシュシステムに適用することを試みた。　WWWにおいては、応答性改善及びネットワーク負荷の抑制を目的として、キャッシュ機能を付加したプロキシサーバが使用されている。しかし、このキャッシュ機能は一度アクセスしたデータを再利用するだけのパッシブなものであり、新たなアクセスには応答性改善効果がない。また、どのデータがキャッシュされているかわからないので、キャッシュの恩恵は偶発的でヒット率の低いものとなる。　そこで、プロキシサーバのキャッシュデータを各利用者毎に整理し、Webブラウザを通して視覚化した。また、キャッシュデータの最新性をバックグラウンドで確認してその更新状況を表示するとともに、今後読む可能性が高いと予測されるデータをトラフィックの少ない時間帯にプリフェッチし、その状況もあわせて視覚化した。一般に、WWW利用時の行動はニュース利用時の行動と比較して予測が困難であるが、見込み計算と視覚化機能との併用によって、良好な応答性能を確保できる見通しを得た。

  • 並行論理プログラミング言語による高速定型処理

    1995  

    　View Summary

    並行論理プログラミング言語は，論理プログラミング・パラダイムに情報の流れを制御するための同期機構を導入し，並行処理記述のための言語としたものであり，柔軟性と簡潔性を大きな特徴とする。しかしながら，これまで，非定型的な並列記号処理のための言語と位置づけられてきたために，定型処理の記述性と効率が不十分であった。一方，並列記号処理の本格的応用のなかには，柔軟な記号処理と，数値計算のような高速定型処理の双方を要するものが増加しつつある。そこで本研究では，並行論理プログラミング言語における効率的な配列操作の枠組の確立を目標として，その基礎研究を行なった。 ベースとなる言語として，静的モード体系を持つ言語Moded Flar GHCを採用した。静的モード体系は，並行論理プログラムの性質に関するもっとも基礎的な情報を提供するもので，制約充足問題として定式化することができ，グラフ単一化によって効率良く解析することができる。また，同様の制約ベースの技法によって，データ型，および参照数（データを指すポインタの数）の解析も可能であることを明らかにした。参照数の解析は，単一代入言語における配列の破壊的操作にとって本質的である。 以上の解析情報は特定の実装に依存しない基礎的情報であるが，浮動小数点演算や配列を用いた処理を最適化し，手続き型言語における効率に近づけるには，さらに，データの具体化状態に関する解析も必要であり，その方式も検討した。 これらの解析情報に基づき，並行処理プログラミング言語処理系KLIC上の浮動小数点数処理および配列処理の高速化を試みた。KLICは，高い基本性能を実現するとともに，ジェネリックオブジェクト機構によってデータ型などの拡張性を確保し，それによって浮動小数点や配列を実装している。しかしながら，ジェネリックオブジェクトによる実装は，空間的，時間的なオーバーヘッドが大きい。 本研究では，上記の各種解析情報によって，ジェネリックオブジェクトによる実装のオーバーヘッドを除去する方法を検討し，実験を行なった。これまでに，典型的な浮動小数点演算で13倍以上，配列の更新演算については，破壊的更新が可能なことが参照数解析によってわかる場合，3.5倍以上の性能向上が得られた。配列演算は，添字検査の手間の比率が大きいため，詳細なプログラム解析によってさらなる性能向上が可能である。今後も，これらの検討を進めることにより，非手続き型言語における配列操作パラダイムの確立を目指し，それを通じて並行論理プログラミングの応用分野の拡大を図ってゆく予定である。

▼display all