LLVM IR heavily relies on branching statements to represent control flow. However, for low-level languages targeting stack-based VMs, like WebAssembly, there are no direct instructions corresponding to branching. Therefore, we need an algorithm to convert the IR into acceptable code.

This article writes about what is functor, contravariant functor, bifunctor, profunctor and faithful/full functor.

Recently someone asked me for help of drawing a graph in LaTeX. And we found that tikz is surprisingly hard to use, the official document is too long to find anything useful and the unofficial document is always stale. So I created this.

This article writes about epis, monos, products, coproducts,etc.

mem2reg is one of the most important passes in LLVM. However, I didn't find a good tutorial for me. All the tutorials I found just throw me either a pile of code or several papers, without a more intuitive explanation. So I wrote this.

We all have learned elementary geometry in high school. Now let's try to prove some elementary geometry theories in Agda!

A brief introduction about decidability related things and their usage in Agda

Now I'm reading LOGIC IN COMPUTER SCIENCE to relearn (and dig deeper) the little bit of mathematical logic I've learnt at university...This article is about binary decision diagrams

Now I'm reading LOGIC IN COMPUTER SCIENCE to relearn (and dig deeper) the little bit of mathematical logic I've learnt at university...This article is about modal logic

I'm reading LOGIC IN COMPUTER SCIENCE to relearn (and dig deeper) the little bit of mathematical logic I've learnt at university...This article is about proof based program verification