Hands-on implementations of type systems, interpreters, and related concepts. Includes exercises from TAPL, PLAI, Software Foundations, and other sources.
Concepts tracker: Notion
Flashcards: Notion
Companion projects:
- dboxide: A rewrite of DBML in Rust, learning from
rust-analyzer.
I would be glad if anyone helps me point out the error that I made or enlighten me on some aspects.
This project uses Nix for reproducible development environments.
- Author: Benjamin C. Pierce
- Language: OCaml
- Link: MIT Press
The definitive textbook on type systems. Covers type systems, operational semantics, lambda calculus, subtyping, polymorphism, and type reconstruction.
- Author: Shriram Krishnamurthi
- Language: Typed Plait (Racket)
- Link: plai.org
An interpreter-based approach to programming languages. Covers parsing, desugaring, interpreters, environments, mutation, objects, type systems, and continuations.
- Authors: Benjamin C. Pierce et al.
- Language: Coq/Rocq
- Link: softwarefoundations.cis.upenn.edu
A series of electronic textbooks on the mathematical underpinnings of reliable software using the Coq proof assistant.
Volumes:
- LF — Logical Foundations
- PLF — Programming Language Foundations
- VFA — Verified Functional Algorithms
- QC — QuickChick: Property-based testing