ReL4 Book