零域

useful as env Map == Dictionary building data structure. use of reflection to streamline proofs. ...

“Algorithms are the computational content of proofs.” —Robert Harper So the book material is desig ...

Basic 每次我们使用 Inductive 来声明数据类型时，Coq 会自动为这个类型生成 归纳原理。Every time we declare a new Inductive datatype, ...

relation 与injective/surjective/bijective function 等相关的知识在 5. Tactics 里，为了避免每次都要 grep 我在这里写一下。 Rela ...

123456Z ::= X;;Y ::= 1;;WHILE ~(Z = 0) DO Y ::= Y * Z;; Z ::= Z - 1END A weird convention through ...

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

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

Basic Extraction OCaml (most mature) Haskell (mostly works) Scheme (a bit out of date) 1Extracti ...