システムFの正式な実装とは何ですか？

Question

System Fは、プロトタイプをプログラミングするときに型を単純に判断するのに最適です。それを自分で実装する以外に、既存の実装を使いたいと思います。

実装を探しているときは、何もないように見えます。なぜそうはわかりません。

私の質問はシステムFの標準的な実装とは何ですか？

Answer 1

Types and Programming Languages B.C. Pierceは、OCamlでタイプされたラムダ計算のimplementationsを提供し、議論することで有名です（とりわけ）。

本はfullpolyと呼ばれるシステムFの実装を提供し、第25章fullpolyでの実装の詳細を説明するブール値とsimply-typedラムダ計算の実装を拡張 - simplebool。

これらの型チェッカーと通訳の作成と実行の手順はhereです。