λ研究室

λ研究室究程序言語理論型系形式法及其用。

大概

λ研究室究程序言語理論型系形式法及其用。此頁記研究題目諸員論著。

常用程序言語之中環境者変数与値之対応也多蔵於実装之内。本研究立一級環境之理環境自身可為程序中値生成授受合成。拡張λ計算明示変数参照環境更新関数適用之簡約規則並究型安全型推論合流性評価戦略。此亦為理解動的軟件更新部品記録明示代入之共通基礎。

継続者自一点以後之計算也以値表之。例外処理協程非局所脱出後戻等可一理記述。本研究設計継続為一級値之λ計算及対象計算究其与線形論理評価順序型推論制御効果之関係。特明資源一度用之線形性与可複製計算之継続之関係以与安全扱高度制御機構之型系基礎。

此研究欲於実行之前以数学確証程序如期動作。型系非唯検査通常資料型亦可表関数用法制御流及実行時成立条件。本研究用多相型線形型漸進的型付詳細化型効果系等法静的保証程序安全及性質。又明大段階意味論小段階意味論抽象機械程序変換之関係結合理論模型与実装。

模型検査者遍探索系之可能状態自動判定不望動作可起否之技術也。本研究以通信規約Web服務器郵便系負荷分散器等為形式模型検証安全性信頼性規則遵守及実時間性。特注服務不能攻撃耐性。用含時間及計算費用之過程代数比較攻撃者課負荷与服務器処理能力。此示形式法可応用於実際網絡系設計解析。

此題以計算機科学理論展於知的系教育及実用軟件。人工知能中結合知識表現与数値計算以可説明形模擬生命現象之複雑制御。分散計算中究用既存Web基盤如記録頁為計算資源之法及在線証明判定系。又実践始於利用者課題之PBL型教育合要求分析集団形成国際協働及系開発以学情報工学。