@BOOK{plfa20.07,
    author = {Philip Wadler and Wen Kokke and Jeremy G. Siek},
    title  = {Programming Language Foundations in {A}gda},
    year   = {2020},
    month  = jul,
    url    = {https://plfa.inf.ed.ac.uk/20.07/},
}

@BOOK{plfa19.08,
    author = {Philip Wadler and Wen Kokke},
    title  = {Programming Language Foundations in {A}gda},
    year   = {2019},
    month  = aug,
    url    = {https://plfa.inf.ed.ac.uk/19.08/},
}

@article{Alessi:2006,
	author = {Alessi, Fabio and Barbanera, Franco and Dezani-Ciancaglini, Mariangiola},
	journal = {Theoretical Computer Science},
	number = {2},
	pages = {108--126},
	title = {Intersection Types and Lambda Models},
	volume = {355},
	year = 2006}

@article{Barendregt:1983,
	address = {Cambridge, UK},
	author = {Henk Barendregt and Mario Coppo and Mariangiola Dezani-Ciancaglini},
	day = {001},
	doi = {10.2307/2273659},
	journal = {Journal of Symbolic Logic},
	month = {12},
	number = {4},
	pages = {931-940},
	publisher = {Cambridge University Press},
	title = {A filter lambda model and the completeness of type assignment},
	volume = {48},
	year = {1983}}

@book{barendregt84:_lambda_calculus,
	author = {H.P. Barendregt},
	date-modified = {2007-05-18 13:42:22 -0600},
	publisher = {Elsevier},
	series = {Studies in Logic},
	title = {The Lambda Calculus},
	volume = {103},
	year = {1984}}

@book{Barendregt:2013,
	author = {Barendregt, Henk and Dekkers, Wil and Statman, Richard},
	collection = {Perspectives in Logic},
	place = {Cambridge},
	publisher = {Cambridge University Press},
	series = {Perspectives in Logic},
	title = {Lambda Calculus with Types},
	year = {2013}}

@inbook{Coppo:1979,
	address = {Berlin, Heidelberg},
	author = {Coppo, M. and Dezani-Ciancaglini, M. and Salle', P.},
	booktitle = {Automata, Languages and Programming: Sixth Colloquium},
	editor = {Maurer, Hermann A.},
	pages = {133--146},
	publisher = {Springer Berlin Heidelberg},
	title = {Functional characterization of some semantic equalities inside lambda-calculus},
	year = {1979}}

@article{Engeler:1981,
	author = {Engeler, Erwin},
	day = {01},
	journal = {Algebra Universalis},
	month = {Dec},
	number = {1},
	pages = {389--392},
	title = {Algebras and combinators},
	volume = {13},
	year = {1981}}

@article{Scott:1976,
	author = {Dana Scott},
	journal = {SIAM Journal on Computing},
	number = {3},
	pages = {522-587},
	publisher = {SIAM},
	title = {Data Types as Lattices},
	volume = {5},
	year = {1976}}

@techreport{Plotkin:1972,
	author = {Gordon D. Plotkin},
	institution = {University of Edinburgh},
	number = {MIP-R-95},
	title = {A Set-Theoretical Definition of Application},
	year = {1972}}

@article{Plotkin:1993,
	author = {Gordon D. Plotkin},
	journal = {Theoretical Computer Science},
	number = {1},
	pages = {351 - 409},
	title = {Set-theoretical and other elementary models of the λ-calculus},
	volume = {121},
	year = {1993}}

@book{Rocca:2004,
	author = {Simona {Ronchi Della Rocca} and Luca Paolini},
	publisher = {Springer},
	title = {The Parametric Lambda Calculus},
	year = {2004}}

@inproceedings{Schafer:2015,
  title={Autosubst: Reasoning with de Bruijn terms and parallel substitutions},
  author={Sch{\"a}fer, Steven and Tebbi, Tobias and Smolka, Gert},
  booktitle={Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings 6},
  pages={359--374},
  year={2015},
  organization={Springer}
}

@techreport{Pfenning:1992,
	author = {Pfenning, Frank},
	institution = {Carnegie Mellon University},
	number = {CMU-CS-92-186},
	publisher = {Carnegie Mellon University},
	title = {A Proof of the Church-Rosser Theorem and Its Representation in a Logical Framework},
	year = {1992}}

@article{Takahashi:1995,
title = {Parallel Reductions in λ-Calculus},
journal = {Information and Computation},
volume = {118},
number = {1},
pages = {120-127},
year = {1995},
doi = {https://doi.org/10.1006/inco.1995.1057},
author = {M. Takahashi}}

@inproceedings{Nipkow:1996,
    author = {Nipkow, Tobias},
    title = {More Church-Rosser Proofs (in Isabelle/HOL)},
    year = {1996},
    publisher = {Springer-Verlag},
    address = {Berlin, Heidelberg},
    booktitle = {Proceedings of the 13th International Conference on Automated Deduction: Automated Deduction},
    pages = {733–747},
    numpages = {15},
    series = {CADE-13}
    }