References

Curated reading and resources that inform the design and implementation of Serene — across type theory, compilers, runtimes, and language design.

Haskell

• Megaparsec tutorial
• Parser Combinators in Haskell
• https://www.learnyouahaskell.com/
• Static binaries with Haskell
• Compiling a functional language to LLVM
• An introduction to typeclass metaprogramming
• Error reporting made easy
• Existential Haskell
• Falsify: Hypothesis-inspired shrinking for Haskell
• Fast Haskell: Competing with C at parsing XML
• hasp: Writing a Lisp Interpreter in Haskell
• Typeclassopedia
• Why GADTs matter for performance
• lens (optics) — composable getters/setters used across the lscz AST.
• You could have invented free monads — the idea behind the free package.
• An introduction to recursion schemes — folding/unfolding ASTs.
• Hedgehog — property-based testing.
• relude — the alternative prelude lscz builds on.

Nix

• FHS Environment
• Zero to Nix — a friendly intro to Nix flakes.

Lisp

• Fexprs as the basis of Lisp function application
  An alternative to macros

• Realistic Compilation By Partial Evaluation
  Fexpr related paper Fexprs as the basis of Lisp function application

• Practical compilation of fexprs using partial evaluation An implementation of Fexprs that suppose to be pretty fast.

Macros

• Structure and Interpretation of Computer Programs (SICP) — the classic on evaluators and metalinguistic abstraction.
• Macros That Work — Clinger & Rees; hygienic macro expansion done right.
• Hygienic macro expansion — Kohlbecker et al; where hygiene started.
• Fear of Macros — a hands-on, modern macro tutorial (Racket).

LLVM

• Brief Overview of LLVM
• A bit in depth details on LLVM
• Official LLVM tutorial C++
• Interactive C++ with Cling
• My First LLVM Compiler
• A Complete Guide to LLVM for Programming Language Creators
• LLVM Internals
• How to learn about compilers (LLVM Version)
• Compiling a functional language to LLVM
• Micro C
• MLIR: A Compiler Infrastructure for the End of Moore's Law — the framework Serene's C++/MLIR era was built on.

TableGen

• Create a backend

Data Structures

• Pure functional datastructures papaer
• Dynamic typing: syntax and proof theory
• Representing Type Information in Dynamically Typed Languages
• An empirical study on the impact of static typing on software maintainability
• Mapping High Level Constructs to LLVM IR
• Ideal Hash Trees — Bagwell; the basis for the runtime's HAMT maps and vector-trie seq.
• Optimizing Hash-Array Mapped Tries (CHAMP) — Steindorfer & Vinju; the map design the runtime cites.
• Understanding Clojure's Persistent Vectors — the clearest explanation of vector tries.

Other languages

• Julia: A Fresh Approach toNumerical Computing
• The implementation of functional programming languages

Memory management

• Visualizing memory management in Golang
• TCMalloc : Thread-Caching Malloc
• A visual guide to Go Memory Allocator from scratch (Golang)
• What Every Programmer Should Know About Memory — Drepper; caches, alignment, allocation.

Concurrency

• Scheduling In Go (Series)
• Revisiting Coroutines — de Moura & Ierusalimschy; the semantics of stackful coroutines/fibers.
• Dynamic Circular Work-Stealing Deque — Chase & Lev; the deque the fiber scheduler implements.
• Correct and Efficient Work-Stealing for Weak Memory Models — Lê, Pop, Cohen & Zappa Nardelli; cited in the scheduler for the atomics.

Asynchronous I/O

• Efficient IO with io_uring — Axboe; the design of io_uring (the reactor backend).
• liburing — the library the reactor uses.
• libuv design overview — an alternative event loop the project has used.

Garbage collection

• GC on V8
• Perceus: Garbage Free Reference Counting with Reuse
• Boehm GC
• MPS
• MMTK
• Whiro
  This is not GC but a tool to debug GC and memory allocation.

JIT

• Machine code generator for C++
• LLVM's Next Generation of JIT API

Optimizations

• Canonicalization

Hashing & text

• xxHash — Collet; the runtime's hash function (third_party/xxhash.h).
• Hacker's Delight — Warren; popcount and the bit tricks behind HAMT indexing.
• The WTF-8 encoding — Sapin; Serene strings follow this (rt/strings.h).

Compiler

• Stack frame layout on x86-64
• Pointers Are Complicated
• Pointers Are Complicated III, or: Pointer-integer casts exposed
• A compiler writting journal
• The Spineless Tagless G-machine A great paper on the foundations of laziness in GHC
• GHC's code generation
• Making a Fast Curry: Push/Enter vs Eval/Apply for Higher-order Languages
• System V AMD64 ABI — calling conventions, register usage, stack alignment (the fiber context switch follows it).
• An Introduction to Lock-Free Programming — Preshing; the C/C++ memory model in practice.
• cppreference: memory order — the precise semantics of the atomics used throughout the scheduler.
• Threads Cannot Be Implemented as a Library — Boehm; why the memory model matters.

