A Coq implementation of a nanopass compiler, using "Meta-Theory à la Carte" techniques

Yet an other 30 days of X challenge by Frad.

Blender Addon: Differential Growth

A Lisp interpreter implemented in Conway's Game of Life

An embeddable Scheme R7 Compiler & Runtime written in Rust

A Lisp interpreter written in untyped lambda calculus

A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.

程序员延寿指南 | A programmer's guide to live longer

Assignments of EoPL, 3rd

Minimal implementations for dependent type checking and elaboration

程序员在家做饭方法指南。Programmer's guide about how to cook at home (Simplified Chinese only).

Programming Languages: Application and Interpretation

List of Computer Science courses with video lectures.

A Coq library for abstract syntactical reasoning

Exploring Möbius transformations and implementing the book Indra's Pearls

📚 《Go语言定制指南》(原名：Go语法树入门/开源免费图书/Go语言进阶/掌握抽象语法树/Go语言AST)

📚 µGo语言实现(从头开发一个迷你Go语言编译器)

A categorized list of C++ resources.

The cuteness implementation of a dependently typed language.

A next-gen functional language

EPIT 2020 - Spring School on Homotopy Type Theory

Hygienic typed literal macros (TLMs) for Reason

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

A simple raytracer written in Lean 4

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.

A small C compiler