第17回プログラミングおよびプログラミング言語ワークショップ（PPL2015）
プログラム

概要  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.

概要  Symbolics社は、1981年に設立されたLispマシンの専業メーカーで、既に倒産して現存していない。MIT AI Lab.で開発されたLM-2をベースに、独自の36ビットアーキテクチャを開発し商用Lispマシンとしての販売に成功し、NewYork証券取引所に上場しました。　Symbolics社では、HardwareだけでなくOperating Systemから開発ツール、アプリケーションソフトウェアまで開発を行っていた。会社の基本コンセプトは、"Software First"　最初にソフトウェアありき。Hardwareは、ソフトウェアを実行するために設計されるべきだという考えのもと、OperatingSystemから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年前の機材なので、動作しない場合はご了承ください。