Bibliography

The sources behind the language: the philosophy that drops bound data, the effect system, the quantities that make dependent types sound with reference counting, the memory model, pattern matching, the property checker, and the compiler's architecture. Every entry is a source the README, the specification or the plans rely on. Where the repository cites only a tool or an overview, the primary paper is listed beside it. The spec chapter that relies on a source is linked where it matters.

Capabilities instead of data

• W. V. O. Quine, Predicate-functor logic, Proceedings of the Second Scandinavian Logic Symposium, North-Holland, 1971 — first-order logic without bound variables, using five combinators on predicates; the model for capabilities as predicate functors over the type universe. (overview)
• John A. De Goes, Death of Data (blog) — functions that traffic in concrete types commit prematurely to a representation; declare the operations instead.
• Jacques Carette, Oleg Kiselyov & Chung-chieh Shan, Finally tagless, partially evaluated (JFP 19(5), 2009) — programs written against an abstract interface, with the interpreter choosing the semantics; Fixed applies the encoding to a whole language, and the compiler is the interpreter. (lecture notes)
• Rethinking Data and Codata through Matrix Transposition (blog) — the data/codata duality behind the match vs fold split.

Algebraic effects

• Gordon Plotkin & Matija Pretnar, Handlers of Algebraic Effects (ESOP 2009) — the semantic model of effects and handlers. (Effects)
• Daan Leijen, Type directed compilation of row-typed algebraic effects (POPL 2017) — the evidence-passing compilation strategy Fixed adopts.
• Ningning Xie & Daan Leijen, Generalized evidence passing for effect handlers (ICFP 2021) — efficient compilation of handlers to C; the refinements Koka ships.
• The Koka language — the closest production reference: row-typed effects, evidence passing, Perceus, FBIP. Fixed adopts all of them and removes named data types.

Quantities

• Robert Atkey, Syntax and Semantics of Quantitative Type Theory (LICS 2018) — the 0/1/ω usage model that keeps dependent types sound with reference counting. (Quantities, paper page)
• Edwin Brady, Idris 2: Quantitative Type Theory in Practice (ECOOP 2021) — a production implementation; Fixed follows its inference shape.
• Philip Wadler, Linear Types Can Change the World!, Programming Concepts and Methods (IFIP TC2), 1990 — the intuition that a value used once can be updated in place.

Memory: Perceus and reuse

• Alex Reinking, Ningning Xie, Leonardo de Moura & Daan Leijen, Perceus: garbage free reference counting with reuse (PLDI 2021) — the core algorithm; Fixed's addition is driving dup/drop from QTT quantities. (Perceus)
• Anton Lorenzen & Daan Leijen, Reference counting with frame limited reuse (ICFP 2022) — the refinement of reuse that shapes FBIP in Fixed.

Pattern matching

• Luc Maranget, Compiling pattern matching to good decision trees (ML Workshop 2008) — the reference algorithm for exhaustiveness, usefulness and decision trees. (Pattern matching)
• Alexander Krauss, Pattern Matching in Theorem Proving — nested-pattern reasoning.
• Benjamin C. Pierce, Types and Programming Languages (MIT Press, 2002), ch. 11 — the pattern-typing rules.

Properties and verification

• C. A. R. Hoare, An axiomatic basis for computer programming (CACM 12(10), 1969) — preconditions and postconditions; the pattern behind prop. (Properties)
• Robert W. Floyd, Assigning Meanings to Programs, Mathematical Aspects of Computer Science, AMS, 1967 — verification conditions.
• Philipp Rümmer, A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic (LPAR 2008) — the calculus behind Princess, the JVM prover the typer uses to discharge prop obligations statically.
• Koen Claessen & John Hughes, QuickCheck: a lightweight tool for random testing of Haskell programs (ICFP 2000) — the property-based testing model for obligations the prover cannot close.

Compiler architecture

• Scala 3 compiler (dotc) — the phase plan, span-identified trees, and bidirectional typer Fixed's compiler follows; distilled in the compiler reference.
• Aleksander Boruch-Gruszecki, Martin Odersky, Edward Lee, Ondřej Lhoták & Jonathan Brachthäuser, Capturing Types (TOPLAS 2023) — Scala's capture checker, the closest existing problem to tracking capabilities through a typer. (reference)

Repository evidence

• Implementation plan — the phases, their milestones and the open design questions.
• Phase 3 typer plan — the type checker in progress.
• Design decisions — one record per resolved language question.
• Grammar — the EBNF the parser implements.
• Examples — the eleven programs that drive the design; the whole corpus parses with zero diagnostics.