Development Resource

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

Nix

• FHS Environment

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][https://arxiv.org/pdf/2303.12254] An implementation of Fexprs that suppose to be pretty fast.

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

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

Other languages

• Julia: A Fresh Approach toNumerical Computing

Memory management

• Visualizing memory management in Golang
• TCMalloc : Thread-Caching Malloc
• A visual guide to Go Memory Allocator from scratch (Golang)

Concurrency

• Scheduling In Go (Series)

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

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][https://dl.acm.org/doi/pdf/10.1145/99370.99385] A great paper on the foundations of laziness in GHC
• [GHC's code generation][https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compiler/generated-code]
• Making a Fast Curry: Push/Enter vs Eval/Apply for Higher-order Languages

Linker

• 20 part linker essay
• LLD Usage

Toolchain

• Building LLVM Distribution

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

Type Theory

• Homotopy Type Theory

• No, dynamic type systems are not inherently more open

• 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

• The Works of Per Martin-Löf:

  • 1972
  • 1979
  • 1984
  • The Complete 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

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