Recent Posts
-
FP in Haskell - Practical ConcernsPartial Functions, Folds and as-pattern
-
Simple Imperative ProgramDefine, evaluate, reasoning about a toy imperative program.
-
Relation PropertiesPlay with math ideas in Coq.
-
ContainersAbstract Interface and Data Structure
-
Induction Principlesthe underlying mechanism of the tactic `induction`.
-
Proof ObjectsThe Curry-Howard Correspondence.