Bibliography
This page exists to collect/organize references to papers and other documents relevant to the theory of Anselm.
Type Theory
- Inductive Types Deconstructed Stefan Monnier
Effects
Do Be Do Be Do Sam Lindley et al.
Overview of the Frank programming language.
Handlers in Action Ohad Kammar et al.
Nice discussion of the benefits of shallow vs. deep handlers.
Call-By-Push-Value
Call-By-Push-Value: A Functional/Imperative Synthesis, Paul Levy
Contains the most comphrensive account of the theory of CBPV
A Formal Equational Theory for Call-By-Push-Value, Christine Rizkallah et al.
OOP
Recursive Object-Oriented Modules, Keiko Nakata et al.
Selective Open Recursion: Modular Reasoning about Components and Inheritance Jonathan Aldrich et al.
Staging
A Gentle Introduction to Multi-stage Programming, Walid Taha
Contains a nice overview of MSP.
Termination
A tutorial on type-based termination, Gilles Barthe et al.
Termination Casts: A Flexible Approach to Termination with General Recursion, Aaron Stump et al.
Regions
A Type System for Reachability and Acyclicity, Yi Lu et al.
Linear Regions Are All You Need, Matthew Fluet et al.
On Regions and Linear Types, David Walker et al.
Equality
Pattern Matching
Type Classes (and related features)
On the Bright Side of Type Classes:Instance Arguments in Agda
Canonical Structures: Programmable type classes and implicits
Implementing Tactics and Tacticals in a Higher-Order Logic Programming Language