PPL 2015：招待講演

橋本和幸 （NVIDIA. 元日本シンボリックス株式会社）

概要

Symbolics社は、1981年に設立されたLispマシンの専業メーカーで、既に倒産して現存していない。MIT AI Lab.で開発されたLM-2をベースに、独自の36ビットアーキテクチャを開発し商用Lispマシンとしての販売に成功し、NewYork証券取引所に上場しました。　Symbolics社では、HardwareだけでなくOperating Systemから開発ツール、アプリケーションソフトウェアまで開発を行っていた。会社の基本コンセプトは、"Software First"　最初にソフトウェアありき。Hardwareは、ソフトウェアを実行するために設計されるべきだという考えのもと、Operating SystemからObject Oriented Programing Modelで設計されており、それを現実的な速度で実行するためのCPUを設計していた。特徴的な機能は、実行時の型チェックとその結果に応じた関数呼び出しや、型変換を行うことと、高速なメッセージパッシングのための専用のキャッシュを装備していた。

オブジェクト指向言語として、Zatalispの拡張となるFlavorsが当初より実装されていた。特徴としては、多重継承機能。その後、CommonLispの制定後、CommonLispの拡張としてCLOS（CommonLisp Object System）が制定された。それに伴い、SymbolicsCommonLispの拡張としてCLOS互換のNewFlavorsが提供されるようになった。またこのCommonLispへの移行に伴い、OSもGeneraと命名された。NewFlavorsの特徴ひとつは、Generic Fucntionである。Lisp関数とObjectのメソッド呼び出しを同一のフォーマットとして、引数の型によって最適な呼び出しを実行時に選択していた。

もっとも大規模なアプリケーションとして、3D Computer Graphics の製作システムがあった。このアニメーションシステムは、MITでのActor理論をベースに開発されていた。また形状モデリングソフトウェアも、Object Oriented Programing Modelで記述されており、多重継承を非常にうまく実装していた。3DCGの製作環境では実行速度が重視されるため、LispですがSillicon Graphics社のUNIXワークステーション上のC言語で記述されたシステムに、劣らないパフォーマンスを実現していた。

Symbolicsの環境の機能とともに、それらから感じられたメリット及び欠点などを紹介していく。

Machintosh IIFXにSymbolicsのIvoryカードを搭載したもので、Symbolics Generaの実機デモを行う予定です。 ただし20年前の機材なので、動作しない場合はご了承ください。

講演者の略歴

経歴

• 86年 中央大学理工学部卒業、
• 86年 日本シンボリックス株式会社 AI、3DCGの技術担当
• 95年 株式会社スクウェア 入社 プログラマー CG技術統括、
• 96年 スクウェアLA VP Technology就任
• 98年 スクウェアUSA ホノルルスタジオ VP R&D
• 00年 株式会社スクウェア 執行役員 研究開発担当 就任,
• 00年 スクウェアUSA SVP CTO 就任
• 02年 エレクトロニック・アーツ社 Vice President Technology, New Platform 就任
• 06年 Avatar Reality社 設立 President就任
• 12年 NVIDIA Japan シニアディレクター・エンタテインメント テクノロジー 就任

職務略歴

Chung-Kil Hur (Seoul National University)

概要

My long-term research goal is to establish a solid foundation for the C/C++ language, which requires a "simple" semantics of C/C++ and a "correct" compiler. For this, we will develop (i) a simple formal semantics of C supporting all practically used features such as integer-pointer casts; and (ii) a verified translation validator for the full LLVM compiler. Achieving both (i) and (ii) is not particularly easy because a simple semantics usually fails to justify many compiler optimizations.

In this talk, I will give a high-level introduction to our project including many technical problems that arise on the way. Then, I will present our solutions to two of the problems. One is to give a simple memory model that supports integer-pointer casts, yet still justify most of the existing compiler optimizations. The other is to give a new reasoning principle for coinduction that does not require any syntactic guardedness checking. We formalized this theory as Paco library for Coq, which made our coinductive reasoning for compilation validation a lot easier.

講演者の略歴

Chung-Kil Hur is an assistant professor in Department of Computer Science and Engineering at Seoul National University. Previously he worked as a postdoctoral researcher at Microsoft Research Cambridge, Max Planck Institute for Software Systems (MPI-SWS) and Laboratoire PPS. He obtained a Ph.D. from University of Cambridge and a B.Sc. in Computer Science and in Mathematics from Korea Advanced Institute of Science and Technology (KAIST). He also received a bronze medal in the 35th International Mathematical Olympiad (IMO) in 1994. His research interests are in software verification, interactive theorem proving, probabilistic programming and Beyesian inference.