Where the ideas come from

Alpha combines several traditions. These sources are conceptual ancestors and close comparisons, not claims that Alpha directly implements any one paper.

S-expressions and symbolic syntax

Alpha's parenthesized prefix forms belong to the Lisp S-expression tradition. John McCarthy's 1960 paper introduced symbolic expressions and recursive functions over them: Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I, DOI.

Dependent type theory and propositions as types

Dependent functions, dependent pairs, universes, equality, and proof terms belong to Martin-Löf type theory. A foundational source is Per Martin-Löf's Intuitionistic Type Theory.

Inductive families and eliminators

Peter Dybjer's Inductive Families develops formation, introduction, elimination, equality, positivity, and recursion for indexed inductive definitions. It is the closest background for Alpha's family, constructor, field, recursive, eliminate, and branch vocabulary.

Practical dependent programming

Hongwei Xi and Frank Pfenning's Dependent Types in Practical Programming, DOI, shows how dependent indices can improve realistic ML-style programs. Xi's later ATS account connects theorem-oriented types with low-level systems work.

Linear logic and linear types

The idea that values may need exact-use discipline comes from linear logic and its programming interpretations. Philip Wadler's Linear Types Can Change the World! is a classic programming account. Linear Haskell shows higher-order polymorphic linearity in a modern language.

Quantitative type theory

Robert Atkey's The Syntax and Semantics of Quantitative Type Theory combines dependency with variable-use information. Edwin Brady's Idris 2: Quantitative Type Theory in Practice demonstrates QTT for erasure and resource protocols in a full language. These are useful frames for Alpha's erased, affine, linear, and unrestricted quantities.

Type-and-effect systems

John Lucassen and David Gifford's Polymorphic Effect Systems established a polymorphic discipline where static descriptions include returned values and possible effects. Alpha's concrete rows and computation types are its own design, but share that goal of making side effects statically visible.

Values versus computations

Paul Blain Levy's Call-by-Push-Value thesis gives a clear account of separating values from computations and organizing effects around that distinction.

Proof erasure and verified low-level programming

Proof-carrying source becomes practical when static evidence can disappear without changing runtime meaning. Verified Low-Level Programming Embedded in F* describes Low*, where specifications and proofs erase before predictable low-level extraction.

Compiler correctness

Xavier Leroy's A Formally Verified Compiler Back-end and CompCert are landmarks for machine-checked semantic preservation in a realistic compiler.

Bidirectional checking

Rich type systems often divide work between synthesizing a type from a term and checking a term against an expected type. Jana Dunfield and Neel Krishnaswami survey the design space in Bidirectional Typing.

Alpha's synthesis

Alpha's distinctive claim is the composition: dependent and quantitative source terms, explicit effects, proof erasure, typed compiler artifacts, project-owned native encoders, fail-closed target behavior, and an evidence vocabulary that continues to physical execution. Each ingredient has precedent; the engineering question is whether this exact chain can remain small, auditable, and reproducible.