@Book{awodey2010category,
	keywords = {category theory},
	title = {Category theory},
	author = {Awodey, Steve},
	year = {2010},
	publisher = {Oxford University Press}
}

@Book{barras1997coq,
	title = {The Coq proof assistant reference manual: Version 6.1},
	author = {Barras, Bruno and Boutin, Samuel and Cornes, Cristina and Courant, Judicaël and Filliatre, Jean-Christophe and Gimenez, Eduardo and Herbelin, Hugo and Huet, Gérard and Munoz, Cesar and Murthy, Chetan},
	year = {1997},
	publisher = {Inria}
}

@Article{church1932set,
	pages = {346--366},
	number = {2},
	volume = {33},
	year = {1932},
	journaltitle = {Annals of Mathematics},
	title = {A set of postulates for the foundation of logic},
	author = {Church, Alonzo}
}

@Article{church1940formulation,
	journaltitle = {The journal of symbolic logic},
	title = {A formulation of the simple theory of types},
	author = {Church, Alonzo},
	volume = {5},
	number = {2},
	pages = {56--68},
	year = {1940}
}

@Misc{coq2019,
	doi = {10.5281/zenodo.2554024},
	url = {https://doi.org/10.5281/zenodo.2554024},
	year = {2019},
	title = {The Coq Proof Assistant, version 8.9.0},
	author = {{The Coq Development Team}}
}

@Article{coquand1988calculus,
	journaltitle = {Information and Computation},
	title = {The calculus of constructions},
	volume = {76},
	number = {2},
	pages = {95--120},
	year = {1988},
	issn = {0890-5401},
	doi = {10.1016/0890-5401(88)90005-3},
	author = {Coquand, Thierry and Huet, Gérard}
}

@InProceedings{coquand1990inductively,
	doi = {10.1007/3-540-52335-9_47},
	pages = {50--66},
	publisher = {Springer, Berlin, Heidelberg},
	volume = {417},
	series = {Lecture Notes in Computer Science},
	editor = {{Martin-Löf}, Per and Mints, Grigori},
	booktitle = {Proceedings of Colog-88},
	year = {1990},
	title = {Inductively defined types},
	author = {Coquand, Thierry and {Paulin-Mohring}, Christine}
}

@Article{curry1948simplification,
	journaltitle = {Synthese},
	file = {Documents/reading/math/curry1948simplification.pdf},
	number = {6-A},
	volume = {7},
	title = {A simplification of the theory of combinators},
	author = {Curry, Haskell B},
	pages = {391--399},
	year = {1948}
}

@InBook{curry1961some,
	file = {Documents/reading/math/haskell_curry.pdf; Documents/reading/math/haskell_curry_cropped.pdf},
	pages = {56--68},
	publisher = {American Mathematical Society},
	volume = {12},
	booktitle = {Structure of language and its mathematical aspects},
	author = {Curry, Haskell B},
	year = {1961},
	title = {Some logical aspects of grammatical structure}
}

@InProceedings{de2015lean,
	title = {The Lean theorem prover (system description)},
	author = {{de Moura}, Leonardo and Kong, Soonho and Avigad, Jeremy and {van Doorn}, Floris and {von Raumer}, Jakob},
	booktitle = {25th International Conference on Automated Deduction (CADE-25)},
	pages = {378--388},
	year = {2015}
}

@InProceedings{egri2004algebraic,
	pages = {315--316},
	series = {International Conference on Implementation and Application of Automata (CIAA)},
	publisher = {Springer-Verlang},
	location = {Kingson, Canada},
	year = {2005},
	booktitle = {Proceedings of the 9th international conference on Implementation and Application of Automata (CIAA '04)},
	title = {Algebraic hierarchical decomposition of finite state automata: comparison of implementations for krohn-rhodes theory},
	author = {Egri-Nagy, Attila and Nehaniv, Chystopher L.}
}

@Book{fong2018seven,
	file = {Documents/reading/math/fong2018seven.pdf},
	keywords = {category theory},
	year = {2018},
	title = {Seven Sketches in Compositionality: An Invitation to Applied Category Theory},
	author = {Fong, Brendan and Spivak, David I.}
}

@Article{girard1987linear,
	pages = {1--101},
	number = {1},
	volume = {50},
	year = {1987},
	journaltitle = {Theoretical computer science},
	title = {Linear logic},
	author = {Girard, Jean-Yves}
}

@Article{henkin1950completeness,
	journaltitle = {The Journal of Symbolic Logic},
	title = {Completeness in the theory of types},
	author = {Henkin, Leon},
	volume = {15},
	number = {2},
	pages = {81--91},
	year = {1950}
}

@Book{leinster2016basic,
	file = {Documents/reading/math/leinster2016basic.pdf},
	keywords = {category theory},
	year = {2016},
	title = {Basic Category Theory},
	author = {Leinster, Tom}
}

@InProceedings{lin2009hierarchical,
	file = {Documents/reading/math/lin2009hierarchical.pdf},
	keywords = {finite automata},
	organization = {ACM},
	year = {2009},
	booktitle = {Proceedings of the 19th ACM Great Lakes symposium on VLSI},
	title = {Hierarchical state machine architecture for regular expression pattern matching},
	author = {Lin, Cheng-Hung and Hsiao, Hsien-Sheng}
}

@Thesis{luo1990extended,
	file = {Documents/reading/math/luo1990extended.pdf},
	year = {1990},
	institution = {University of Edinburgh},
	type = {PhD},
	title = {An Extended Calculus of Constructions},
	author = {Luo, Zhaohui}
}

@InBook{luo1992unifying,
	pages = {293--304},
	editor = {Nerode, Anil and Taitslin, Mikhail},
	booktitle = {Logical Foundations of Computer Science -- Tver '92},
	author = {Luo, Zhaohui},
	year = {1992},
	subtitle = {The schematic approach},
	title = {A unifying theory of dependent types}
}

@Unpublished{luo2012notes,
	title = {Notes on universes in type theory},
	author = {Luo, Zhaohui},
	note = {Lecture notes for a talk at Institute for Advanced Study, Princeton},
	url = {http://www.cs.rhul.ac.uk/home/zhaohui/universes.pdf},
	year = {2012}
}

@Article{luo2013coercive,
	pages = {18--42},
	volume = {233},
	year = {2013},
	journaltitle = {Information and Computation},
	subtitle = {Theory and implementation},
	title = {Coercive subtyping},
	author = {Luo, Zhaohui and Soloviev, Sergei and Xue, Tao}
}

@Book{martinlof1984intuitionistic,
	title = {Intuitionistic type theory},
	author = {Martin-Löf, Per},
	publisher = {Naples: Bibliopolis},
	year = {1984}
}

@InBook{mazur2008when,
	file = {Documents/reading/math/mazur2008when.pdf},
	pages = {221--241},
	volume = {59},
	booksubtitle = {Mathematics and Philosophy},
	booktitle = {Proof and Other Dilemmas},
	author = {Mazur, Barry},
	year = {2008},
	title = {When is one thing equal to some other thing?}
}

@Article{mohri1997finite,
	journaltitle = {Computational Linguistics},
	file = {Documents/reading/math/mohri1997finite.pdf},
	keywords = {finite automata},
	pages = {269--311},
	number = {2},
	volume = {23},
	year = {1997},
	title = {Finite-state transducers in language and speech processing},
	author = {Mohri, Mehryar}
}

@InProceedings{niemi2007representing,
	keywords = {finite automata},
	pages = {355--362},
	series = {Nordic Conference on Computational Linguistics (NoDaLiDa)},
	editor = {Nivre, Joakim and Kaalep, Heiki-Jann and Muischnek, Kadri and Koit, Mare},
	year = {2007},
	booktitle = {Nordic Conference on Computational Linguistics (NoDaLiDa) 2007 Conference Proceedings},
	title = {Representing Calendar Expressions with Finite-State Transducers that Bracket Periods of Time on a Hierarchical Timeline},
	author = {Niemi, Jyrki and Koskenniemi, Kimmo}
}

@InProceedings{reghizzi2011from,
	file = {Documents/reading/math/reghizzi2011from.pdf},
	keywords = {finite automata},
	doi = {10.4204/EPTCS.63.14},
	pages = {103--111},
	organization = {WORDS},
	number = {63},
	series = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},
	editor = {Ambrož, Petr, Holub, Štěpán and Masáková, Zuzana},
	booktitle = {8th International Conference of WORDS},
	year = {2011},
	title = {From regular to strictly local testable languages},
	author = {Reghizzi, Stefano Crespi and {San Pietro}, Pierluigi}
}

@Book{riehl2014category,
	file = {Documents/reading/math/riehl2014category.pdf},
	keywords = {category theory},
	year = {2014},
	title = {Category Theory in Context},
	author = {Riehl, Emily}
}

@InBook{troelstra2011history,
	pages = {150--179},
	booktitle = {Set Theory, Arithmetic, and Foundations of Mathematics},
	year = {2011},
	title = {History of constructivism in the 20th century},
	author = {Troelstra, Anne Sjerp}
}

@Book{vanheijenoort1967frege,
	publisher = {Harvard University Press},
	volume = {9},
	year = {1967},
	subtitle = {a source book in mathematical logic, 1879--1931},
	title = {From Frege to Gödel},
	author = {Van Heijenoort, Jean}
}

@Article{wadler1991linear,
	pages = {255--273},
	number = {9},
	volume = {26},
	year = {1991},
	journaltitle = {ACM SIGPLAN Notices},
	title = {Is there a use for linear logic?},
	author = {Wadler, Philip}
}

@Comment{
Local Variables:
bibtex-dialect: biblatex
End:
}