2013-12-01から1ヶ月間の記事一覧
この記事は Theorem Prover Advent Calendar 2013 最終日 (25日目)*1の記事です. 元々このネタは, 後学期の3年生向けの実験でCoqを教える際に提示した 「挿入ソートの正当性を示す」という最終課題の模範解答を作成する際に気づいたことです. このため,…
この記事は Theorem Prover Advent Calendar 2013 最終日 (25日目)*1の記事です. 元々このネタは, 後学期の3年生向けの実験でCoqを教える際に提示した 「挿入ソートの正当性を示す」という最終課題の模範解答を作成する際に気づいたことです. このため,…