はてなブックマーク

(このページの内容は更新されておりません。近況については千葉工業大学 人工知能・ソフトウェア技術研究センターの紹介ページをご参照ください。) 米澤明憲 To English Version/英語版へ 研究室と米澤の紹介 米澤は、並列オブジェクトに関する研究を、長年にわたり世界の先頭に立って行ってきた。最初の着想を得たのは、 1970年代中頃、マサチューセッツ工科大学（ＭＩＴ）の博士課程に在学中まで遡る。当時はコンピュータがまだ高価で、 一台のコンピュータを多くの利用者が共用せざるをえない時代であったにも係わらず、無尽蔵と言えるくらいに多数 コンピュータを同時・並列的に利用するソフトウェアの構成はいかにあるべきかを考え、その構成原理を世界に先駆けて提唱したた。 ＭＩＴでPh.Dを取得した後、東京工業大学を経て、１９８９年には東京大学理学部情報科学科教授に就任し、 今日にいたるまで、並列オブジ

News (2010-11-09) Jonathan Kimmitt created a pretty GUI frontend for iPad and it is now available on AppStore! Build Instruction 1. Requirements You need a working toolchain (gcc and binutils) for iOS (iPod Touch/iPad/iPhone). For example, you can use the official iOS SDK. In addition, in order to run your O'Caml programs, you need the iPhone Simulator of SDK, registered iOS devices, or jailbroken

情報科学演習 III 課題紹介（小林研究室） 近年、プログラミング言語における型システムをはじめとする基礎理論の役割 がますます重要になってきており、プログラムの正しさの保証だけでなく、コ ンパイラにおけるプログラム最適化や効率のよいランタイムシステムの構築、 セキュリティの問題の解決のためにも種々の型システムやプログラム解析が用 いられています。当研究室でも最近は（特に並行プログラミング言語の）型シ ステムとそれに基づくプログラム解析・メモリ管理といったトピックに力を入 れて研究をすすめています。 そこで情報科学演習 III では、型システムなどの基礎理論とコンパイラやラ ンタイムシステムがどのようにかかわっているかを知ってもらうために、以下 のテーマを用意してみました（この中には、4週間の演習期間の中で完了させ るのは難しい課題も含まれています。そういうものについては、4週間の期間 中

Kenji Kaneda received his Ph.D. in Computer Science from the University of Tokyo in 2006. He received his Bachelor of Science in Information Science and Master of Information Science and Technology in Computer Science in 2001 and 2003 from the University of Tokyo respectively. He joined Google Japan Inc. in June, 2006. Before that, he was a postdoctoral researcher granted by Japan Society for the

About TVMM Tiny Virtual Machine Monitor (TVMM) is a yet-another virtual machine monitor, which has been developed for the purpose of education and verification. Since its design and implementation are simpler than those of existing virtual machine monitors (e.g., VMware, Xen), programmers can easily understand how the VMM works. In addition, TVMM is useful as a building block towards secure virtua

Next: 並列オブジェクト指向言語の汎用高並列計算機向け処理系の開発と その応用実証プログラムによる評価 １ 概要 ２ 言語設計 ３ 実装技術 ４ プログラム開発ツール ５ 応用実証プログラム設計・開発 Mitsubishi Research Institute,Inc. Mon Feb 24 13:38:59 JST 1997

研究室紹介 米澤 明憲 教授 私のソフトウェア研究, コンピュータソフトウェア, 21(4), 2004 (pdf) 研究室概要 (pdf) 研究室までの案内図 主なプロジェクト・研究グループ e-Society (安全なシステム記述言語および高信頼OS) 高安全なC言語，およびC++言語コンパイラの開発 (VITC) OS用型付きアセンブリ言語の設計・実装 (TALK, TOS, Kernel Mode Linux) プロトコル実装の形式的検証 (Applpi) Towards Formal Verification of Memory Properties using Separation Logic Combining Type-Based Analysis and Model Checking for Finding Counterexamples against Non-Inte

Recent Papers IEEE International Symposium on High Performance Distributed Computing (2006) "WOW: Self-organizing Wide Area Overlay Networks of Virtual Workstations" Arijit Ganguly, Abhishek Agrawal, P. Boykin, and Renato Figueiredo "Policy Driven Virtual Machine Monitor for Protected Grids" Fabrizio Baiardi, Paolo Mori, Laura Ricci, and Anna Vaccarelli "Autonomic Adaptation of Virtual Distributed

輪講スケジュール 読む本 B. Pierce: Types and Programming Languages お知らせ Bounded polymorphism 以降は秋口から行います。 参加者 大根田 末永 立沢 洪 小林 アフェルト 清木 前田 遠藤 川崎 川中 スケジュール

For English Version News (May 15, 2006) Version 0.3 が公開されました．(Changelog). (July 6, 2005) 新しいデモムービーが公開されました．仮想 8-way マルチプロセッサマシンが起動しています． (May 31, 2005) Version 0.2 が公開されました．(Changelog). (Dec 20, 2004) Version 0.1 が公開されました．(Changelog). Overview Virtual Multiprocessorは，単一システムイメージを提供するための 仮想マシンモニタです．このシステムは，ネットワークで結合された複数のマ シン上に，共有メモリ型マルチプロセッサマシンを仮想的に構築します． 例えば，N台のシングルプロセッサマシン上に，Nプロセッ サからなる仮想マルチプロセッサ

Kernel Mode Linux : Execute user processes in kernel mode Kernel Mode Linux Patch for Linux Kernel 4.0 (for IA-32, AMD64, MicroBlaze, and ARM) (last updated 2015-04-16 : version 4.0_001. ChangeLog (for 4.*). Old versions (for 4.*)) Kernel Mode Linux Patch for Linux Kernel 3.19 (for IA-32, AMD64, MicroBlaze, and ARM) (last updated 2015-04-12 : version 3.19_001. ChangeLog (for 3.*). Old versions (fo

Introduction G'Caml is a variant of O'Caml compiler which extends ML parametric polymorphism to non-parametric one, called extensional polymorphism. Freed from the clear but simple parametricity, G'Caml provides many useful features which were impossible or very hard to achieve in O'Caml, such as overloading, type safe value marshalling, ML value printer, etc., etc.. With these long awaited functi