Notes on Type Theory

Here are some notes about type theory, mainly from the book Type Theory and Formal Proof: An Introduction.

An Impulse Engine in Rust and WebAssembly

This is a simple 2D physics engine that simulates rigid body dynamics using impulse-based methods. It is written in Rust and compiled to WebAssembly.

Integer Factorization and RSA

This article is the final report of CSCI5440: Theory of Cryptography. I summarized the mathematical details of factoring algorithms and RSA.

Raspberry Pi 3 Bare Metal in Rust

I bought a Raspberry Pi 3 several days ago. Playing with Linux seems boring for me, so I decided to pay some attention on ARM architecture. There are a lot of documents about bare metal development of Raspberry Pi, but almost all of them are using C & assembly. Since I’m learning Rust these days, it should be fun to try to implement something using Rust.

CUHK Quick Setup Guide

Although I used to be an RA at CUHK, it still cost me nearly two weeks to setup everything on my desktop. Here is the recording.