Linker

• 20 part linker essay
• LLD Usage

Toolchain Related

• Building LLVM Distribution
• Meson build system — builds the C runtime.

Cross compilation

• Creating portable Linux binaries
  A nice to read article on some of the common problems when linking statically with none default libc or libc++

Lang

• Scheme
  • Chicken Scheme - Easy-to-use compiler and interpreter, with lots of libraries
  • Stalin - Brutally optimizing Scheme compiler, with lots of optimization flags

• Crafting Interpreters

Emacs mode

• Adding A New Language to Emacs
• The Definitive Guide To Syntax Highlighting
• NewLisp
  A lisp based on Fexprs

Mathematics

• CS410 course: Advance Functional Programming
  If you need to learn Agda (We use it for the mathematics side of Serene, to proof certain features) check out

• Programming Language Foundations in Agda
  This book is an introduction to programming language theory using the proof assistant Agda.

• Logic and linear algebra: an introduction
  An introduction to linear algebra that can be used to model concurrency in Serene

Curry-Howard correspondence

• The formulae-as-types notion of construction
• Propositions as Types (paper) — Wadler.

Type Theory

• Homotopy Type Theory

• No, dynamic type systems are not inherently more open

• A tutorial implementation of a dependently typed lambda calculus (LambdaPi) — Löh, McBride & Swierstra; a "build a tiny dependent checker" walkthrough.

• Practical Foundations of Programming Languages

  • Online copy (2nd Edition Preview)
  • Dead-tree copy (2nd Edition)

• Types and Programming Languages

  • Online supplements
  • Dead-tree copy

• Advanced Topics in Types and Programming Languages

  • Online supplements
  • Dead-tree copy

• A Library of papers on Dependent Type Theory:

  • Dependent Type Theory Library

• The Works of Per Martin-Löf:

  • 1972
  • 1979
  • 1984
  • The Complete Works of Per Martin-Löf
  • The collected works of Per Martin-Löf

• Programming In Martin-Löf's Type Theory

• The Works of John Reynolds

  • Types, Abstraction and Parametric Polymorphism
  • Parametricity for System F
  • A Logic For Shared Mutable State
  • Course notes on separation logic
  • Course notes on denotational semantics

• The HoTT book

• Student's Notes on HoTT

• Materials for the Schools and Workshops on UniMath

• Dependently typed programming with singletons ACM or brynmaw

Quantitative Type Theory

• Syntax and Semantics of Quantitative Type Theory — Atkey; defines QTT (Serene's 0/1/ω quantities).
• I Got Plenty o' Nuttin' — McBride; the precursor motivating resource tracking.
• Idris 2: Quantitative Type Theory in Practice — Brady; QTT in a real implementation.

Bidirectional type checking

• Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism — Dunfield & Krishnaswami (cited in the spec).
• Bidirectional Typing (survey) — Dunfield & Krishnaswami; the whole design space.
• A judgmental reconstruction of modal logic — Pfenning & Davies (cited in the spec for the judgmental rules).

Normalization by evaluation & elaboration

• elaboration-zoo — Kovács; the best practical NbE + elaboration resource.
• Normalization by Evaluation: Dependent Types and Impredicativity — Abel; the theory behind NbE for dependent types.

Idris2 (the lscz2 host language)

• Idris2 documentation — the manual.
• Type-Driven Development with Idris — Brady; the book.

Proof Theory

• Frank Pfenning's Lecture Notes

  • Introductory Course
  • Linear Logic
  • Modal Logic

• Proofs and Types

• The Blind Spot: Lectures on Logic

• Mustard Watches: An Integrated Approach to Time and Food

Category Theory

• Category Theory in Context

  • Online version
  • Dead-tree version
  • The author's post on the book

• Practical Foundations of Mathematics

  • HTML version
  • Dead-tree version

• Category Theory

• Ed Morehouse's Category Theory Lecture Notes

• Categorical Logic and Type Theory

  • Jacob's thesis, containing much of what went into the book
  • A definitely not suspicious online copy
  • Dead-tree copy

• Introduction to Higher-Order Categorical Logic

• Sheaves in Geometry and Logic

Others

• Gunter's "Semantics of Programming Language"

• Abramsky and Jung's "Domain Theory"

• Realizability: An Introduction to Its Categorical Side

• OPLSS:
  The Oregon Programming Languages Summer School is a 2 week long bootcamp on PLs held annually at the university of Oregon. It's a wonderful event to attend but if you can't make it they record all their lectures anyways! They're taught be a variety of lecturers but they're all world class researchers.

  • 2012
  • 2013
  • 2014
  • 2015
  • 2016
  • 2017
  • 2018

• SIGPLAN Conferences

• SIGPLAN

• An index of research confs