2025/09/19 更新

写真a

ニシザキ　シンヤ
西崎　真也
NISHIZAKI SHIN-YA
所属
情報基盤センター 教授
職名
教授
ホームページ
http://www.lambda.cs.titech.ac.jp/
外部リンク

学位

  • 京都大学博士(理学) （ 京都大学理学研究科 ）

研究分野

  • 情報通信 / ソフトウェア

学歴

  • 京都大学

    - 1994年

    　 詳細を見る

  • 京都大学大学院   理学研究科   数理解析専攻

    - 1994年

    　 詳細を見る

    国名： 日本国

    researchmap

  • 京都大学   理学部

    - 1989年

    　 詳細を見る

    国名： 日本国

    researchmap

経歴

▼全件表示

所属学協会

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

    　 詳細を見る

  • Association of Computing Machinary

    　 詳細を見る

  • European Association of Theoretical Computer Science

    　 詳細を見る

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

    　 詳細を見る

  • 人工知能学会

    　 詳細を見る

  • European Association of Theoretical Computer Science

    　 詳細を見る

  • Association of Computing Machinary

    　 詳細を見る

▼全件表示

委員歴

  • 日本ソフトウェア科学会   編集委員  

    2000年   

    　 詳細を見る

    団体区分：学協会

    日本ソフトウェア科学会

    researchmap

  • 情報処理学会プログラミング研究会   論文誌編集委員  

    1998年 - 2001年   

    　 詳細を見る

    団体区分：学協会

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

    researchmap

論文

▼全件表示

書籍等出版物

  • この定理が美しい

    数学書房  2009年  （ ISBN:4903342107 ）

    　詳細を見る

  • 理工系のためのコンピュータサイエンス

    サイエンス社  2008年  （ ISBN:4781911846 ）

    　詳細を見る

  • 論理と計算のしくみ

    岩波書店  2007年  （ ISBN:4000061917 ）

    　詳細を見る

  • 関数的環境計算の合流性，

    日本ソフトウェア科学会 第16回大会論文集  1999年 

    　詳細を見る

  • Formalization of Graph Search Algorithm and Its Applications

    Lecture Notes in Computer Science  1998年 

    　詳細を見る

  • Formalization of Graph Search Algorithm and Its Applications

    Lecture Notes in Computer Science  1998年 

    　詳細を見る

▼全件表示

