Category: Academic

Understanding Fix_eq in Coq

The problemWhen we try to prove that one general recursion defined in coq is actually correct, in the sense that the fixpoint gives exact the same result if we unfold it once. In words of Coq, it is 1

Reasoning about programs

Summary of last yearIt has been quite a long time since my last post (which is also unfinished). Lots of things has happened and changed since last blog. I’ve been interning at Apple through the end o

LaTeX and more

Since LaTeX is recommanded in VV186 and many other courses and LaTeX is unfriendly to newbies, I’m going to share my LaTeX writing style. ShareLaTeXShareLaTeX is an online LaTeX editor, and even mor