biblio.bib

@article{Bohm85,
	added-at = {2018-11-02T00:00:00.000+0100},
	author = {B{\"o}hm, Corrado and Berarducci, Alessandro},
	biburl = {https://www.bibsonomy.org/bibtex/2f7db5b2f43516ff90ede9e64f9c944f0/dblp},
	ee = {https://doi.org/10.1016/0304-3975(85)90135-5},
	interhash = {1a09f13edf5f7c2fe5670fc5acebc0c6},
	intrahash = {f7db5b2f43516ff90ede9e64f9c944f0},
	journal = {Theor. Comput. Sci.},
	pages = {135--154},
	timestamp = {2018-11-03T12:34:37.000+0100},
	title = {Automatic Synthesis of Typed Lambda-Programs on Term Algebras.},
	url = {http://dblp.uni-trier.de/db/journals/tcs/tcs39.html#BohmB85},
	volume = 39,
	x-fetchedfrom = {Bibsonomy},
	year = 1985
}

@book{TTFPLambdaC,
	abstract = {{"Type theory is a fast-evolving field at the crossroads of logic, computer science and mathematics. This gentle step-by-step introduction is ideal for graduate students and researchers who need to understand the ins and outs of the mathematical machinery, the role of logical rules therein, the essential contribution of definitions and the decisive nature of well-structured proofs. The authors begin with untyped lambda calculus and proceed to several fundamental type systems culminating in the well-known and powerful Calculus of Constructions. The book also covers the essence of proof checking and proof development, and the use of dependent type theory to formalize mathematics. The only prerequisites are a good knowledge of undergraduate algebra and analysis. Carefully chosen examples illustrate the theory throughout. Each chapter ends with a summary of the content, some historical context, suggestions for further reading and a selection of exercises to help readers familiarize themselves with the material"--}},
	added-at = {2017-06-29T07:13:07.000+0200},
	author = {Nederpelt, R. P. and Geuvers, Herman},
	biburl = {https://www.bibsonomy.org/bibtex/243fa82ff81d6d1bcfeee62d74bb3ae51/gdmcbain},
	citeulike-article-id = {14255143},
	citeulike-linkout-0 = {http://www.worldcat.org/isbn/9781107036505},
	citeulike-linkout-1 = {http://books.google.com/books?vid=ISBN9781107036505},
	citeulike-linkout-2 = {http://www.amazon.com/gp/search?keywords=9781107036505\&index=books\&linkCode=qs},
	citeulike-linkout-3 = {http://www.librarything.com/isbn/9781107036505},
	citeulike-linkout-4 = {http://www.worldcat.org/oclc/874733138},
	interhash = {b72fb675034890047980f2ea5b536513},
	intrahash = {43fa82ff81d6d1bcfeee62d74bb3ae51},
	isbn = {9781107036505},
	keywords = {03b15-higher-order-logic-type-theory},
	pages = {127},
	posted-at = {2017-01-15 01:52:06},
	priority = {2},
	timestamp = {2017-06-29T07:13:07.000+0200},
	title = {Type theory and formal proof : an introduction},
	url = {http://www.worldcat.org/isbn/9781107036505},
	x-fetchedfrom = {Bibsonomy},
	year = 2014
}

@book{TAPLVariants,
	abstract = {{A type system is a syntactic method for automatically checking the absence of certain erroneous behaviors by classifying program phrases according to the kinds of values they compute. The study of type systems--and of programming languages from a type-theoretic perspective -- -has important applications in software engineering, language design, high-performance compilers, and security. This text provides a comprehensive introduction both to type systems in computer science and to the basic theory of programming languages. The approach is pragmatic and operational; each new concept is motivated by programming examples and the more theoretical sections are driven by the needs of implementations. Each chapter is accompanied by numerous exercises and solutions, as well as a running implementation, available via the Web. Dependencies between chapters are explicitly identified, allowing readers to choose a variety of paths through the material. The core topics include the untyped lambda-calculus, simple type systems, type reconstruction, universal and existential polymorphism, subtyping, bounded quantification, recursive types, kinds, and type operators. Extended case studies develop a variety of approaches to modeling the features of object-oriented languages.}},
	added-at = {2017-06-29T07:13:07.000+0200},
	author = {Pierce, Benjamin C.},
	biburl = {https://www.bibsonomy.org/bibtex/2078fb5cb1e3638d53ec8aa21e241c306/gdmcbain},
	citeulike-article-id = {105547},
	citeulike-attachment-1 = {pierce\_02\_types\_1110544.pdf; /pdf/user/gdmcbain/article/105547/1110544/pierce\_02\_types\_1110544.pdf; 22f1c7b32c71606a20ff1a75bd784ae57685f7d2},
	citeulike-linkout-0 = {http://ropas.snu.ac.kr/\~{}kwang/520/pierce\_book.pdf},
	citeulike-linkout-1 = {http://www.amazon.ca/exec/obidos/redirect?tag=citeulike09-20\&path=ASIN/0262162091},
	citeulike-linkout-10 = {http://www.librarything.com/isbn/0262162091},
	citeulike-linkout-11 = {http://www.worldcat.org/oclc/51958338},
	citeulike-linkout-2 = {http://www.amazon.de/exec/obidos/redirect?tag=citeulike01-21\&path=ASIN/0262162091},
	citeulike-linkout-3 = {http://www.amazon.fr/exec/obidos/redirect?tag=citeulike06-21\&path=ASIN/0262162091},
	citeulike-linkout-4 = {http://www.amazon.jp/exec/obidos/ASIN/0262162091},
	citeulike-linkout-5 = {http://www.amazon.co.uk/exec/obidos/ASIN/0262162091/citeulike00-21},
	citeulike-linkout-6 = {http://www.amazon.com/exec/obidos/redirect?tag=citeulike07-20\&path=ASIN/0262162091},
	citeulike-linkout-7 = {http://www.worldcat.org/isbn/0262162091},
	citeulike-linkout-8 = {http://books.google.com/books?vid=ISBN0262162091},
	citeulike-linkout-9 = {http://www.amazon.com/gp/search?keywords=0262162091\&index=books\&linkCode=qs},
	comment = {recommended by Tony Morris, NICTA, 2015-09-16 ---=note-separator=--- Recommended as second text by 'type-theory/learn-tt':https://github.com/type-theory/learn-tt},
	day = 01,
	edition = 1,
	file = {pierce_02_types_1110544.pdf},
	howpublished = {Hardcover},
	interhash = {4d6e4bcf471203882efcef73f6463035},
	intrahash = {078fb5cb1e3638d53ec8aa21e241c306},
	isbn = {0262162091},
	keywords = {03b15-higher-order-logic-type-theory},
	month = feb,
	pages = {136--142},
	posted-at = {2015-09-16 07:18:50},
	priority = {5},
	privnote = {recommended by Tony Morris, NICTA, 2015-09-16 ---=note-separator=--- Recommended as second text by 'type-theory/learn-tt':https://github.com/type-theory/learn-tt},
	publisher = {MIT Press},
	timestamp = {2017-06-29T07:13:07.000+0200},
	title = {Types and Programming Languages},
	url = {http://ropas.snu.ac.kr/\~{}kwang/520/pierce\_book.pdf},
	x-fetchedfrom = {Bibsonomy},
	year = 2002
}

@article{Eisenberg16,
	added-at = {2018-08-13T00:00:00.000+0200},
	author = {Eisenberg, Richard A.},
	biburl = {https://www.bibsonomy.org/bibtex/26f4bb63eb8b3285d86a3ea8bc2552075/dblp},
	ee = {http://arxiv.org/abs/1610.07978},
	interhash = {24197fb6def2d6582c0b5411a5016ed2},
	intrahash = {6f4bb63eb8b3285d86a3ea8bc2552075},
	journal = {CoRR},
	timestamp = {2018-08-14T14:43:37.000+0200},
	title = {Dependent Types in Haskell: Theory and Practice.},
	url = {http://dblp.uni-trier.de/db/journals/corr/corr1610.html#Eisenberg16},
	volume = {abs/1610.07978},
	x-fetchedfrom = {Bibsonomy},
	year = 2016
}

@article{Idris13,
	author = {BRADY, EDWIN},
	doi = {10.1017/S095679681300018X},
	issn = {1469-7653},
	issue = {05},
	journal = {Journal of Functional Programming},
	month = {9},
	numpages = {42},
	pages = {552--593},
	title = {Idris, a general-purpose dependently typed programming language: Design and implementation},
	url = {https://journals.cambridge.org/article_S095679681300018X},
	volume = {23},
	year = {2013}
}

@inproceedings{LiquidTypes08,
	added-at = {2018-11-06T00:00:00.000+0100},
	author = {Rondon, Patrick Maxim and Kawaguchi, Ming and Jhala, Ranjit},
	biburl = {https://www.bibsonomy.org/bibtex/2fb6ff40842e39a3be310611d63b1afaa/dblp},
	booktitle = {PLDI},
	editor = {Gupta, Rajiv and Amarasinghe, Saman P.},
	ee = {https://doi.org/10.1145/1375581.1375602},
	interhash = {90a6a09a83611cfe6156a7b3c7fed781},
	intrahash = {fb6ff40842e39a3be310611d63b1afaa},
	isbn = {978-1-59593-860-2},
	pages = {159--169},
	publisher = {ACM},
	timestamp = {2018-11-07T13:54:15.000+0100},
	title = {Liquid types.},
	url = {http://dblp.uni-trier.de/db/conf/pldi/pldi2008.html#RondonKJ08},
	x-fetchedfrom = {Bibsonomy},
	year = 2008
}

@article{Reflection18,
	added-at = {2020-09-05T00:00:00.000+0200},
	author = {Vazou, Niki and Tondwalkar, Anish and Choudhury, Vikraman and Scott, Ryan G. and Newton, Ryan R. and Wadler, Philip and Jhala, Ranjit},
	biburl = {https://www.bibsonomy.org/bibtex/223a4d586cb4125da2fa6d92702c40a27/dblp},
	ee = {https://doi.org/10.1145/3158141},
	interhash = {b281903a0fb1e3ccba200dbb834fd349},
	intrahash = {23a4d586cb4125da2fa6d92702c40a27},
	journal = {Proc. ACM Program. Lang.},
	number = {POPL},
	pages = {53:1--53:31},
	timestamp = {2020-09-09T11:42:27.000+0200},
	title = {Refinement reflection: complete verification with SMT.},
	url = {http://dblp.uni-trier.de/db/journals/pacmpl/pacmpl2.html#VazouTCSNWJ18},
	volume = 2,
	x-fetchedfrom = {Bibsonomy},
	year = 2018
}

@book{Schmidt1994,
	added-at = {2006-03-09T08:15:35.000+0100},
	address = {Cambridge, Mass.},
	annote = {Hundreds of references.},
	author = {Schmidt, David A.},
	biburl = {https://www.bibsonomy.org/bibtex/26bc58f88b3239fbcc740426bb4b163d0/snowball},
	interhash = {8c15936924c3e7a8e297c2417ba2df25},
	intrahash = {6bc58f88b3239fbcc740426bb4b163d0},
	key = {Schmidt},
	keywords = {imported},
	publisher = {MIT Press},
	series = {Foundations of Computing Series},
	timestamp = {2006-03-09T08:15:35.000+0100},
	title = {The Structure of Typed Programming Languages},
	x-fetchedfrom = {Bibsonomy},
	year = 1994
}

@article{Barendregt92,
	abstract = {-},
	added-at = {2014-11-23T03:26:08.000+0100},
	author = {Barendregt, Henk and Abramsky, S. and Gabbay, D. M. and Maibaum, T. S. E. and Barendregt, H. P.},
	biburl = {https://www.bibsonomy.org/bibtex/225d5f957941866685798b48257bce93e/t.uemura},
	booktitle = {Handbook of Logic in Computer Science},
	description = {Lambda Calculi with Types},
	interhash = {9d58a7843aa38dcede40ca0baaafde98},
	intrahash = {25d5f957941866685798b48257bce93e},
	keywords = {lambda calculus},
	pages = {117--309},
	publisher = {Oxford University Press},
	timestamp = {2014-11-23T03:26:08.000+0100},
	title = {Lambda Calculi with Types},
	url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.4391},
	x-fetchedfrom = {Bibsonomy},
	year = 1992
}

@inproceedings{Constable87,
	added-at = {2017-12-29T00:00:00.000+0100},
	author = {Constable, Robert L. and Smith, Scott F.},
	biburl = {https://www.bibsonomy.org/bibtex/25a90fa99f18dafd4e77717448e4940ef/dblp},
	booktitle = {LICS},
	interhash = {4a3e2d02ecfd46d9bba9c1c15f72cacb},
	intrahash = {5a90fa99f18dafd4e77717448e4940ef},
	pages = {183--193},
	publisher = {IEEE Computer Society},
	timestamp = {2017-12-30T11:37:12.000+0100},
	title = {Partial Objects In Constructive Type Theory},
	url = {http://dblp.uni-trier.de/db/conf/lics/lics87.html#ConstableS87},
	x-fetchedfrom = {Bibsonomy},
	year = 1987
}

@article{Rushby98,
	added-at = {2015-12-10T00:00:00.000+0100},
	author = {Rushby, John M. and Owre, Sam and Shankar, Natarajan},
	biburl = {https://www.bibsonomy.org/bibtex/2059b66574a76d7af32c4d4c77691482e/dblp},
	ee = {http://doi.ieeecomputersociety.org/10.1109/32.713327},
	interhash = {780cfb18245aa9ae3169e8bc7af69780},
	intrahash = {059b66574a76d7af32c4d4c77691482e},
	journal = {IEEE Trans. Software Eng.},
	number = 9,
	pages = {709--720},
	timestamp = {2015-12-12T11:51:30.000+0100},
	title = {Subtypes for Specifications: Predicate Subtyping in PVS.},
	url = {http://dblp.uni-trier.de/db/journals/tse/tse24.html#RushbyOS98},
	volume = 24,
	x-fetchedfrom = {Bibsonomy},
	year = 1998
}

@article{abel1998foetus,
	author = {Abel, Andreas},
	journal = {Programming Lab Report},
	publisher = {Citeseer},
	title = {foetus--termination checker for simple functional programs},
	volume = {474},
	year = {1998}
}

@phdthesis{Vazou16,
	added-at = {2017-05-16T00:00:00.000+0200},
	author = {Vazou, Niki},
	biburl = {https://www.bibsonomy.org/bibtex/25de5e29474f465ce61a46599b28653e5/dblp},
	ee = {https://www.base-search.net/Record/581e03c8b1659d297c15667c22401cf92ca39037ef773937be1aa5536823102e},
	interhash = {6d7110d979cdc95cfeeffeb49bf66581},
	intrahash = {5de5e29474f465ce61a46599b28653e5},
	note = {base-search.net (ftcdlib:qt8dm057ws)},
	school = {University of California, San Diego, USA},
	timestamp = {2017-05-18T19:35:40.000+0200},
	title = {Liquid Haskell: Haskell as a Theorem Prover.},
	x-fetchedfrom = {Bibsonomy},
	year = 2016
}

@misc{MetaFStar,
	abstract = {  We introduce Meta-F*, a tactics and metaprogramming framework for the F*
program verifier. The main novelty of Meta-F* is allowing the use of tactics
and metaprogramming to discharge assertions not solvable by SMT, or to just
simplify them into well-behaved SMT fragments. Plus, Meta-F* can be used to
generate verified code automatically.
  Meta-F* is implemented as an F* effect, which, given the powerful effect
system of F*, heavily increases code reuse and even enables the lightweight
verification of metaprograms. Metaprograms can be either interpreted, or
compiled to efficient native code that can be dynamically loaded into the F*
type-checker and can interoperate with interpreted code. Evaluation on
realistic case studies shows that Meta-F* provides substantial gains in proof
development, efficiency, and robustness.
},
	archiveprefix = {arXiv},
	author = {Mart{\'\i}nez, Guido and Ahman, Danel and Dumitrescu, Victor and Giannarakis, Nick and Hawblitzel, Chris and Hritcu, Catalin and Narasimhamurthy, Monal and Paraskevopoulou, Zoe and Pit-Claudel, Cl{\'e}ment and Protzenko, Jonathan and Ramananandro, Tahina and Rastogi, Aseem and Swamy, Nikhil},
	comment = {published = 2018-03-17T18:08:13Z, updated = 2019-03-07T13:25:38Z, Full version of ESOP'19 paper},
	eprint = {1803.06547v4},
	month = mar,
	primaryclass = {cs.PL},
	title = {Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms},
	url = {http://arxiv.org/abs/1803.06547v4; http://arxiv.org/pdf/1803.06547v4},
	x-fetchedfrom = {arXiv.org},
	year = {2019}
}

@article{CoqHammer,
	added-at = {2020-09-02T00:00:00.000+0200},
	author = {Czajka, Lukasz and Kaliszyk, Cezary},
	biburl = {https://www.bibsonomy.org/bibtex/25643c3bf3a38a883d2590c1f8038bdb8/dblp},
	ee = {https://www.wikidata.org/entity/Q90699792},
	interhash = {afcd59e05b935c6bf2a513955f4b8d54},
	intrahash = {5643c3bf3a38a883d2590c1f8038bdb8},
	journal = {J. Autom. Reason.},
	number = {1-4},
	pages = {423--453},
	timestamp = {2020-09-09T13:35:05.000+0200},
	title = {Hammer for Coq: Automation for Dependent Type Theory.},
	url = {http://dblp.uni-trier.de/db/journals/jar/jar61.html#CzajkaK18},
	volume = 61,
	x-fetchedfrom = {Bibsonomy},
	year = 2018
}

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

@inproceedings{SystemFAgda,
	added-at = {2020-04-18T00:00:00.000+0200},
	author = {Chapman, James and Kireev, Roman and Nester, Chad and Wadler, Philip},
	biburl = {https://www.bibsonomy.org/bibtex/27a3bbdfd0b2211254dae33486e007825/dblp},
	booktitle = {MPC},
	editor = {Hutton, Graham},
	ee = {https://doi.org/10.1007/978-3-030-33636-3_10},
	interhash = {0c7c5d0e19449166df546a710ba06a70},
	intrahash = {7a3bbdfd0b2211254dae33486e007825},
	isbn = {978-3-030-33636-3},
	pages = {255--297},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	timestamp = {2020-04-21T11:42:56.000+0200},
	title = {System F in Agda, for Fun and Profit.},
	url = {http://dblp.uni-trier.de/db/conf/mpc/mpc2019.html#ChapmanKNW19},
	volume = 11825,
	x-fetchedfrom = {Bibsonomy},
	year = 2019
}

@article{LocallyNameless,
	added-at = {2020-09-02T00:00:00.000+0200},
	author = {Chargu{\'e}raud, Arthur},
	biburl = {https://www.bibsonomy.org/bibtex/2b9f06e1959349846c89d4c5b7bbbe868/dblp},
	ee = {https://doi.org/10.1007/s10817-011-9225-2},
	interhash = {09db8ab20f8e9c3bb099b08457fa8654},
	intrahash = {b9f06e1959349846c89d4c5b7bbbe868},
	journal = {J. Autom. Reason.},
	number = 3,
	pages = {363--408},
	timestamp = {2020-09-09T13:34:35.000+0200},
	title = {The Locally Nameless Representation.},
	url = {http://dblp.uni-trier.de/db/journals/jar/jar49.html#Chargueraud12},
	volume = 49,
	x-fetchedfrom = {Bibsonomy},
	year = 2012
}

@misc{CoqBinNums,
	author = {{The Coq development team}},
	howpublished = {\url{https://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html}},
	note = {[Online; accessed 03-April-2021]},
	title = {The Coq proof assistant reference manual: Binary Numerical Datatypes},
	year = {2021}
}

@article{LeibnizEq,
	added-at = {2020-09-05T00:00:00.000+0200},
	author = {Abel, Andreas and Cockx, Jesper and Devriese, Dominique and Timany, Amin and Wadler, Philip},
	biburl = {https://www.bibsonomy.org/bibtex/27f5f4d61d6ebc899ea28dd72bbab1a67/dblp},
	ee = {https://doi.org/10.1017/S0956796820000155},
	interhash = {de77c75a02799a137ebeb15d4639fb36},
	intrahash = {7f5f4d61d6ebc899ea28dd72bbab1a67},
	journal = {J. Funct. Program.},
	timestamp = {2020-09-09T13:38:56.000+0200},
	title = {Leibniz equality is isomorphic to Martin-L{\"o}f identity, parametrically.},
	url = {http://dblp.uni-trier.de/db/journals/jfp/jfp30.html#AbelCDTW20},
	volume = 30,
	x-fetchedfrom = {Bibsonomy},
	year = 2020
}