MISC

  • 論理と計算のしくみと私

    西崎 真也

    コンピュータ ソフトウェア   32 ( 3 )   3_96 - 3_97   2015年

    　詳細を見る

    記述言語：日本語   出版者・発行元：日本ソフトウェア科学会  

    DOI： 10.11309/jssst.32.3_96

    CiNii Research

    researchmap

  • 東日本大震災 危機発生時の対応について考える:14.放射線量測定・放射性物質拡散シミュレーション（独，仏，日本）

    西崎, 真也, Shin-ya, NISHIZAKI

    情報処理   52 ( 9 )   1088 - 1089   2011年8月

    　詳細を見る

    記述言語：日本語   出版者・発行元：情報処理学会  

    本記事では、福島第一原子力発電所の事故に伴いおこなわれてきた、空間放射線量や環境放射能の測定結果、放射性物質の拡散シミュレーション、そしてそれらの情報提供の状況について記述する。

    CiNii Books

    CiNii Research

    researchmap

    その他リンク： http://id.nii.ac.jp/1001/00075794/

  • 証明支援系を用いたMorrisの二分木走査アルゴリズムの検証

    山田 一宏, 渡部 卓雄, 森口 草介, 西崎 真也

    情報処理学会研究報告. ソフトウェア工学研究会報告   2011 ( 26 )   1 - 4   2011年3月

    　詳細を見る

    記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

    我々はMorrisのアルゴリズムのCによる実装の検証を試みた.このアルゴリズムは再帰やスタックを用いずに二分木の走査を行うものであり,節点内部に余分なタグも不要であるという特徴がある.本研究はポインタ操作を伴うCプログラムへの検証支援ツール適用のケーススタディであり,今回は検証支援系CaduceusおよびWhy,自動証明系Simplifyおよび対話的証明支援系Coqを使用した.本稿では,これらによる検証手法とその結果の概要を述べる.

    researchmap

  • 実行速度に依存するシステムの形式化と検証—Formalization of Systems Depending on Execution Speed

    水野 孝久, 西崎 真也

    日本ソフトウェア科学会大会論文集 / 日本ソフトウェア科学会 編   27   1 - 9   2010年9月

    　詳細を見る

    記述言語：日本語   出版者・発行元：[東京] : 日本ソフトウェア科学会  

    CiNii Books

    CiNii Research

    researchmap

    その他リンク： https://ndlsearch.ndl.go.jp/books/R000000004-I026943424

  • Programs with continuations and linear logic

    Shin-ya NISHIZAKI

    Science of Computer Programming   21 ( 2 )   165 - 190   2010年

    　詳細を見る

  • モデル検査器を用いたソフトウェアの耐故障性解析—Analysis of Software Fault Tolerance by Model Checking

    熊本 浩紀, 西崎 真也, 成田 憲亮

    日本ソフトウェア科学会大会論文集 / 日本ソフトウェア科学会 編   26   245 - 256   2009年9月

    　詳細を見る

    記述言語：日本語   出版者・発行元：[東京] : 日本ソフトウェア科学会  

    CiNii Books

    CiNii Research

    researchmap

    その他リンク： https://ndlsearch.ndl.go.jp/books/R000000004-I029997497

  • プロセス生成コスト解析するためのプロセス計算—Process Algebra for Cost Analysis of Process Creation

    藤井 みづき, 西崎 真也, 池田 立野

    日本ソフトウェア科学会大会論文集 / 日本ソフトウェア科学会 編   24   1 - 19   2007年9月

    　詳細を見る

    記述言語：日本語   出版者・発行元：[東京] : 日本ソフトウェア科学会  

    CiNii Books

    CiNii Research

    researchmap

    その他リンク： https://ndlsearch.ndl.go.jp/books/R000000004-I030116156

  • プロセス計算によるコスト解析とネットワークシミュレーションとの比較—Comparison between Cost Analysis with Process Calculus and Network Simulation

    池田 立野, 西崎 真也

    日本ソフトウェア科学会大会論文集 / 日本ソフトウェア科学会 編   24   1 - 6   2007年9月

    　詳細を見る

    記述言語：日本語   出版者・発行元：[東京] : 日本ソフトウェア科学会  

    CiNii Books

    CiNii Research

    researchmap

    その他リンク： https://ndlsearch.ndl.go.jp/books/R000000004-I030116163

  • 定理アーカイブにおけるDoS攻撃耐性

    西崎, 真也, Shin-ya, Nishizaki

    情報処理学会論文誌プログラミング（PRO）   47 ( SIG6(PRO29) )   70 - 70   2006年5月

    　詳細を見る

    記述言語：日本語   出版者・発行元：情報処理学会  

    本研究では，定理を保存する定理アーカイブにおけるサービス不能攻撃への耐性について考察する．格納される定理は，アーカイブ自身において，その定理の正当性が保証されるべきである．定理の正当性検証は，一般に計算コストは軽くなく，悪意のある者からのアクセスにより，サービス不能攻撃（DoS 攻撃）をしかけられる脆弱性を有している．本研究では，等式系とそれと等価な完備な項書き換え系を定理ととらえ，等式アーカイブにおけるDoS 攻撃に対する耐性を向上させる手法を提案する．
    We study resistance against Denial-of-Services attacks in a theorem archives server. The server should guarantee correctness of the stored theorems. Since the cost of correctness checking in the server is not negligible, the server has vulnerability to Denial-of-service attacks from malicious submission of theorems. In our study, we regard equation archives as theorem archives and propose improvement method of Denial-of-Service attack resistance.

    CiNii Books

    CiNii Research

    researchmap

    その他リンク： http://id.nii.ac.jp/1001/00016568/

  • 通信プロトコルにおけるサービス不能攻撃耐性のための型付π計算

    冨岡 大悟, 池田立野, 西崎真也

    コンピュータソフトウェア   23 ( 3 )   66 - 84   2006年

    　詳細を見る

    記述言語：日本語   出版者・発行元：日本ソフトウェア科学会  

    通信プロトコルの安全性,特に認証プロトコルにおける認証の正当性に関する研究は,AbadiやGordonによるspi計算(secure pi-calculus)などをはじめとして,近年さかんに行なわれている.プロトコルにおける安全性は,認証の正当性や機密性などの他に,最近では,サービス不能攻撃(Denial-of-Service attack)耐性が重要視される.もっとも典型的な攻撃例としては,TCPの3ウェイハンドシェイクにおけるSYNあふれ攻撃(SYN-flooding attack)が知られている.プロトコルのサービス不能攻撃耐性を形式的に扱う枠組みとしては,メドーズらにより提唱された,コスト情報を付記したアリス・ボブ記法があった.この他に,最近,冨岡らにより提唱されたspice計算[13]がある.spice計算は,spi計算を拡張したもので,プロセスの計算における計算コストが,サーバーやクライアントの計算機において,どのように費されるかを明示的に表現できるように,システムにおける計算機構成を型として形式化した.そして,書き換えスタイルの操作的意味論があたえられており,プロセスに対する型付けの情報を利用することにより,計算の進行における計算コストを区別するようになっている.記憶コストは,サービス不能攻撃耐性を測る場合,各種の計算コストのうちで最も重要となるのだが,spice計算では,記憶領域の解放を明示的に行なうようにした.本研究では,従来のspice計算における型体系と操作的意味論を,計算機ごとの記憶コストの見積りに併せて,記憶領域の解放に関する正当性を保証するように,改良した.また,SYNあふれ攻撃とその防御策であるSYNクッキーが形式化できることを適用例として紹介する.Security on communication protocols, especially authentication protocols, has been studied by many researchers, for example, the secure pi-calculus by Abadi and Gordon. Resistance against the denial-of-service attack is one of the important issues of secure protocols as secrecy and authenticity. A typical example of the denial-of-service attack is TCP SYN-flooding attack. Meadows proposed an Alice-and-Bob notation annotated with cost description as a formal framework for analyzing resistance against denial-of-service attacks. In this paper, we proposed the spice-calculus, which is an extended secure pi-calculus by adding explicit description on computation costs. We give operational semantics and a type system to the spice-calculus; the typing represents configuration of network system. We then investigate theoretical properties on the type system, e. g. subject reduction. We present formalization of TCP SYN flooding attack and its protection method, SYN-cookie, on the typed spice-calculus as examples.

    DOI： 10.11309/jssst.23.3_66

    CiNii Books

    researchmap

    その他リンク： https://projects.repo.nii.ac.jp/?action=repository_uri&item_id=288763

  • Spice計算からモデル記述言語Promelaへの変換によるサービス不能攻撃耐性解析

    西崎 真也

    第3回システム検証の科学技術シンポジウム論文集   7 - 14   2006年

    　詳細を見る

  • 等式アーカイブにおける安全な検査—Safely Checking in Equation Archive

    玉野 浩嗣, 西崎 真也

    日本ソフトウェア科学会大会論文集 / 日本ソフトウェア科学会 編   22   1 - 6   2005年9月

    　詳細を見る

    記述言語：日本語   出版者・発行元：[東京] : 日本ソフトウェア科学会  

    CiNii Books

    CiNii Research

    researchmap

    その他リンク： https://ndlsearch.ndl.go.jp/books/R000000004-I030161087

  • 多相環境計算における強正規化可能性

    清水, 亮, Ryo, Shimizu

    情報処理学会論文誌プログラミング（PRO）   46 ( SIG6(PRO25) )   35 - 46   2005年4月

    　詳細を見る

    記述言語：日本語   出版者・発行元：情報処理学会  

    多相環境計算は，環境をファーストクラスオブジェクトとして扱うことができるλ 計算に，多相型体系を導入したものである．これまでに，ML 多相型体系を持つ環境計算とその型推論アルゴリズムは提案し，その主部簡約定理を得ていたが，強正規化可能性定理はまだ得ていなかった．本論文ではML 多相型体系を包含する，2 階型体系を提案し，その強正規化可能性定理を証明する．この性質は，多相環境計算から多相λ 計算（2 階型付λ 計算）への変換をもちいて，多相環境計算の強正規化可能性を多相λ 計算の強正規化可能性に帰着することによって得られる．
    Polymorphic environment calculus is a polymorphic lambda calculus with first-class environments. We proposed environment calculus with ML-polymorphic type system and its type inference algorithm and proved principal type theorem with respect to the type system. In this paper, we propose second-order type system for the environment calculs, which includes the ML-polymorphic type system and prove strong normalization theorem with respect to the second-order type system. The theorem is proved by using transformation of the environment calculus to the polymorphic lambda calculus.

    CiNii Books

    CiNii Research

    researchmap

    その他リンク： http://id.ndl.go.jp/bib/7326677

  • 等式アーカイブにおける安全な検査

    玉野 浩嗣, 西崎 真也

    日本ソフトウェア科学会大会講演論文集   22   368 - 373   2005年

    　詳細を見る

    記述言語：日本語   出版者・発行元：日本ソフトウェア科学会  

    定理証明系において等式を適用することによる式の簡略化は証明の重要な要素である。それらの等式の重要な性質として、停止性と合流性がある。定理証明系が使用できる停止性、合流性をみたす等式アーカイブをサーバ側に構築することを目標とし、本研究では信頼できないクライアントに対しても安全にこれらの性質を検査する方法を提唱する。

    DOI： 10.11309/jssstconference.22.0.368.0

    CiNii Research

    researchmap

  • 多相環境計算の強正規化可能性

    西崎 真也

    情報処理学会論文誌 46・SIG4   2005年

    　詳細を見る

  • プロコルのDoS攻撃耐性解析のための計算体系における時間モデル

    西崎 真也

    日本ソフトウェア科学会第22回大会予稿集 (CD-Rom)   2005年

    　詳細を見る

  • 対話的証明器つき証明文書—Proof documents with interactive prover

    玉野 浩嗣, 西崎 真也

    日本ソフトウェア科学会大会論文集 / 日本ソフトウェア科学会 編   21   1 - 4   2004年9月

    　詳細を見る

    記述言語：日本語   出版者・発行元：[東京] : 日本ソフトウェア科学会  

    CiNii Books

    CiNii Research

    researchmap

    その他リンク： https://ndlsearch.ndl.go.jp/books/R000000004-I030226668

  • 対話的証明器つき証明文書

    玉野 浩嗣, 西崎 真也

    日本ソフトウェア科学会大会講演論文集   21   79 - 79   2004年

    　詳細を見る

    出版者・発行元：日本ソフトウェア科学会  

    本論文では，提唱する``PDIP''は，対話的証明器を証明文書を組み込むというアーキテクチャであり，可搬性に富んでいる．その手始めに，等式論理をベースとしたPDIPのシステムを実装した．証明文書はHTML文書として表現し，証明器は，JavaScriptのスクリプトとして実現した．証明器によってなされた計算結果は，すべてHTML文書内に表現し，JavaScriptインタプリタ内の状態としては持たないように実装し，visibilityに配慮した

    DOI： 10.11309/jssstconference.21.0.79.0

    CiNii Research

    researchmap

  • ファーストクラス継続を持つオブジェクト計算

    西崎, 真也, Shin-Ya, Nishizaki

    情報処理学会論文誌プログラミング（PRO）   44 ( SIG13(PRO18) )   116 - 116   2003年10月

    　詳細を見る

    記述言語：日本語   出版者・発行元：情報処理学会  

    AbadiとCardelliにより提唱されたオブジェクト計算は，大変簡潔な構文と意味論により定義されるにもかかわらず，セルフパラメータの遅延束縛などオブジェクト指向言語の主要な計算機構をモデル化することに成功している．継続とは，計算のある時点における計算の残りの部分を表現する概念であり，実行系の内部状態の1つである．ファーストクラス継続は，ある時点の継続をデータとして保存したり，データとして保存した継続をしたりすることを可能とするものである．ファーストクラス継続は，プログラミング言語Schemeで実現され，コルーチンやバックトラックなどを表現できることが知られている．本研究では，オブジェクト計算にファーストクラス継続の概念を導入した継続オブジェクト計算を提唱する，この体系において，意味論は評価文脈を用いて定義される弱簡約関係により与えられる．ファーストクラス継続は，評価文脈をフィールドに保存する継続オブジェクトとして形式化される．最初に型なし継続オブジェクト計算を紹介する．次に，継続オブジェクト計算の1階型体系を与え，主部簡約定理を示す．さらに，部分型体系を与え，主部簡約定理のほか，基本的性質を示す．
    With the advance of information society, releasing the software at an early stage that satisfies users has been required, and therefore it has been more important to quickly develop the software that the user can check and feed back. In software development, based on users’ concept, developers make the specifications of a program cooperating with the users, and then design, make, test and debug the program. Through this procedure, programs are completed. If we can use the image that users have to design a program, and if the program is completed when the design finishes, we can easily develop software and reduce the time required to develop it. This presentation presents an approach to a brain-image oriented programming method and describes the BioPro system that implements this method for Web applications. The brain-image oriented programming has the features that users can develop programs based on their image, (2) easily verify the completeness of components that make up the program and the consistency between them, and (3) easily confirm what they have developed so far in the middle of the development.

    CiNii Books

    CiNii Research

    researchmap

    その他リンク： http://id.nii.ac.jp/1001/00016739/

  • ファーストクラス継続をもつ仮想機械 : 関数型仮想機械の単純化—Abstract Machine with First-class Continuations

    西崎 真也, 植田 友幸

    日本ソフトウェア科学会大会論文集 / 日本ソフトウェア科学会 編   20   1 - 4   2003年9月

    　詳細を見る

    記述言語：日本語   出版者・発行元：[東京] : 日本ソフトウェア科学会  

    CiNii Books

    CiNii Research

    researchmap

    その他リンク： https://ndlsearch.ndl.go.jp/books/R000000004-I030279104

  • ファーストクラス継続をもつ仮想機械

    西崎 真也, 植田 友幸

    日本ソフトウェア科学会大会講演論文集   2003   6 - 6   2003年

    　詳細を見る

    出版者・発行元：日本ソフトウェア科学会  

    従来，関数型言語のためのバイトコードを解釈する仮想機械として、SECDマシンやCAMマシンなど多くのものが提唱され，それらに基づく実装や理論的な側面に関する研究がなされてきた．本論文では，SECDマシンを単純化した仮想機械SAM(Simple Abstract Machine)を提唱する．変数参照機能を単純化することにより，仮想機械におけるファーストクラス継続を簡潔に扱うことが可能になっている。

    DOI： 10.11309/jssstconference.2003.0.6.0

    CiNii Research

    researchmap

  • 特集「セキュアコンピューティング」の編集にあたって

    西崎 真也, 加藤 和彦

    コンピュータ ソフトウェア   20 ( 3 )   213 - 213   2003年

    　詳細を見る

    記述言語：日本語   出版者・発行元：日本ソフトウェア科学会  

    DOI： 10.11309/jssst.20.213

    CiNii Books

    CiNii Research

    researchmap

  • 計算機構成の型を導入した、DoS攻撃耐性解析におけるコスト評価のための計算体系—Computational system with configuration type for cost analysis on DoS-attack resistance

    西崎 真也, 冨岡 大悟, 大石 浩司

    日本ソフトウェア科学会大会論文集 / 日本ソフトウェア科学会 編   19   1 - 5   2002年9月

    　詳細を見る

    記述言語：日本語   出版者・発行元：[東京] : 日本ソフトウェア科学会  

    CiNii Books

    CiNii Research

    researchmap

    その他リンク： https://ndlsearch.ndl.go.jp/books/R000000004-I030350171

  • 名前呼び環境PCFの意味論

    須藤, 正人, Masato, Suto

    情報処理学会論文誌プログラミング（PRO）   43 ( SIG03(PRO14) )   52 - 61   2002年3月

    　詳細を見る

    記述言語：日本語   出版者・発行元：情報処理学会  

    ファーストクラス環境とは，実行状態の1 つである環境をファーストクラスオブジェクトとしたり，それを戻したりできる機能である．環境λ 計算は，λ 計算にそのような機能を組みこんだものである．PCF は，再帰演算子を持つ単純型付きλ 計算であり，評価戦略の研究のための枠組みとして用いられる．本研究では，ファーストクラス環境と名前呼び評価戦略との関連を研究するために，環境PCF とPCF の名前呼び評価戦略を環境計算に拡張したものを定義する．そして，評価戦略と意味論に関する基本的性質である計算的適切さなど，理論的性質について考察する．
    The first-class environment is one of the evaluation states, which enables us to use meta-level environments as object-level entities, and oppositely, to use the object-level environments as meta-level ones. The environment calculus is a variant of lambda calculus, which is provided with such mechanism. Formal system PCF, a simply-typed lambda calculus with recursive operator, is a framework for semantical study of evaluation strategy. In this paper, we propose an extended system of PCF with first-class environments and study call-by-name strategy and its semantical properties, including computational adequacy.

    CiNii Books

    CiNii Research

    researchmap

    その他リンク： http://id.ndl.go.jp/bib/6124111

  • DoS攻撃に対するプロトコルの耐性に関する解析 : 形式的枠組みの構築にむけて—Analysis of Tolerance of Network Protocol for Denial of Service

    冨岡 大悟, 西崎 真也

    日本ソフトウェア科学会大会論文集 / 日本ソフトウェア科学会 編   18   1 - 4   2001年9月

    　詳細を見る

    記述言語：日本語   出版者・発行元：[東京] : 日本ソフトウェア科学会  

    CiNii Books

    CiNii Research

    researchmap

    その他リンク： https://ndlsearch.ndl.go.jp/books/R000000004-I030483278

  • 対称的な型推論アルゴリズム—Balanced Type Inference

    松下 祐介, 植田 友幸, 西崎 真也

    日本ソフトウェア科学会大会論文集 / 日本ソフトウェア科学会 編   18   1 - 4   2001年9月

    　詳細を見る

    記述言語：日本語   出版者・発行元：[東京] : 日本ソフトウェア科学会  

    CiNii Books

    CiNii Research

    researchmap

    その他リンク： https://ndlsearch.ndl.go.jp/books/R000000004-I030481625

  • ファーストクラス環境による単一化機構の関数型言語への組み込み

    西崎, 真也, Shin-Ya, Nishizaki

    情報処理学会論文誌プログラミング（PRO）   41 ( SIG09(PRO8) )   103 - 103   2000年11月

    　詳細を見る

    記述言語：日本語   出版者・発行元：情報処理学会  

    本論文では，ファーストクラス環境の機構を用いて単一化機構を関数型言語へ組み込む方法を提唱する．単一化子は変数上の代入として表現されるが，これを変数の束縛する環境とを同一視することにより，単一化の機構を関数型言語へ自然に組み込むことが可能となる．
    In this paper, we propose a way of embedding of the unification mechanism into function languages through facility of first-class environments, where unificands are introduced as expressions and their evaluation is defined as the first-order unification.

    CiNii Books

    CiNii Research

    researchmap

    その他リンク： http://id.nii.ac.jp/1001/00016918/

  • A Polymorphic Environment Calculus and its Type-Inference Algorithm.

    Shin-ya Nishizaki

    Higher-Order and Symbolic Computation   13 ( 3 )   239 - 278   2000年9月

    　詳細を見る

    記述言語：英語   出版者・発行元：Kluwer Academic Publishers  

    DOI： 10.1023/A:1010010314528

    Scopus

    researchmap

  • Javaにおけるインテグリティモデル—Java Integrity Model

    児島 尚, 丸山 宏, 西崎 真也

    日本ソフトウェア科学会大会論文集 / 日本ソフトウェア科学会 編   17   1 - 4   2000年9月

    　詳細を見る

    記述言語：日本語   出版者・発行元：[東京] : 日本ソフトウェア科学会  

    CiNii Books

    CiNii Research

    researchmap

    その他リンク： https://ndlsearch.ndl.go.jp/books/R000000004-I030479266

  • 環境計算とオブジェクト計算との比較—Comparison between Environment Calculus and Object Calculus

    西崎 真也

    日本ソフトウェア科学会大会論文集 / 日本ソフトウェア科学会 編   17   1 - 4   2000年9月

    　詳細を見る

    記述言語：日本語   出版者・発行元：[東京] : 日本ソフトウェア科学会  

    CiNii Books

    CiNii Research

    researchmap

    その他リンク： https://ndlsearch.ndl.go.jp/books/R000000004-I030479198

  • 第5回東工大スーパーコンピュータ・コンテスト

    西崎 真也

    数学セミナー   39 ( 1 )   52 - 56   2000年1月

    　詳細を見る

    記述言語：日本語   出版者・発行元：東京 : 日本評論社  

    資料形態 : テキストデータ プレーンテキスト
    コレクション : 国立国会図書館デジタルコレクション > デジタル化資料 > 雑誌

    CiNii Books

    CiNii Research

    researchmap

    その他リンク： https://ndlsearch.ndl.go.jp/books/R000000004-I4935523

  • グラフ探索アルゴリズムの発展とその検証

    山本光晴, 高橋孝一, 萩谷昌己, 西崎真也, 玉井哲雄

    コンピュータソフトウェア別冊   92   2000年

    　詳細を見る

  • Evolution of Graph Search Algorithms and Their Verification

    Computer Software   92   2000年

    　詳細を見る

  • A Polymorphic Environment Calculus and its Type-Inference Algorithm

    Shin-ya Nishizaki

    Higher-Order and Symbolic Computation   13 ( 3 )   239 - 278   2000年

    　詳細を見る

  • Translations of First-Class Environments to Records

    Nishizaki Shin-ya

    Proceedings of First International Workshop on Explicit Substitutions: Theory and Applications to Programs and Proofs   81 - 92   1998年7月

    　詳細を見る

    記述言語：英語  

    CiNii Research

    researchmap

  • 環境λ計算と単一化機構

    西崎 真也

    情報処理学会研究報告. PRO, [プログラミング]   96 ( 58 )   37 - 42   1996年5月

    　詳細を見る

    記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

    著者は、関数型プログラミング言語の理論的モデルであるλ計算を拡張し、環境がファーストクラスな対象として扱えるような体系「環境λ計算」を提唱し研究してきた。環境λ計算では、環境を代入として形式化し、代人を項としてオブジェクトレベルで扱うことにより、環境をファーストクラスな対象として形式化することを可能にしている。本論文では、単一化問題を環境λ計算の構文に導入し、その評価を単一化とし、そして、その解である単一化代入をファーストクラスな環境とみなすことにより、環境λ計算への単一化機構の融合をおこなった。

    CiNii Books

    CiNii Research

    researchmap

  • 構造化プログラミング—構造<特集>

    西崎 真也

    数学セミナー   33 ( 11 )   p42 - 45   1994年11月

    　詳細を見る

    記述言語：日本語   出版者・発行元：東京 : 日本評論社  

    資料形態 : テキストデータ プレーンテキスト
    コレクション : 国立国会図書館デジタルコレクション > デジタル化資料 > 雑誌
    記事分類: データ処理・計算機器--ソフトウェア

    CiNii Books

    CiNii Research

    researchmap

    その他リンク： https://ndlsearch.ndl.go.jp/books/R000000004-I3901005

  • PROGRAMS WITH CONTINUATIONS AND LINEAR LOGIC

    S NISHIZAKI

    SCIENCE OF COMPUTER PROGRAMMING   21 ( 2 )   165 - 190   1993年10月

    　詳細を見る

  • 環境をファースト・クラス・オブジェクトとして扱えるλ計算

    西崎 真也

    情報処理学会研究報告. [プログラミング-言語基礎実践-]   93 ( 46 )   9 - 16   1993年5月

    　詳細を見る

    記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

    Lispの方言の一つ,Schemeでは環境をファースト・クラス・オブジェクトとして取り扱うことができる.この機能を付加した単純型つきλ計算λ^<env>を提唱し,その簡約規則の停止性を示した.またDe-Bruijnインデックスやα同値関係などにおける,通常のλ計算との違いについて考察した.

    CiNii Books

    CiNii Research

    researchmap

  • Programs with Continuations and Linear Logic.

    Shin-ya Nishizaki

    Science of Computer Programming   21 ( 2 )   165 - 190   1993年

    　詳細を見る

  • 92-9 制御におけるFormulae-as-Typesの概念

    西崎 真也

    情報処理   33 ( 3 )   295 - 296   1992年3月

    　詳細を見る

    記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

    CiNii Books

    CiNii Research

    researchmap

  • Programs with Continuations and Linear Logic.

    Shin-ya Nishizaki

    Theoretical Aspects of Computer Software(TACS)   21 ( 2 )   513 - 531   1991年

    　詳細を見る

    記述言語：英語   出版者・発行元：Springer  

    DOI： 10.1007/3-540-54415-1_62

    Scopus

    researchmap

    その他リンク： https://dblp.uni-trier.de/db/conf/tacs/tacs91.html#Nishizaki91

