the parser relies on some “monadic” programming idioms basically, parser combinator (But 非常麻烦 in Coq) Lex12345678910Inducti...

Step-Indexed Evaluator…Copied from 12-imp.md: Chapter ImpCEvalFun provide some workarounds to make functional evalution work...

Basic Extraction OCaml (most mature) Haskell (mostly works) Scheme (a bit out of date) 1Extraction "imp1.ml" ce...

auto - proof search Ltac - automated forward reasoning (hypothesis matching machinery) eauto, eapply - deferred instantiatio...

又到了回顾以明得失，展望以知进退的时候。 首先想感慨一下我的拖延癌应该已经是确定到了晚期了，2018 年伊始的时候也不是没想过做一下 2017 年盘点，春节后第一次出国游走，回来之后也想着要写一个游记，而现在已经是 2019 年一月的下旬了，它俩还没...

issues on coqc module linkingSome module (e.g.Map) not foundeither maunally make map.vo or proof general can solve that. Beha...

TBD

TBD

TBD

Recall Big-step Pros & ConsBig-step 一步到位 : eval to its final value (plus final store) Pros - natural (so called natura...