serene/docs/pages/resources.md

title
Resources

Development Resource

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)

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

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

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

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.

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

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