Programming Languages.
Programming Languages/Compilers/Interpreters
Heavily inspired from here
Theory
- Theory of Computation by Michael Sipser
- Types and Programming Languages
- Classical Papers in PL, recommendations
- PL-Compilers-Resources
- All you need is call/cc
- Racket evaluation model(has a bit of stuff on continuation)
- Racket continuations
- Type System for Memory Safety(another banger by borretti)
- Programming Languages Research (many papers and links consolidated here)
- How to read inference rules
- How to implement effect handlers
- How should I read type system notation?(by lexilambda)
- ACM India summer School on PL and optimizations
- ACM India Summer School on Programming Languages(Thing of more interest is Program Semantics lectures(done in F*))
- ACM Summer School on Compiler Design and construction(uses some llvm)
- PL Semantics by Graham Hutton
- Getting Started with Category Theory
- NUPRL - 10 papers that all PhD students in programming languages ought to know, for some value of 10
- What does it mean for a type system or language to be "sound"?
- Normalization by Evaluation Four Ways: Reconstructing NbE Designs from First Principles
- Parametric Higher-Order Abstract Syntax , HOAS
- The precise definition of Normalization By Evaluation?
- Normalization by Evaluation, Agda
- Normalisation by Evaluation in the Compilation of Typed Functional Programming Languages - Sam Lindley Thesis
- Zulip Chat Archive - Subject Reduction
- Zulip Chat Archive - What is the subject reduction debate?
- Subject reduction in Lean
- How much of trouble is Lean's failure of normalization, given that logical consistency is not obviously broken?
Overview
Compiler Architecture
- How the TypeScript Compiler Compiles - understanding the compiler internal
- Anders Hejlsberg on Modern Compiler Construction
- AOSA book: LLVM
Parsing
JIT
- Adventures in JIT Compilation
- Rhizome - a JIT for Ruby, implemented in pure Ruby
- Kipply's blog(lots of content relating to JIT)
Functional Languages
- The Implementation of Functional Programming Languages - by Simon Peyton Jones
- Compiling Functional Languages to LLVM, a series(Lots of other cool articles as well in blog about typeclasses)
GC
- Baby's First Garbage Collector
- The Garbage Collection Handbook
- Oilshell "Pictures of a working garbage collector"(Goldmine for garbage collector stuff, see the whole blog)
- Modern Garbage Collection(HN Discussion) Part 1 Part 2
- Boehm-Demers-Weiser Garbage Collector(Has papers linked in the GitHub repo)
- Understanding GC in JSC From Scratch
- Riptide,Webkit's GC
- High Performance GC for C++
- Precise Stack Scanning in C++
- GC Resources, Thorsten Ball
- Whippet, towards a new local maximum(more posts about GC present in the site)
- Deep Dive into ZGC, a modern garbage collector
- Memory Allocation Strategies
- LuaJIT quad color GC
Compiler Optimizations
Educational Projects
- chibcc by Rui Ueyama
- Multi-Language Programmable Linter
- NEAL(Language agnostic code analysis tool)
- AST Grep tool
- Comby, Tool for searching and changing code structure
- Parser Parser Combinators(Talk about Comby)
- Making a Language(information about typechecker, looks good)
- GCC Translation Validation(uses smt with gcc)
- Not exactly educational, but FStar wiki seems very comprehensive(I want to read all of this sooo badly)
- Hackett by lexilambda
- labrys
- llvm-tutor
- lura(IDE focused programming language study)
- Soft(Lisp that compiles to LLVM)
- Wasm reference interpreter in OCaml
- Mukul Rathi's Bolt(has a series of blog posts explaining implementation)
- Carbon Design Documents
- Trustfall(super cool thing)
- Extensive tutorial of Hindley Milner
- Write your own tiny programming system(s) (Hindley-Milner, OOP, Prolog,etc implementation)
- Type systems in ocaml
Virtual Machine
- How to Build a Virtual Machine
- Small VMs and coroutines HN Lobsters
- Faster Virtual Machines Lobsters
- Interesting things about the Lua Interpreter(HN post link)
- Writing Interpreters in Rust
Misc Compilers
- Cranelift Stuff(Reg Alloc, Instruction Selector etc, a series of blogs)
- Let's write a setjmp(HN Discussion)
- Design of Austral Compiler(See other articles as well to see more about typechecker)
- What Austral Proves(Lobsters discussion and link)
- Fibers, Oh My!
- Dmitry Vyukov — Go scheduler: Implementing language with lightweight concurrency
- Phil Eaton's Favourite Compiler and Interpreter Resources
- JVM Internals by Aleksey Shipilev
- Max Bernstein(tekknolagi) pl resources
- A lisp compiler and interpreter writing series by tekknolagi
- How to compile with continutations
- Design roadmap about YSH(by oilshell guy)
- Tao programming language(has so many cool features,see how they're implemented)
- Alexis King - “Effects for Less” @ ZuriHac 2020(content is just madd) , GHC proposal link
- Blog for Kalyn(Compiled Typed Haskell like Lisp)
- Alexis King - "Delimited Continuations, Demystified", same talk ZuriHac 2023
- GHC Reading List
- Mapping High level constructs to LLVM IR
- Program Analysis Resources(very comprehensive)
- Learning Resources for Clang libraries
- Compiler Optimizations
- Algebraic Effects for the Rest of Us
Linkers
Courses and Assignments
- CIS 341 - Compilers(Has very nice assignments)
- CSE 131 - Compiler Construction(Haskell)
- CSE 131 - Compiler Construction(Ocaml)
- CSE 131/231- Compiler Construction(Rust)
- CMU Compilers Course by Jan Hoffman
- Essentials of Compilation Course and Book
- Course on VMs and Managed Runtimes
- (Book)Design and semantics of PL, in Scala
- Programs and Proofs
- Software Foundations(Course Cornell)
- Software Foundations Books
- An introduction to creating a C compiler for those who want to know the lower layers(In Japanese, so have to translate)
- PL Class by Edward Z Yangz, materials link( i think )
- Advanced Functional Programming(in Agda with videos)
- Programming languages(follows TAPL and content looks great)
- Xavier Leroy - Program logics: reasoning principles for high-assurance software
- Xavier Leroy - Mechanized semantics: when machines reason about their languages
- Xavier Leroy - Programming = proving? The Curry-Howard correspondence today
- Xavier Leroy - Control structures
Theorem Provers
- Logic and Proofs in Lean(3?)
- Theorem Proving in Lean4
- Mathematics in Lean
- Mechanics of Proofs
- What is the difference between Gallina and Ltac?
- Coq <-> Lean4 Tactics Cheat Sheet
- Lean Tactic Reference
- Logic and Computation Course, uses Lean 4
- Lean 3 Type theory
- Typechecking in Lean4
- Lean4Lean
- Semantics Course in Coq/Rocq - Saarland University
- A Logical Approach to Type Soundness
- Iris Tutorial , Iris Lecture Notes
- PulseCore: A Dependently Typed Stratified Separation Logic
- Hitchhiker's Guide to Logical Verification - Lean4
Some Cool stuff I've found
- How does this work??? (Mulligan)
- Garbage collection with zero cost at non-GC time
- Why is Idris 2 much faster than Idris 1?
- Making more out of traits(Rust) and many other discussion about Rust language design
- New research programming languages thread Reddit
Dependent Types
- A tutorial implementation of a dependently typed lambda calculus (LambdaPi)
- OCaml Discuss - Dependent Types in the Purest Form
- Swift Discuss - [Pitch] Dependent Types & Universes (Stage 1 of Proof-Driven Development?)
- Dependent Theory of Types
- Online reference book for implementing concepts in type theory, Answererd by Andras Kovacs