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
Category theory appears everywhere when I learn things, so I'd better learn it systematically. This article writes about what is Category and some examples.
Notes for the sixth HoTT course of HoTTEST Summer School 2022
Notes for the fifth HoTT course of HoTTEST Summer School 2022
Notes for the fourth HoTT course of HoTTEST Summer School 2022