▼全件表示

講演・口頭発表等

  • Time Model of Computational System for DoS attack resistance of Protocols

    2010年 

    　詳細を見る

  • 継続つきプログラミング言語と線形論理

    1991年 

    　詳細を見る

  • Safely Checking in Equation Archive

    2010年 

    　詳細を見る

  • プロトコルのDoS攻撃耐性解析のための計算体系における時間モデル

    日本ソフトウェア科学会第22回大会  2010年 

    　詳細を見る

  • 等式アーカイブにおける安全な検査

    日本ソフトウェア科学会第22回大会  2010年 

    　詳細を見る

  • Programs with continuations and linear logic

    Theoretical Aspects of Computer Software  1991年 

    　詳細を見る

  • Programs with continuations and linear logic

    Theoretical Aspects of Computer Software  1991年 

    　詳細を見る

  • First-class Environments and polymorphism

    1994年 

    　詳細を見る

  • ML with First-class Environments and Type Inference Algorithm

    Lecture Notes in Computer Science  1994年 

    　詳細を見る

  • ファーストクラスな環境と多相型

    関数プログラミングＩＩ  1994年 

    　詳細を見る

  • ML with First-class Environments and Type Inference Algorithm

    Lecture Notes in Computer Science  1994年 

    　詳細を見る

  • A Visualization Tool for a Proof Checker that Deals with Diagrammatic Objects

    1995年 

    　詳細を見る

  • Type Inference for Simply-Typed Environment Calculus with Shadowing

    Fuji International Workshop on Functional and Logic Programming  1995年 

    　詳細を見る

  • 図的対象を扱う証明チェッカのための視覚化ツール

    第3回「インタラクティブシステムとソフトウェアに関するワークショップ」(WISS’95)  1995年 

    　詳細を見る

  • Type Inference for Simply-Typed Environment Calculus with Shadowing

    Fuji International Workshop on Functional and Logic Programming  1995年 

    　詳細を見る

  • Translations of First-Class Environments to Records

    First International Workshop on Explicit Substitutions: Theory and Applications to Programs and Proofs  1998年 

    　詳細を見る

  • Javaのクラスローダ制約の定式化

    情報処理学会論文誌プログラミング  2000年 

    　詳細を見る

  • Translations of First-Class Environments to Records

    First International Workshop on Explicit Substitutions: Theory and Applications to Programs and Proofs  1998年 

    　詳細を見る

  • Programmable Environment Calculus as Theory of Dynamic Software Evolution

    International Symposium on Principles of Software Evolution, ISPSE 2000  2000年 

    　詳細を見る

  • 名前呼び環境PCFの意味論

    情報処理学会論文誌  2001年 

    　詳細を見る

  • Programmable Environment Calculus as Theory of Dynamic Software Evolution

    International Symposium on Principles of Software Evolution, ISPSE 2000  2000年 

    　詳細を見る

  • Formalization of Classloader Constraints of Java

    IPSJ Transactions on Programming  2000年 

    　詳細を見る

  • AnZenMail: A Secure and Certified E-mail System

    Lecture Notes in Computer Science  2002年 

    　詳細を見る

  • Semantics of Call-by-name environment PCF

    Journal of Information Processing Society of Japan  2001年 

    　詳細を見る

  • AnZenMail: A Secure and Certified E-mail System

    Lecture Notes in Computer Science  2002年 

    　詳細を見る

  • A Cost Estimation Calculus for Analyzing the Resistance to Denial-of-Service Attack

    Second Mext-NSF-JSPS International Symposium, ISSS 2003  2004年 

    　詳細を見る

  • A Cost Estimation Calculus for Analyzing the Resistance to Denial-of-Service Attack

    Second Mext-NSF-JSPS International Symposium, ISSS 2003  2004年 

    　詳細を見る

  • Secure Filtering of Client-Side Scripts by Program Transformation

    FIT 2003  2003年 

    　詳細を見る

  • Secure Filtering of Client-Side Scripts by Program Transformation

    FIT 2003  2003年 

    　詳細を見る

  • プロセス計算によるコスト解析とネットワークシミュレーションの比較

    日本ソフトウェア科学会第24 回大会  2007年 

    　詳細を見る

  • プロセス生成コスト解析するためのプロセス計算

    日本ソフトウェア科学会第24 回大会論文集  2007年 

    　詳細を見る

  • Spice計算からモデル記述言語Promelaへの変換によるサービス不能攻撃耐性解析

    第三回システム検証の科学技術シンポジウム  2006年 

    　詳細を見る

  • プロセス計算による定性的コスト解析とネットワークシミュレータによ る定量的コスト解析

    第４回システム検証の科学技術シ ンポジウム論文集  2007年 

    　詳細を見る

  • Spice 計算へのブロードキャスト通信の拡張

    第5回システム検証の科学技術シンポジウム  2008年 

    　詳細を見る

  • Spice計算へのブロードキャスト通信の拡張

    システム検証の科学技術シンポジウム(SSV 2008)  2008年 

    　詳細を見る

▼全件表示

受賞

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

    1995年  

    　詳細を見る

    受賞国：日本国

    researchmap

  • 情報処理学会研究賞

    1993年  

    　詳細を見る

    受賞国：日本国

    researchmap