2019-12-01から1ヶ月間の記事一覧

formalized-egison -- Egisonの型安全性の証明に向けて

概要 Egisonのパターンマッチの動作を定理証明支援系Coq上で定義し、「Egisonの処理系が項Mを値vに評価する」という命題をCoq上で表現できるようにしました。 動機 Egisonの中核的な機能はユーザが拡張可能なパターンマッチ機構です。例えば以下に示すように…