291 lines
8.3 KiB
BibTeX
291 lines
8.3 KiB
BibTeX
|
|
@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:
|
|
}
|
|
|