In this repository, I will publish my notes for GaTech's Advanced Operating Systems course (CS6210).

Randomized Property-Based Testing Plugin for Coq

⏰ Collaboratively track deadlines of conferences recommended by CCF (Website, Python Cli, Wechat Applet) / If you find it useful, please star this project, thanks~

Book of Elementary Functional Algorithms and Data structures

A textbook on informal homotopy type theory

《软件基础》中译版 Software Foundations Chinese Translation

Random collections of my interested research papers / projects

Repo for counting stars and contributing. Press F to pay respect to glorious developers.

955 不加班的公司名单 - 工作 955，work–life balance (工作与生活的平衡)

The DeepSEA programming language

做题

一份硬核(hardcore)计算机科学CS自学计划，偏向软件工程和系统架构方向

LLVM IR入门指南

更新2008年版本的《上海交通大学生存手册》gitbook发布于https://survivesjtu.gitbook.io/survivesjtumanual/

The Vellvm (Verified LLVM) coq development.

Verified Software Toolchain

Several OS labs from IPADS@SJTU

Git Source Code Mirror - This is a publish-only repository but pull requests can be turned into patches to the mailing list via GitGitGadget (https://gitgitgadget.github.io/). Please follow Documen…

How to create an OS from scratch

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive develo…

A Library for Representing Recursive and Impure Programs in Coq

Compositional CompCert

The CompCert formally-verified C compiler

Rust version of THU uCore OS. Linux compatible.

👨‍💻 ❤️ 💻 上海交通大学计算机系本科作业参考

更新2008年版本的《上海交通大学生存手册》gitbook发布于https://survivesjtu.gitbook.io/survivesjtumanual/