@article{Category3-AFP,
  author  = {Eugene W. Stark},
  title   = {Category Theory with Adjunctions and Limits},
  journal = {Archive of Formal Proofs},
  month   = jun,
  year    = 2016,
  note    = {\url{http://isa-afp.org/entries/Category3.shtml}, Formal proof development},
  ISSN    = {2150-914x},
}
@article{cts,
	author = "E. W. Stark",
	title = "Concurrent Transition Systems",
	journal = "Theoretical Computer Science",
	volume = 64,
	month = JUL,
	pages = "221--269",
	year = 1989
}
@article{huet-residual-theory,
	author = "G. Huet",
	title = "Residual theory in \lambda-calculus: A formal development",
	journal = "Journal of Functional Programming",
	volume = 4,
	number = 3,
  pages = "371--394",
	year = 1994
}
@book{barendregt,
	author = "H. Barendregt",
	title = "The Lambda-calculus: Its Syntax and Semantics",
	year = 1984,
	publisher = "North-Holland"
}
@phdthesis{levy,
  author = "J.-J. Lévy",
	title = "Réductions correctes et optimales dans le \lambda-calcul",
  school = "U. Paris VII",
	year = 1978,
  note = "Th\`ese d'Etat"
}
@phdthesis{schroer,
  author = "D. E. Schroer",
  title = "The Church-Rosser Theorem",
  school = "Cornell University",
  year = 1965
}
@article{deBruijn,
	author = "N. G. {de Bruijn}",
  title = "Lambda-Calculus notation with nameless dummies, a tool for automatic
           formula manipulation, with application to the Church-Rosser theorem",
	journal = {Indagationes Mathematicae (Proceedings)},
	volume = 34,
	number = 5,
  pages = "381--392",
	year = 1972
}
@article{deVrijer,
	author = "R. {de Vrijer}",
	title = "A Direct Proof of the Finite Developments Theorem",
	volume = "50",
	number = "2",
	month = JUN,
	year = 1985,
	pages = "339--343",
	journal = "The Journal of Symbolic Logic"
}
@article{hindley,
	author = "R. Hindley",
  title = "Reductions of Residuals are Finite",
	volume = 240,
	year = 1978,
	month = JUN,
	pages = "345--361",
	journal = "Transactions of the American Mathematical Society"
}
@book{curry-and-feys,
	author = "H. B. Curry and R. Feys",
	title = "Combinatory Logic",
  volume = 1,
	year = 1958,
	publisher = "North-Holland"
}
@mastersthesis{copes,
  author = "M. Copes",
  title = "A machine-checked proof of the Standardization Theorem in Lambda Calculus
           using multiple substitution",
  school = "Universidad ORT Uruguay",
  year = 2018,
  note = {\url{https://dspace.ort.edu.uy/bitstream/handle/20.500.11968/3725/Material%20completo.pdf}},
}

