型安全インタプリタ

型安全インタプリタとはある言語(A)のプログラムの型安全性を、Aのインタプリタを言語(B)で書き、Bの型システムによって保証するようなものです。我々は先進的な言語機能、例えばエフェクト、コエフェクト、制御演算などに対応した型安全インタプリタの作成を目指しています。特に型安全性の証明を抽象化することで、そのようなインタプリタ定義を簡潔にできることを目標としています。

お知らせ