← chronology · paper

Primary-source index

External sources used to locate the formal statements in the chronology. Dates locate these sources, not first discovery. The checked terms on the paper remain the authority for results proved there.

Older and physical identities

• Euclid, Elements VII, defs. 1–2. “Unit” and “number as a multitude composed of units.” Perseus text. Paper §6.1–6.3.
• Weber (1901), followed explicitly by Silberstein (1907). Complex electromagnetic field combining electric and magnetic fields. Silberstein: doi:10.1002/andp.19073270313. Paper §7.

1930s–1960s

• Gödel, K. (1931), “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I.” Arithmetization/Gödel numbering; paper §4.5–4.9.
• Curry, H. B. (1934), “Functionality in Combinatory Logic.” PNAS 20(11), 584–590. doi:10.1073/pnas.20.11.584. Early functionality/type–implication structure.
• Church, A. & Rosser, J. B. (1936), “Some Properties of Conversion.” Transactions AMS 39. Church–Rosser/confluence; paper §5.11 contrasts it with the stronger one-step diamond.
• Kleene, S. C. (1936), “General Recursive Functions of Natural Numbers.” Mathematische Annalen 112, 727–742. doi:10.1007/BF01565439. Recursive-function coding/equivalence context.
• Turing, A. M. (1936), “On Computable Numbers, with an Application to the Entscheidungsproblem.” Machine computation, universal execution, halting obstruction; paper §4.10.
• Newman, M. H. A. (1942). Original random-descent result: the quasi-diamond/WCR1 condition implies same normal form and same maximal reduction length when a normal form exists. Modern exposition: van Oostrom & Toyama, Normalisation by Random Descent, FSCD 2016, doi:10.4230/LIPIcs.FSCD.2016.32. Paper §5.11–5.13 proves the instance directly.
• Shannon, C. E. (1948), “A Mathematical Theory of Communication.” Quantitative information/entropy vocabulary; paper §3.
• Huffman, D. A. (1952), “A Method for the Construction of Minimum-Redundancy Codes.” Two-smallest weighted merge rule; paper §9.10.
• Kleene, S. C. (1952), Introduction to Metamathematics. Standard mature presentation of Gödel numbering, universal partial recursive functions, parameter/specialization machinery, and recursion theorems. Paper §4.12 reads Lawvere positively as recursion/self-reference.
• Bellman, R. (1957), Dynamic Programming. Princeton University Press. Principle of optimality / dynamic-programming recurrence; paper §5.15, §8.11, §9.13.
• Landauer, R. (1961), “Irreversibility and Heat Generation in the Computing Process.” IBM J. R&D 5, 183–191. Erasure bound; paper §5.9.
• Howard, W. A. (1969 notes; published 1980), “The Formulae-as-Types Notion of Construction.” Formulae-as-types/proofs-as-terms. Paper §5.1–5.3.
• Lawvere, F. W. (1969), “Diagonal Arguments and Cartesian Closed Categories.” Abstract fixed-point theorem. Paper §4.2–4.15.

Dependent equality, sharing, interaction

• Martin-Löf, P. (1970s onward), constructive/dependent type theory. Identity types, J, dependent substitution/transport. Paper §0.
• Lévy, J.-J. (1970s). Réductions sûres dans le lambda-calcul (1974); labelled lambda-calculus work; Réductions correctes et optimales dans le lambda-calcul (1978); “Le problème du partage dans l'évaluation des lambda-expressions” (1978). Residuals/families and optimal sharing; paper §5.24 lineage.
• Girard, J.-Y. (1987), “Linear Logic.” Explicit resource structure; proof nets/Geometry of Interaction supply neighboring graphical dynamics.
• Lamping, J. (1990), “An Algorithm for Optimal Lambda Calculus Reduction.” POPL '90. Local sharing-graph implementation of Lévy optimality.
• Lafont, Y. (1990), “Interaction Nets.” POPL '90, pp. 95–108. doi:10.1145/96709.96718. Principal ports/active pairs; direct geometry used at §5.11.
• Asperti, A.; Giovannetti, C.; Naletto, A. (1996), “The Bologna Optimal Higher-Order Machine.” JFP 6(6), 763–810. doi:10.1017/S0956796800001994.
• Lafont, Y. (1997), “Interaction Combinators.” Information and Computation 137, 69–101. doi:10.1006/inco.1997.2643. Three symbols/six rules universal distributed computation.
• Asperti, A. & Guerrini, S. (1998), The Optimal Implementation of Functional Programming Languages. Cambridge Tracts in Theoretical Computer Science 45. Comprehensive optimal-sharing synthesis.
• Hofmann, M. & Streicher, T. (1998), “The Groupoid Interpretation of Type Theory.” Nontrivial intensional identity structure.

Univalence and cubical computation

• Voevodsky / Univalent Foundations (2000s–2010s). Univalence: equivalence as identity of types.
• Bezem, M.; Coquand, T.; Huber, S. (2014), “A Model of Type Theory in Cubical Sets.” TYPES 2013 proceedings, LIPIcs 26, 107–128. doi:10.4230/LIPIcs.TYPES.2013.107. Constructive cubical model transforming equivalence into equality.
• Cohen, C.; Coquand, T.; Huber, S.; Mörtberg, A. (2016 preprint; 2018 proceedings), “Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom.” arXiv:1611.02108; LIPIcs TYPES 2015, doi:10.4230/LIPIcs.TYPES.2015.5. De Morgan interval, composition/filling, Glue, computational univalence; paper §§0–3.

Scope: this is the modern technical source index for the current chronology, not the deeper historical lineage. Older/parallel attestations should be added only at primary-source quality and without treating later notation as the standard by which earlier mathematics is judged.