references.bib 46.6 KB
Newer Older
Nicola Botta's avatar
Nicola Botta committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
@misc{idristutorial,
  author =	 {{The Idris Community}},
  title =	 {The {Idris} tutorial},
  howpublished = {\url{http://docs.idris-lang.org/en/latest/tutorial/index.html}},
  url =		 {http://docs.idris-lang.org/en/latest/tutorial/index.html},
  year =	 2020
}

@misc{idrisreference,
  author =	 {{The Idris Community}},
  title =	 {Language {Reference}},
  howpublished = {\url{http://docs.idris-lang.org/en/latest/reference/index.html}},
  url =		 {http://docs.idris-lang.org/en/latest/reference/index.html},
  year =	 2020
}

@misc{idrisguides,
  author =	 {{The Idris Community}},
  title =	 {Tutorials on the {Idris} {Language}},
  howpublished = {\url{http://docs.idris-lang.org/en/latest/guides/index.html}},
  url =		 {http://docs.idris-lang.org/en/latest/guides/index.html},
  year =	 2020
}

25
26
27
28
29
30
31
32
33
@misc{idrisdocs,
  author =	 {{The Idris Community}},
  title =	 {{D}ocumentation for the {I}dris {L}anguage},
  howpublished = {\url{http://docs.idris-lang.org/en/latest/}},
  url =		 {http://docs.idris-lang.org/en/latest/},
  year =	 2020
}


Nicola Botta's avatar
Nicola Botta committed
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
@book{idrisbook,
  author =	 {Edwin Brady},
  publisher =	 {Manning Publications Co.},
  title =	 {Type-{D}riven {D}evelopment in {I}dris},
  year =	 2017
}

@article{schoenfinkel1924,
  author =	 {M. Sch{\"o}nfinkel},
  journal =	 {Mathematische Annalen},
  pages =	 {305--316},
  title =	 {{\"U}ber die {B}austeine der mathematischen {L}ogik},
  year =	 1924
}

@misc{botta20162018,
  author =	 {Nicola Botta},
  howpublished = {\url{https://gitlab.pik-potsdam.de/botta/IdrisLibs}},
  title =	 {{I}dris{L}ibs},
Nicola Botta's avatar
Final.    
Nicola Botta committed
53
  year =	 {2016--2021}
Nicola Botta's avatar
Nicola Botta committed
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
}

@inproceedings{ionescujansson:LIPIcs:2013:3899,
  address =	 {Dagstuhl, Germany},
  annote =	 {Keywords: dependently-typed programming,
                  domain-specific languages, climate impact research,
                  formalization},
  author =	 {Cezar Ionescu and Patrik Jansson},
  booktitle =	 {Proc. {TYPES} 2011},
  commenteditor ={Nils Anders Danielsson and Bengt Nordstr{\"o}m},
  commentisbn =	 {978-3-939897-49-1},
  commentissn =	 {1868-8969},
  commenturl =	 {http://drops.dagstuhl.de/opus/volltexte/2013/3899},
  doi =		 {10.4230/LIPIcs.TYPES.2011.41},
  longbooktitle ={18th International Workshop on Types for Proofs and
                  Programs (TYPES 2011)},
  pages =	 {41--54},
Nicola Botta's avatar
Final.    
Nicola Botta committed
71
  publisher =	 {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
Nicola Botta's avatar
Nicola Botta committed
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
  series =	 {Leibniz International Proceedings in Informatics
                  (LIPIcs)},
  title =	 {Testing versus proving in climate impact research},
  volume =	 19,
  year =	 2013
}

@book{bellman1957,
  author =	 {Richard Bellman},
  publisher =	 {Princeton University Press},
  title =	 {Dynamic Programming},
  year =	 1957
}

@article{2017_Botta_Jansson_Ionescu,
  author =	 {Nicola Botta and Patrik Jansson and Cezar Ionescu},
  title =	 {Contributions to a computational theory of policy
                  advice and avoidability},
  journal =	 {Journal of Functional Programming},
  shortjournal = {J. Funct. Program.},
  issn =	 {0956-7968},
  publisher =	 {Cambridge University Press},
  volume =	 27,
  pages =	 {1--52},
  year =	 2017,
  DOI =		 {10.1017/S0956796817000156},
  COMMENTnote =	 {Accepted for publication 2017-09-20. Published
                  online 2017-10-24.},
  abstract =	 {We present the starting elements of a mathematical
                  theory of policy advice and avoidability. More
                  specifically, we formalize a cluster of notions
                  related to policy advice, such as policy, viability,
                  reachability, and propose a novel approach for
                  assisting decision making, based on the concept of
                  avoidability. We formalize avoidability as a
                  relation between current and future states,
                  investigate under which conditions this relation is
                  decidable and propose a generic procedure for
                  assessing avoidability. The formalization is
                  constructive and makes extensive use of the
                  correspondence between dependent types and logical
                  propositions, decidable judgments are obtained
                  through computations. Thus, we aim for a
                  computational theory, and emphasize the role that
                  computer science can play in global system science.}
}

@article{2014_Botta_et_al,
  author =	 {Nicola Botta and Patrik Jansson and Cezar Ionescu
                  and David R. Christiansen and Edwin Brady},
  bibsource =	 {dblp computer science bibliography, http://dblp.org},
  biburl =
                  {http://dblp.uni-trier.de/rec/bib/journals/corr/BottaJICB16},
  doi =		 {10.23638/LMCS-13(1:7)2017},
  journal =	 {Logical Methods in Computer Science},
  number =	 1,
  timestamp =	 {Wed, 03 May 2017 14:47:56 +0200},
  title =	 {Sequential decision problems, dependent types and
                  generic solutions},
  volume =	 13,
  year =	 2017
}

@phdthesis{ionescu2009,
  author =	 {Cezar Ionescu},
  school =	 {Freie Universit{\"a}t Berlin},
  title =	 {Vulnerability Modelling and Monadic Dynamical
                  Systems},
  url =		 {https://d-nb.info/1023491036/34},
  year =	 2009
}

@incollection{Ross2008-ROSGT,
  author =	 {Don Ross},
  booktitle =	 {Stanford Encyclopedia of Philosophy},
  title =	 {Game Theory},
  year =	 {2008}
}

@incollection{sep-decision-causal,
  author =	 {Paul Weirich},
  booktitle =	 {The Stanford Encyclopedia of Philosophy},
  edition =	 {Winter 2016},
  editor =	 {Edward N. Zalta},
Nicola Botta's avatar
Final.    
Nicola Botta committed
156
  howpublished = {\url{https://plato.stanford.edu/archives/win2016/entries/decision-causal/}},
Nicola Botta's avatar
Nicola Botta committed
157
158
159
160
161
162
163
164
165
166
167
168
  publisher =	 {Metaphysics Research Lab, Stanford University},
  title =	 {Causal Decision Theory},
  year =	 2016
}

@inproceedings{DBLP:conf/lics/Moggi89,
  author =	 {Eugenio Moggi},
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org},
  biburl =	 {https://dblp.org/rec/bib/conf/lics/Moggi89},
  booktitle =	 {Proceedings of the Fourth Annual Symposium on Logic
                  in Computer Science {(LICS} '89), Pacific Grove,
Nicola Botta's avatar
Final.    
Nicola Botta committed
169
                  California, USA, June 5--8, 1989},
Nicola Botta's avatar
Nicola Botta committed
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
  crossref =	 {DBLP:conf/lics/1989},
  doi =		 {10.1109/LICS.1989.39155},
  pages =	 {14--23},
  timestamp =	 {Wed, 16 Oct 2019 14:14:54 +0200},
  title =	 {Computational Lambda-Calculus and Monads},
  url =		 {https://doi.org/10.1109/LICS.1989.39155},
  year =	 1989
}

@article{DBLP:journals/cacm/Wadler15,
  author =	 {Philip Wadler},
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org},
  biburl =	 {https://dblp.org/rec/bib/journals/cacm/Wadler15},
  doi =		 {10.1145/2699407},
  journal =	 {Commun. {ACM}},
  number =	 12,
  pages =	 {75--84},
  timestamp =	 {Wed, 14 Nov 2018 10:22:36 +0100},
  title =	 {Propositions as types},
  url =		 {https://doi.org/10.1145/2699407},
  volume =	 58,
  year =	 2015
}

@inproceedings{DBLP:conf/fpca/Wadler89,
  author =	 {Philip Wadler},
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org},
  biburl =	 {https://dblp.org/rec/bib/conf/fpca/Wadler89},
  booktitle =	 {Proceedings of the fourth international conference
                  on Functional programming languages and computer
                  architecture, {FPCA} 1989, London, UK, September
Nicola Botta's avatar
Final.    
Nicola Botta committed
203
                  11--13, 1989},
Nicola Botta's avatar
Nicola Botta committed
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
  crossref =	 {DBLP:conf/fpca/1989},
  doi =		 {10.1145/99370.99404},
  pages =	 {347--359},
  timestamp =	 {Wed, 14 Nov 2018 10:57:36 +0100},
  title =	 {Theorems for Free!},
  url =		 {https://doi.org/10.1145/99370.99404},
  year =	 1989
}

@inproceedings{DBLP:conf/nato/Wadler92,
  author =	 {Philip Wadler},
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org},
  biburl =	 {https://dblp.org/rec/bib/conf/nato/Wadler92},
  booktitle =	 {Program Design Calculi, Proceedings of the {NATO}
                  Advanced Study Institute on Program Design Calculi,
                  Marktoberdorf, Germany, July 28 - August 9, 1992},
  crossref =	 {DBLP:conf/nato/1992pdc},
  doi =		 {10.1007/978-3-662-02880-3\_8},
  pages =	 {233--264},
  timestamp =	 {Sun, 14 May 2017 18:58:39 +0200},
  title =	 {Monads for functional programming},
  url =		 {https://doi.org/10.1007/978-3-662-02880-3\_8},
  year =	 1992
}

@book{DBLP:books/daglib/0096998,
  author =	 {Richard S. Bird and Oege de Moor},
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org},
  biburl =	 {https://dblp.org/rec/bib/books/daglib/0096998},
  isbn =	 {978-0-13-507245-5},
  publisher =	 {Prentice Hall},
Nicola Botta's avatar
Final.    
Nicola Botta committed
237
238
  series =	 {Prentice Hall International Series in Computer
                  Science},
Nicola Botta's avatar
Nicola Botta committed
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
  timestamp =	 {Thu, 03 Feb 2011 12:08:27 +0100},
  title =	 {Algebra of programming},
  year =	 {1997}
}

@book{DBLP:books/daglib/0073499,
  author =	 {Carroll Morgan},
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org},
  biburl =	 {https://dblp.org/rec/bib/books/daglib/0073499},
  isbn =	 {978-0-13-123274-7},
  publisher =	 {Prentice Hall},
  series =	 {Prentice Hall International series in computer
                  science},
  timestamp =	 {Thu, 22 Feb 2018 18:20:56 +0100},
  title =	 {Programming from specifications, 2nd Edition},
  year =	 1994
}

@article{Ionescu_2016,
  author =	 {Cezar Ionescu and Patrik Jansson},
  doi =		 {10.4204/eptcs.230.1},
  issn =	 {2075-2180},
  journal =	 {Electronic Proceedings in Theoretical Computer
                  Science},
  month =	 {Nov},
  pages =	 {1--15},
  publisher =	 {Open Publishing Association},
  title =	 {Domain-Specific Languages of Mathematics: Presenting
                  Mathematical Analysis Using Functional Programming},
  url =		 {http://dx.doi.org/10.4204/EPTCS.230.1},
  volume =	 230,
  year =	 2016
}

@misc{DSLsofMathProject,
  author =	 {Patrik Jansson and Cezar Ionescu},
  title =	 {Domain Specific Languages of Mathematics
                  (DSLsofMath)},
Nicola Botta's avatar
Final.    
Nicola Botta committed
278
279
  url =          {https://www.chalmers.se/en/projects/Pages/Domain-Specific-Languages-of-Mathematics-QDSLsofMathQ.aspx},
  year =	 {2014--2021}
Nicola Botta's avatar
Nicola Botta committed
280
281
282
}

@book{Kuznetsov:1998:EAB:289919,
Nicola Botta's avatar
Final.    
Nicola Botta committed
283
  address =	 {Berlin},
Nicola Botta's avatar
Nicola Botta committed
284
285
  author =	 {Yuri A. Kuznetsov},
  isbn =	 {0-387-98382-1},
Nicola Botta's avatar
Final.    
Nicola Botta committed
286
287
288
  publisher =	 {Springer},
  title =	 {Elements of Applied Bifurcation Theory},
  edition =      {2.},
Nicola Botta's avatar
Nicola Botta committed
289
290
291
292
293
294
295
296
297
298
  year =	 1998
}

@book{DBLP:books/daglib/0067018,
  author =	 {Carroll Morgan},
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org},
  biburl =	 {https://dblp.org/rec/bib/books/daglib/0067018},
  isbn =	 {978-0-13-726233-5},
  publisher =	 {Prentice Hall},
Nicola Botta's avatar
Final.    
Nicola Botta committed
299
300
  series =	 {Prentice Hall International Series in Computer
                  Science},
Nicola Botta's avatar
Nicola Botta committed
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
  timestamp =	 {Thu, 22 Feb 2018 18:20:56 +0100},
  title =	 {Programming from specifications},
  year =	 1990
}

@article{Reynolds1998,
  day =		 {01},
  doi =		 {10.1023/A:1010027404223},
  issn =	 {1573-0557},
  journal =	 {Higher-Order and Symbolic Computation},
  month =	 {Dec},
  number =	 {4},
  pages =	 {363--397},
  title =	 {Definitional Interpreters for Higher-Order
                  Programming Languages},
  url =		 {https://doi.org/10.1023/A:1010027404223},
  volume =	 {11},
  year =	 {1998}
}

@inbook{QuineVanHeijenoort,
  author =	 {W. Orman van Quine},
  booktitle =	 {From Frege to G{\"o}del: A Source Book in
                  Mathematical Logic, 1879-1931},
  editor =	 {J. {Van Heijenoort}},
  isbn =	 {9780674324497},
  lccn =	 {67010905},
  pages =	 {355--357},
  publisher =	 {Harvard University Press},
  series =	 {Source books in the history of the sciences},
  title =	 {Introduction to Moses Sch{\"o}nfinkel's "Bausteine
                  der mathematischen Logik"},
  url =		 {https://books.google.be/books?id=v4tBTBlU05sC},
  year =	 {1967}
}

@proceedings{DBLP:conf/lics/1989,
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org},
  biburl =	 {https://dblp.org/rec/bib/conf/lics/1989},
  isbn =	 {0-8186-1954-6},
  publisher =	 {{IEEE} Computer Society},
  timestamp =	 {Wed, 16 Oct 2019 14:14:54 +0200},
  title =	 {Proceedings of the Fourth Annual Symposium on Logic
                  in Computer Science {(LICS} '89), Pacific Grove,
Nicola Botta's avatar
Final.    
Nicola Botta committed
346
                  California, USA, June 5--8, 1989},
Nicola Botta's avatar
Nicola Botta committed
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
  url =
                  {https://ieeexplore.ieee.org/xpl/conhome/249/proceeding},
  year =	 1989
}

@proceedings{DBLP:conf/fpca/1989,
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org},
  biburl =	 {https://dblp.org/rec/bib/conf/fpca/1989},
  doi =		 {10.1145/99370},
  editor =	 {Joseph E. Stoy},
  isbn =	 {0-201-51389-7},
  publisher =	 {{ACM}},
  timestamp =	 {Tue, 06 Nov 2018 11:07:48 +0100},
  title =	 {Proceedings of the fourth international conference
                  on Functional programming languages and computer
                  architecture, {FPCA} 1989, London, UK, September
Nicola Botta's avatar
Final.    
Nicola Botta committed
364
                  11--13, 1989},
Nicola Botta's avatar
Nicola Botta committed
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
  url =		 {https://doi.org/10.1145/99370},
  year =	 1989
}

@proceedings{DBLP:conf/nato/1992pdc,
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org},
  biburl =	 {https://dblp.org/rec/bib/conf/nato/1992pdc},
  doi =		 {10.1007/978-3-662-02880-3},
  editor =	 {Manfred Broy},
  isbn =	 {978-3-642-08164-4},
  publisher =	 {Springer},
  series =	 {{NATO} {ASI} Series},
  timestamp =	 {Sun, 14 May 2017 18:55:41 +0200},
  title =	 {Program Design Calculi, Proceedings of the {NATO}
                  Advanced Study Institute on Program Design Calculi,
                  Marktoberdorf, Germany, July 28 - August 9, 1992},
  url =		 {https://doi.org/10.1007/978-3-662-02880-3},
  volume =	 118,
  year =	 1993
}

@book{curryFeys,
  title =	 {Combinatory Logic},
  author =	 {Curry, H.B. and Feys, R.},
  number =	 {v. 1},
  lccn =	 {a59001593},
  series =	 {Combinatory Logic},
  url =		 {https://books.google.be/books?id=fEnuAAAAMAAJ},
  year =	 1958,
  publisher =	 {North-Holland Publishing Company}
}

@book{bird2014thinking,
  title =	 {Thinking Functionally with {H}askell},
  author =	 {Bird, R.},
  isbn =	 9781107087200,
  lccn =	 2014024954,
  url =		 {https://books.google.de/books?id=B4RxBAAAQBAJ},
  year =	 2014,
  publisher =	 {Cambridge University Press}
}

@misc{HuttonCT,
  author =	 {Graham Hutton},
  comment =	 "Slides - not a published book",
  title =	 {Introduction to Category Theory},
  url =		 {http://www.cs.nott.ac.uk/~pszgmh/cat.html},
  year =	 2010
}

@article{10.1017/S0956796805005721,
  author =	 {Erwig, Martin and Kollmansberger, Steve},
  title =	 {{FUNCTIONAL PEARLS}: Probabilistic Functional
                  Programming in {Haskell}},
  year =	 2006,
  issue_date =	 {January 2006},
  publisher =	 {Cambridge University Press},
  volume =	 16,
  number =	 1,
  issn =	 {0956-7968},
  url =		 {https://doi.org/10.1017/S0956796805005721},
  doi =		 {10.1017/S0956796805005721},
Nicola Botta's avatar
Final.    
Nicola Botta committed
428
  journal =	 {Journal of Functional Programming},
Nicola Botta's avatar
Nicola Botta committed
429
  month =	 jan,
Nicola Botta's avatar
Final.    
Nicola Botta committed
430
  pages =	 {21--34},
Nicola Botta's avatar
Nicola Botta committed
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
  numpages =	 14
}

@article{Avery_2016,
  title =	 {Codensity and the {G}iry monad},
  volume =	 220,
  ISSN =	 {0022-4049},
  url =		 {http://dx.doi.org/10.1016/j.jpaa.2015.08.017},
  DOI =		 {10.1016/j.jpaa.2015.08.017},
  number =	 3,
  journal =	 {Journal of Pure and Applied Algebra},
  publisher =	 {Elsevier BV},
  author =	 {Avery, Tom},
  year =	 2016,
  month =	 {Mar},
Nicola Botta's avatar
Final.    
Nicola Botta committed
446
  pages =	 {1229--1251}
Nicola Botta's avatar
Nicola Botta committed
447
448
449
450
451
452
453
454
}

@phdthesis{norell2007thesis,
  author =	 {Norell, Ulf},
  keywords =	 {Dependent Types},
  school =	 {Chalmers University of Technology},
  title =	 {Towards a practical programming language based on
                  dependent type theory},
Nicola Botta's avatar
Final.    
Nicola Botta committed
455
  url =          {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7934&rep=rep1&type=pdf},
Nicola Botta's avatar
Nicola Botta committed
456
457
458
459
460
461
  volume =	 32,
  doi =		 {10.1.1.436.7331},
  year =	 2007
}

@book{martinlof1984,
Nicola Botta's avatar
Final.    
Nicola Botta committed
462
463
464
465
466
  author =	 {Martin-L{\"o}f, Per and Sambin, Giovanni},
  title =	 {Intuitionistic type theory},
  volume =       {9},
  publisher =	 {Bibliopolis Naples},
  year =	 1984
Nicola Botta's avatar
Nicola Botta committed
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
}

@Incollection{giry1981,
  author =	 "Giry, M.",
  title =	 {A categorial approach to probability theory},
  editor =	 {Banaschewski, B.},
  booktitle =	 {Categorical Aspects of Topology and Analysis},
  series =	 {Lecture Notes in Mathematics},
  volume =	 915,
  publisher =	 {Springer},
  address =	 {Berlin},
  pages =	 {68--85},
  year =	 1981
}

482
483
484
485
486
487
488
489
490
@misc{CoqProofAssistant,
  author       = {{The Coq Development Team}},
  title        = {The Coq Proof Assistant (Version 8.13.0)},
  month        = jan,
  year         = 2021,
  publisher    = {Zenodo},
  version      = {8.13},
  doi          = {10.5281/zenodo.4501022},
  howpublished = {\url{https://doi.org/10.5281/zenodo.4501022}}
Nicola Botta's avatar
Nicola Botta committed
491
492
493
494
495
496
}

@book{nordstrom1990programming,
  title =	 {Programming in {M}artin-{L}{\"o}f’s type theory},
  author =	 {Nordstr{\"o}m, Bengt and Petersson, Kent and Smith,
                  Jan M},
Nicola Botta's avatar
Final.    
Nicola Botta committed
497
  series =       {International Series of Monographs on Computer Science},
Nicola Botta's avatar
Nicola Botta committed
498
499
  volume =	 200,
  year =	 1990,
Nicola Botta's avatar
Final.    
Nicola Botta committed
500
  publisher =	 {Oxford University Press}
Nicola Botta's avatar
Nicola Botta committed
501
502
503
504
}

@misc{brede2020,
  author =	 {Brede, Nuria and Botta, Nicola},
505
  title =	 {On the correctness of monadic backward induction},
Nicola Botta's avatar
Final.    
Nicola Botta committed
506
  howpublished = {Submitted to Journal of Functional Programming, \url{https://arxiv.org/abs/2008.02143}},
507
  year =	 2021
Nicola Botta's avatar
Nicola Botta committed
508
509
510
511
512
513
514
}

@article{gnesi1981dynamic,
  title =	 {Dynamic programming as graph searching: An algebraic
                  approach},
  author =	 {Gnesi, Stefania and Montanari, Ugo and Martelli,
                  Alberto},
Nicola Botta's avatar
Final.    
Nicola Botta committed
515
  journal =	 {Journal of the {ACM}},
Nicola Botta's avatar
Nicola Botta committed
516
517
518
519
  volume =	 28,
  number =	 4,
  pages =	 {737--751},
  year =	 1981,
Nicola Botta's avatar
Final.    
Nicola Botta committed
520
  publisher =	 {ACM}
Nicola Botta's avatar
Nicola Botta committed
521
522
523
524
525
}

@inproceedings{de_moor1995,
  author =	 {De Moor, Oege},
  title =	 {A generic program for sequential decision processes},
Nicola Botta's avatar
Final.    
Nicola Botta committed
526
527
528
529
  booktitle =	 {{PLILPS} '95
                  Symposium on Programming Languages: Implementations,
                  Logics and Programs},
  longbooktitle =	 {{PLILPS} '95 Proceedings of the 7th International
Nicola Botta's avatar
Nicola Botta committed
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
                  Symposium on Programming Languages: Implementations,
                  Logics and Programs},
  pages =	 {1--23},
  publisher =	 {Springer},
  year =	 1995,
}

@article{de_moor1999,
  title =	 {Dynamic programming as a software component},
  author =	 {De Moor, Oege},
  journal =	 {Proc. 3rd {WSEAS} Int. Conf. Circuits, Systems,
                  Communications and Computers ({CSCC} 1999)},
  pages =	 {4--8},
  year =	 1999
}

@article{sozeau2010new,
  title =	 {A new look at generalized rewriting in type theory},
  author =	 {Sozeau, Matthieu},
Nicola Botta's avatar
Final.    
Nicola Botta committed
549
  journal =	 {Journal of Formalized Reasoning},
Nicola Botta's avatar
Nicola Botta committed
550
551
552
553
554
555
556
  volume =	 2,
  number =	 1,
  pages =	 {41--62},
  year =	 2010
}


Nicola Botta's avatar
Final.    
Nicola Botta committed
557
@phdthesis{hofmann1995extensional,
Nicola Botta's avatar
Nicola Botta committed
558
  title =	 {Extensional concepts in intensional type theory},
Nicola Botta's avatar
Final.    
Nicola Botta committed
559
  school =       {University of Edinburgh},
Nicola Botta's avatar
Nicola Botta committed
560
561
562
563
  author =	 {Hofmann, Martin},
  year =	 1995,
  publisher =	 {University of Edinburgh. College of Science and
                  Engineering.},
Nicola Botta's avatar
Final.    
Nicola Botta committed
564
  URL =          {https://www.lfcs.inf.ed.ac.uk/reports/95/ECS-LFCS-95-327/}
Nicola Botta's avatar
Nicola Botta committed
565
566
567
568
}

@book{hofmann2012extensional,
  title =	 {Extensional constructs in intensional type theory},
Nicola Botta's avatar
Final.    
Nicola Botta committed
569
  doi =          {10.1007/978-1-4471-0963-1},
Nicola Botta's avatar
Nicola Botta committed
570
  author =	 {Hofmann, Martin},
Nicola Botta's avatar
Final.    
Nicola Botta committed
571
  series=        {Distinguished Dissertations},
Nicola Botta's avatar
Nicola Botta committed
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
  year =	 2012,
  publisher =	 {Springer Science \& Business Media}
}

@article{mu2009algebra,
  title =	 {Algebra of programming in {A}gda: dependent types
                  for relational program derivation},
  author =	 {Mu, Shin-Cheng and Ko, Hsiang-Shang and Jansson,
                  Patrik},
  journal =	 {Journal of Functional Programming},
  volume =	 19,
  number =	 5,
  pages =	 {545--579},
  year =	 2009,
  publisher =	 {Cambridge University Press}
}

@inproceedings{wadler1992essence,
  title =        {The essence of functional programming},
  author =       {Wadler, Philip},
Nicola Botta's avatar
Final.    
Nicola Botta committed
592
593
  booktitle =    {{ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages},
  longbooktitle =    {Proceedings of the 19th {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages},
Nicola Botta's avatar
Nicola Botta committed
594
595
596
597
  pages =        {1--14},
  year =         {1992}
}

Nicola Botta's avatar
Final.    
Nicola Botta committed
598
@article{streicher2003category_old,
Nicola Botta's avatar
Nicola Botta committed
599
600
601
602
603
604
605
  title =        {Category {T}heory and {C}ategorical {L}ogic},
  author =       {Streicher, Thomas},
  journal =      {Lecture {N}otes, {T}echnische {U}niversit{\"a}t {D}armstadt,
	          https://www2.mathematik.tu-darmstadt.de/~streicher/CTCL.pdf},
  year =         {2003}
}

Nicola Botta's avatar
Final.    
Nicola Botta committed
606
607
608
609
610
611
612
613
614
@misc{streicher2003category,
  title =        {Category {T}heory and {C}ategorical {L}ogic},
  author =       {Streicher, Thomas},
  howpublished = {Lecture {N}otes, {T}echnische {U}niversit{\"a}t {D}armstadt,
	          \url{https://www2.mathematik.tu-darmstadt.de/~streicher/CTCL.pdf}},
  year =         {2003}
}

@misc{dawson2007compound,
Nicola Botta's avatar
Nicola Botta committed
615
616
  title =        {Compound monads and the {K}leisli category},
  author =       {Dawson, Jeremy E},
Nicola Botta's avatar
Final.    
Nicola Botta committed
617
  howpublished = {unpublished note, http://users. cecs. anu. edu. au/jeremy/pubs/cmkc/cmkc. pdf},
Nicola Botta's avatar
Nicola Botta committed
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
  year =         2007
}


@article{barthe2003setoids,
  title =	 {Setoids in type theory},
  author =	 {Barthe, Gilles and Capretta, Venanzio and Pons,
                  Olivier},
  journal =	 {Journal of Functional Programming},
  volume =	 13,
  number =	 2,
  pages =	 261,
  year =	 2003,
  publisher =	 {Cambridge University Press}
}

@book{thomas2012catastrophe,
  title =	 {Catastrophe Theory},
  author =	 {Thomas, R.K. and Arnol'd, V.I.},
  isbn =	 9783642967993,
  lccn =	 83020031,
  url =		 {https://books.google.de/books?id=kQT8CAAAQBAJ},
  year =	 2012,
Nicola Botta's avatar
Final.    
Nicola Botta committed
641
  publisher =	 {Springer}
Nicola Botta's avatar
Nicola Botta committed
642
643
644
}

@Book{hottbook,
Nicola Botta's avatar
Final.    
Nicola Botta committed
645
646
647
648
649
650
  author =       {{The Univalent Foundations Program}},
  title =        {Homotopy Type Theory: Univalent Foundations of Mathematics},
  publisher =    {\url{https://homotopytypetheory.org/book}},
  address =      {Institute for Advanced Study},
  year =         2013
}
Nicola Botta's avatar
Nicola Botta committed
651
652

@book{DBLP:books/daglib/0067012,
Nicola Botta's avatar
Final.    
Nicola Botta committed
653
654
655
656
657
658
659
660
661
662
663
  author    =    {Thomas Streicher},
  title     =    {Semantics of type theory - correctness, completeness and independence
                  results},
  series    =    {Progress in Theoretical Computer Science},
  publisher =    {Birkh{\"{a}}user},
  year      =    {1991},
  isbn      =    {978-0-8176-3594-7},
  timestamp =    {Wed, 17 Jul 2019 17:20:52 +0200},
  biburl    =    {https://dblp.org/rec/books/daglib/0067012.bib},
  bibsource =    {dblp computer science bibliography, https://dblp.org}
}
Nicola Botta's avatar
Nicola Botta committed
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695

@inproceedings{10.5555/788021.788977,
  author =	 {Altenkirch, Thorsten},
  title =	 {Extensional Equality in Intensional Type Theory},
  year =	 1999,
  isbn =	 0769501583,
  publisher =	 {IEEE Computer Society},
  address =	 {USA},
  booktitle =	 {Proceedings of the 14th Annual IEEE Symposium on
                  Logic in Computer Science},
  pages =	 412,
  numpages =	 1,
  keywords =	 {categorical models, Type Theory},
  series =	 {LICS ’99}
}

@article{Palmgren_2014,
  title =	 {Constructing categories and setoids of setoids in
                  type theory},
  volume =	 10,
  ISSN =	 {1860-5974},
  url =		 {http://dx.doi.org/10.2168/LMCS-10(3:25)2014},
  DOI =		 {10.2168/lmcs-10(3:25)2014},
  number =	 3,
  journal =	 {Logical Methods in Computer Science},
  author =	 {Palmgren, Erik and Wilander, Olov},
  editor =	 {Escardó, Martín},
  year =	 2014,
  month =	 {Sep}
}

@article{KINOSHITA2014145,
Nicola Botta's avatar
Final.    
Nicola Botta committed
696
697
  title =	 {Category theoretic structure of setoids},
  journal =	 {Theoretical Computer Science},
Nicola Botta's avatar
Nicola Botta committed
698
  volume =	 546,
Nicola Botta's avatar
Final.    
Nicola Botta committed
699
  pages =	 {145--163},
Nicola Botta's avatar
Nicola Botta committed
700
  year =	 2014,
Nicola Botta's avatar
Final.    
Nicola Botta committed
701
702
703
704
705
706
707
  note =	 {Models of Interaction: Essays in Honour of Glynn
                  Winskel},
  issn =	 {0304-3975},
  doi =		 {https://doi.org/10.1016/j.tcs.2014.03.006},
  url =          {http://www.sciencedirect.com/science/article/pii/S0304397514001819},
  author =	 {Yoshiki Kinoshita and John Power},
  keywords =	 {Setoid, Proof assistant, Proof irrelevance,
Nicola Botta's avatar
Nicola Botta committed
708
                  Cartesian closed category, Coproduct, -category,
Nicola Botta's avatar
Final.    
Nicola Botta committed
709
710
                  -inserter, -category, -coinserter},
  abstract =	 {A setoid is a set together with a constructive
Nicola Botta's avatar
Nicola Botta committed
711
712
713
714
715
716
717
718
719
720
721
722
723
724
                  representation of an equivalence relation on
                  it. Here, we give category theoretic support to the
                  notion. We first define a category Setoid and prove
                  it is Cartesian closed with coproducts. We then
                  enrich it in the Cartesian closed category Equiv of
                  sets and classical equivalence relations, extend the
                  above results, and prove that Setoid as an
                  Equiv-enriched category has a relaxed form of
                  equalisers. We then recall the definition of
                  E-category, generalising that of Equiv-enriched
                  category, and show that Setoid as an E-category has
                  a relaxed form of coequalisers. In doing all this,
                  we carefully compare our category theoretic
                  constructs with Agda code for type-theoretic
Nicola Botta's avatar
Final.    
Nicola Botta committed
725
                  constructs on setoids.}
Nicola Botta's avatar
Nicola Botta committed
726
727
728
}

@inproceedings{DBLP:conf/lics/HofmannS94,
Nicola Botta's avatar
Final.    
Nicola Botta committed
729
730
731
732
733
734
735
736
737
738
739
740
  author    =    {Martin Hofmann and Thomas Streicher},
  title     =    {The Groupoid Model Refutes Uniqueness of Identity Proofs},
  booktitle =    {Proc. Symposium on Logic in Computer Science {(LICS} '94)},
  longbooktitle =    {Proceedings of the Ninth Annual Symposium on Logic in Computer Science
                  {(LICS} '94), Paris, France, July 4--7, 1994},
  pages     =    {208--212},
  year      =    {1994},
  url       =    {https://doi.org/10.1109/LICS.1994.316071},
  doi       =    {10.1109/LICS.1994.316071},
  timestamp =    {Wed, 16 Oct 2019 14:14:54 +0200},
  biburl    =    {https://dblp.org/rec/conf/lics/HofmannS94.bib},
  bibsource =    {dblp computer science bibliography, https://dblp.org}
Nicola Botta's avatar
Nicola Botta committed
741
742
743
}

@article{DBLP:journals/jfp/AbelCDTW20,
Nicola Botta's avatar
Final.    
Nicola Botta committed
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
  author    =    {Andreas Abel and Jesper Cockx and
                  Dominique Devriese and Amin Timany and
                  Philip Wadler},
  title     =    {Leibniz equality is isomorphic to Martin-L{\"{o}}f identity,
                  parametrically},
  journal =	 {Journal of Functional Programming},
  shortjournal = {J. Funct. Program.},
  volume    =    {30},
  pages     =    {e17},
  year      =    {2020},
  url       =    {https://doi.org/10.1017/S0956796820000155},
  doi       =    {10.1017/S0956796820000155},
  timestamp =    {Mon, 29 Jun 2020 18:01:27 +0200},
  biburl    =    {https://dblp.org/rec/journals/jfp/AbelCDTW20.bib},
  bibsource =    {dblp computer science bibliography, https://dblp.org}
Nicola Botta's avatar
Nicola Botta committed
759
760
761
}

@book{Bishop1967-BISFOC-3,
Nicola Botta's avatar
Final.    
Nicola Botta committed
762
763
764
765
  title =        {Foundations of Constructive Analysis},
  author =       {Errett Bishop},
  publisher =    {McGraw-Hill},
  year =         {1967}
Nicola Botta's avatar
Nicola Botta committed
766
767
768
}

@article{spitters_vanderweegen_2011,
Nicola Botta's avatar
Final.    
Nicola Botta committed
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
  title =        {Type classes for mathematics in type theory},
  author =       {Spitters, Bas and van der Weegen, Eelis},
  volume =       {21},
  doi =          {10.1017/S0960129511000119},
  number =       {4},
  journal =      {Mathematical Structures in Computer Science},
  publisher =    {Cambridge University Press},
  year =         {2011},
  pages =        {795–825}
}

@misc{selsam2020tabled,
  title =        {Tabled Typeclass Resolution},
  author =       {Daniel Selsam and Sebastian Ullrich and Leonardo de Moura},
  year =         {2020},
  eprint =       {2001.04301},
  archivePrefix ={arXiv},
  primaryClass = {cs.PL}
}

@article{Krebbers_2013,
  title =        {Type classes for efficient exact real arithmetic in {Coq}},
  volume =       {9},
  number =       {1},
  ISSN =         {1860-5974},
  url =          {https://lmcs.episciences.org/958},
  DOI =          {10.2168/lmcs-9(1:1)2013},
  journal =      {Logical Methods in Computer Science},
  author =       {Krebbers, Robbert and Spitters, Bas},
  editor =       {Escardó, Martín},
  year =         {2013},
  month =        Feb
}

@inproceedings{10.1007/978-3-540-71067-7_23,
  author =       {Sozeau, Matthieu and Oury, Nicolas},
  editor =       {Mohamed, Otmane Ait and Mu{\~{n}}oz, C{\'e}sar
                  and Tahar, Sofi{\`e}ne},
  title =        {First-Class Type Classes},
  booktitle =    {Theorem Proving in Higher Order Logics},
  year =         {2008},
  publisher =    {Springer},
  address =      {Berlin},
  pages =        {278--293},
  isbn =         {978-3-540-71067-7}
Nicola Botta's avatar
Nicola Botta committed
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
}

@article{cohen2016cubical,
  oldkey =	 {DBLP:journals/corr/CohenCHM16},
  author =	 {Cyril Cohen and Thierry Coquand and Simon Huber and
                  Anders M{\"{o}}rtberg},
  title =	 {Cubical Type Theory: a constructive interpretation
                  of the univalence axiom},
  journal =	 {CoRR},
  volume =	 {abs/1611.02108},
  year =	 2016,
  url =		 {http://arxiv.org/abs/1611.02108},
  archivePrefix ={arXiv},
  eprint =	 {1611.02108},
  timestamp =	 {Mon, 13 Aug 2018 16:48:16 +0200},
  biburl =	 {https://dblp.org/rec/journals/corr/CohenCHM16.bib},
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org}
}

Nicola Botta's avatar
Final.    
Nicola Botta committed
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
@inproceedings{cohenetal18:cubical,
  author =	 {Cyril Cohen and Thierry Coquand and Simon Huber and Anders M{\"o}rtberg},
  title =	 {{Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom}},
  booktitle =	 {Proc. {TYPES} 2015},
  longbooktitle =	 {21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  pages =	 {5:1--5:34},
  series =	 {Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	 {978-3-95977-030-9},
  ISSN =	 {1868-8969},
  year =	 {2018},
  volume =	 {69},
  commenteditor =	 {Tarmo Uustalu},
  publisher =	 {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	 {Dagstuhl, Germany},
  URL =		 {http://drops.dagstuhl.de/opus/volltexte/2018/8475},
  URN =		 {urn:nbn:de:0030-drops-84754},
  doi =		 {10.4230/LIPIcs.TYPES.2015.5},
  annote =	 {Keywords: univalence axiom, dependent type theory, cubical sets}
}

Nicola Botta's avatar
Nicola Botta committed
854
@article{10.1145/3341691,
Nicola Botta's avatar
Final.    
Nicola Botta committed
855
  author =	 {Vezzosi, Andrea and M\"{o}rtberg, Anders and Abel, Andreas},
Nicola Botta's avatar
Nicola Botta committed
856
857
858
859
  title =	 {Cubical {Agda}: A Dependently Typed Programming
                  Language with Univalence and Higher Inductive Types},
  year =	 2019,
  issue_date =	 {August 2019},
Nicola Botta's avatar
Final.    
Nicola Botta committed
860
  publisher =	 {ACM},
Nicola Botta's avatar
Nicola Botta committed
861
862
863
864
865
866
867
868
869
870
871
872
873
  address =	 {New York, NY, USA},
  volume =	 3,
  number =	 {ICFP},
  url =		 {https://doi.org/10.1145/3341691},
  doi =		 {10.1145/3341691},
  journal =	 {Proc. {ACM} Program. Lang.},
  month =	 jul,
  articleno =	 87,
  numpages =	 29,
  keywords =	 {Dependent Pattern Matching, Higher Inductive Types,
                  Cubical Type Theory, Univalence}
}

Nicola Botta's avatar
Final.    
Nicola Botta committed
874
875
876
877
878
879
880
881
882
883
884
885
@article{cubicalagda2,
  title = 	 {Cubical {Agda}: A dependently typed programming language with univalence and higher inductive types},
  volume =	 {31},
  doi =		 {10.1017/S0956796821000034},
  journal =	 {Journal of Functional Programming},
  publisher =	 {Cambridge University Press},
  author = 	 {Vezzosi, Andrea and M{\"o}rtberg, Anders and Abel, Andreas},
  year =	 {2021},
  pages =        {e8}
}


Nicola Botta's avatar
Nicola Botta committed
886
887
888
@misc{CoRN_library,
  author =	 {Spitters, Bas and Semeria, Vincent (Maintainers)},
  howpublished = {\url{https://github.com/coq-community/corn}},
889
890
891
892
  title =	 {Coq Repository at Nijmegen (Version 1.2.0)},
  year =	 {2017}
}

Nicola Botta's avatar
Final.    
Nicola Botta committed
893
894
895
896
897
898
899
900
901
902
903
904
@inproceedings{10.1007/978-3-540-27818-4_7,
  author =       {Cruz-Filipe, Lu{\'i}s and Geuvers, Herman
                  and Wiedijk, Freek},
  editor =       {Asperti, Andrea and Bancerek, Grzegorz
                  and Trybulec, Andrzej},
  title =        {C-CoRN, the Constructive Coq Repository at Nijmegen},
  booktitle =    {Mathematical Knowledge Management},
  year =         2004,
  publisher =    {Springer},
  address =      {Berlin},
  pages =        {88--103},
  isbn =         {978-3-540-27818-4}
Nicola Botta's avatar
Nicola Botta committed
905
906
907
908
909
}

@misc{CoLoR_library,
  author =	 {Frederic Blanqui and others},
  howpublished = {\url{https://github.com/fblanqui/color}},
910
911
  title =	 {CoLoR: a Coq Library on Rewriting and termination (Version 1.8.0)},
  year =	 {2020}
Nicola Botta's avatar
Nicola Botta committed
912
913
}

914
@article{blanqui_koprowski_2011,
Nicola Botta's avatar
Final.    
Nicola Botta committed
915
916
917
918
919
920
921
922
923
924
925
  title =        {CoLoR: a Coq library on well-founded rewrite relations and
	          its application to the automated verification of termination
	          certificates},
  volume =       {21},
  doi =          {10.1017/S0960129511000120},
  number =       {4},
  journal =      {Mathematical Structures in Computer Science},
  publisher =    {Cambridge University Press},
  author =       {Blanqui, Fred{\'e}d{\'e}ric and Koprowski, Adam},
  year =         {2011},
  pages =        {827--859}}
926

Nicola Botta's avatar
Nicola Botta committed
927
928
929
@misc{arend_prover,
  author =	 {{JetBrains Research}},
  howpublished = {\url{https://arend-lang.github.io/}},
930
931
  title =	 {Arend Theorem Prover (Version 1.6.0)},
  year =	 {2021}
Nicola Botta's avatar
Nicola Botta committed
932
933
934
935
936
937
938
939
940
}

@Misc{UniMath,
  author =	 {Voevodsky, Vladimir and Ahrens, Benedikt and
                  Grayson, Daniel and others},
  title =	 {{UniMath} --- a computer-checked library of
                  univalent mathematics},
  url =		 {https://github.com/UniMath/UniMath},
  howpublished = {Available at
941
942
                  \url{https://github.com/UniMath/UniMath}},
  year = {2021}
Nicola Botta's avatar
Nicola Botta committed
943
944
945
946
947
}

@book{pierce_basic_1991,
  author =	 {Benjamin C. Pierce},
  title =	 {Basic Category Theory for Computer Scientists},
Nicola Botta's avatar
Final.    
Nicola Botta committed
948
  series =	 {Foundations of Computing Series},
Nicola Botta's avatar
Nicola Botta committed
949
  isbn =	 {978-0-262-66071-6},
Nicola Botta's avatar
Final.    
Nicola Botta committed
950
  publisher =	 {MIT},
Nicola Botta's avatar
Nicola Botta committed
951
952
953
954
955
956
957
958
  biburl =	 {https://dblp.org/rec/books/daglib/0069193.bib},
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org},
  year =	 1991
}

@Misc{carette_agda,
  author =	 {Jacques Carette and Jason Z. S. Hu},
959
  title =	 {A new Categories library for {Agda} (Version 0.1.5)},
Nicola Botta's avatar
Nicola Botta committed
960
  howpublished = {\url{https://github.com/agda/agda-categories}},
961
  year =	 2021
Nicola Botta's avatar
Nicola Botta committed
962
963
964
}

@Misc{wiegley_coq,
Nicola Botta's avatar
Final.    
Nicola Botta committed
965
966
967
968
969
  author =       {Wiegley, John},
  title  =       {Category Theory in {Coq}},
  howpublished = {Available from \url{https://github.com/jwiegley/category-theory}},
  year =         {2018},
  COMMENTyear =         {2014--2018}
Nicola Botta's avatar
Nicola Botta committed
970
971
972
}

@Misc{megasz_coq,
Nicola Botta's avatar
Final.    
Nicola Botta committed
973
974
975
976
  author =       {Megacz, Adam},
  title  =       {Category Theory in {Coq} (coq-categories)},
  howpublished = {\url{http://www.megacz.com/berkeley/coq-categories/}},
  year =         2011
Nicola Botta's avatar
Nicola Botta committed
977
978
}

Nicola Botta's avatar
Final.    
Nicola Botta committed
979
980
981
982
983
984
985
986
@incollection{huet_saibi,
  author    =    {G{\'e}rard Huet and Amokrane Sa{\"i}bi},
  title     =    {Constructive category theory},
  booktitle =    {Proof, Language, and Interaction. Essays in Honor of Robin Milnor},
  editor    =    {Gordon Plotkin and Colin Stirling and Mads Tofte},
  publisher =    {MIT},
  year      =    {2000},
  pages     =    {239--275},
Nicola Botta's avatar
Nicola Botta committed
987
988
989
}

@Misc{altenkirch_setoidhell,
Nicola Botta's avatar
Final.    
Nicola Botta committed
990
991
992
993
  author =       {Altenkirch, Thorsten},
  title  =       {From setoid hell to homotopy heaven?},
  howpublished = {\url{https://www.cs.nott.ac.uk/~psztxa/talks/types-17-hell.pdf}},
  year =         {2017}
Nicola Botta's avatar
Nicola Botta committed
994
995
996
}

@inproceedings{DBLP:conf/mpc/AltenkirchBKT19,
Nicola Botta's avatar
Final.    
Nicola Botta committed
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
  author    =    {Thorsten Altenkirch and Simon Boulier and
                  Ambrus Kaposi and Nicolas Tabareau},
  editor    =    {Graham Hutton},
  title     =    {Setoid Type Theory - {A} Syntactic Translation},
  booktitle =    {Mathematics of Program Construction - 13th International Conference,
                  {MPC} 2019, Porto, Portugal, October 7--9, 2019, Proceedings},
  series    =    {Lecture Notes in Computer Science},
  volume    =    {11825},
  pages     =    {155--196},
  publisher =    {Springer},
  year      =    2019,
  url       =    {https://doi.org/10.1007/978-3-030-33636-3\_7},
  doi       =    {10.1007/978-3-030-33636-3\_7},
  timestamp =    {Tue, 22 Oct 2019 16:07:29 +0200},
  biburl    =    {https://dblp.org/rec/conf/mpc/AltenkirchBKT19.bib},
  bibsource =    {dblp computer science bibliography, https://dblp.org}
Nicola Botta's avatar
Nicola Botta committed
1013
1014
1015
}

@inproceedings{DBLP:conf/plpv/AltenkirchMS07,
Nicola Botta's avatar
Final.    
Nicola Botta committed
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
  author    =    {Thorsten Altenkirch and Conor McBride and
                  Wouter Swierstra},
  editor    =    {Aaron Stump and Hongwei Xi},
  title     =    {Observational equality, now!},
  booktitle =    {Proceedings of the {ACM} Workshop Programming Languages meets Program
                  Verification, {PLPV} 2007, Freiburg, Germany, October 5, 2007},
  pages     =    {57--68},
  publisher =    {{ACM}},
  year      =    {2007},
  url       =    {https://doi.org/10.1145/1292597.1292608},
  doi       =    {10.1145/1292597.1292608},
  timestamp =    {Sun, 02 Jun 2019 21:19:59 +0200},
  biburl    =    {https://dblp.org/rec/conf/plpv/AltenkirchMS07.bib},
  bibsource =    {dblp computer science bibliography, https://dblp.org}
Nicola Botta's avatar
Nicola Botta committed
1030
1031
}
@book{manes1976algebraic,
Nicola Botta's avatar
Final.    
Nicola Botta committed
1032
1033
1034
1035
  title     =    {Algebraic {T}heories},
  author    =    {Manes, Ernest G},
  year      =    {1976},
  publisher =    {Springer}
Nicola Botta's avatar
Nicola Botta committed
1036
1037
1038
1039
1040
}

@inproceedings{jeuringHaskell12ClassLaws,
  author =	 {Johan Jeuring and Patrik Jansson and Cl\'audio
                  Amaral},
Nicola Botta's avatar
Final.    
Nicola Botta committed
1041
  booktitle =	 {Proceedings of the 2012 Haskell Symposium},
Nicola Botta's avatar
Nicola Botta committed
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
  pages =	 {49--60},
  publisher =	 {ACM},
  title =	 {Testing type class laws},
  year =	 2012,
  doi =		 {10.1145/2364506.2364514},
}

@article{DBLP:journals/corr/abs-1808-05789,
  author =	 {Andreas Arvidsson and Moa Johansson and Robin
                  Touche},
  title =	 {Proving Type Class Laws for {Haskell}},
  journal =	 {CoRR},
  volume =	 {abs/1808.05789},
  year =	 2018,
  url =		 {http://arxiv.org/abs/1808.05789},
  archivePrefix ={arXiv},
  eprint =	 {1808.05789},
  timestamp =	 {Sun, 02 Sep 2018 15:01:56 +0200},
Nicola Botta's avatar
Final.    
Nicola Botta committed
1060
  biburl =       {https://dblp.org/rec/journals/corr/abs-1808-05789.bib},
Nicola Botta's avatar
Nicola Botta committed
1061
1062
1063
1064
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org}
}

Nicola Botta's avatar
Final.    
Nicola Botta committed
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
@InProceedings{arvidssonetal19:typeclasslaws,
  author =       {Arvidsson, Andreas and Johansson, Moa and Touche, Robin},
  editor =       {Van Horn, David and Hughes, John},
  title =        {Proving Type Class Laws for {Haskell}},
  booktitle =    {Trends in Functional Programming},
  year =         2019,
  publisher =    {Springer},
  address =      {Cham},
  pages =        {61--74},
  abstract =     {Type classes in Haskell are used to implement ad-hoc polymorphism,
	         i.e. a way to ensure both to the programmer and the compiler that
	         a set of functions are defined for a specific data type. All instances
		 of such type classes are expected to behave in a certain way and
		 satisfy laws associated with the respective class. These are however
		 typically just stated in comments and as such, there is no real way
		 to enforce that they hold. In this paper we describe a system which
		 allows the user to write down type class laws which are then
		 automatically instantiated and sent to an inductive theorem prover
		 when declaring a new instance of a type class.},
  isbn =         {978-3-030-14805-8}
}

Nicola Botta's avatar
Nicola Botta committed
1087
1088
1089
@inproceedings{danielssonetal06:fastandloose,
  author =	 {Nils Anders Danielsson and John Hughes and Patrik
                  Jansson and Jeremy Gibbons},
Nicola Botta's avatar
Final.    
Nicola Botta committed
1090
1091
  booktitle =	 {ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2006)},
  longbooktitle =	 {Conference record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2006)},
Nicola Botta's avatar
Nicola Botta committed
1092
  pages =	 {206--217},
Nicola Botta's avatar
Final.    
Nicola Botta committed
1093
  publisher =	 {{ACM}},
Nicola Botta's avatar
Nicola Botta committed
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
  title =	 {Fast and Loose Reasoning is Morally Correct},
  year =	 2006,
  doi =		 {10.1145/1111037.1111056},
}

@article{janssonjeuring-dataconv,
  author =	 {Jansson, Patrik and Jeuring, Johan},
  journal =	 {Science of Computer Programming},
  number =	 1,
  pages =	 {35--75},
  title =	 {Polytypic Data Conversion Programs},
  volume =	 43,
  year =	 2002,
  doi =		 {10.1016/S0167-6423(01)00020-X},
}

Nicola Botta's avatar
Final.    
Nicola Botta committed
1110
@inproceedings{peytonjones2001playing,
Nicola Botta's avatar
Nicola Botta committed
1111
1112
1113
1114
1115
1116
1117
1118
  author =	 {Peyton Jones, Simon and Tolmach, Andrew and Hoare,
                  Tony},
  title =	 {Playing by the rules: rewriting as a practical
                  optimisation technique in {GHC}},
  organization = {ACM SIGPLAN},
  booktitle =	 {2001 Haskell Workshop},
  year =	 2001,
  month =	 {September},
Nicola Botta's avatar
Final.    
Nicola Botta committed
1119
  pages =        {203--233},
Nicola Botta's avatar
Nicola Botta committed
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
  abstract =	 {We describe a facility for improving optimization of
                  Haskell programs using rewrite rules. Library
                  authors can use rules to express domain-specific
                  optimizations that the compiler cannot discover for
                  itself. The compiler can also generate rules
                  internally to propagate information obtained from
                  automated analyses. The rewrite mechanism is fully
                  implemented in the released Glasgow Haskell
                  Compiler.  Our system is very simple, but can be
                  effective in optimizing real programs. We describe
                  two practical applications involving short-cut
                  deforestation, for lists and for rose trees, and
                  document substantial performance improvements on a
                  range of programs.},
Nicola Botta's avatar
Final.    
Nicola Botta committed
1134
  url =          {https://www.microsoft.com/en-us/research/publication/playing-by-the-rules-rewriting-as-a-practical-optimisation-technique-in-ghc/},
Nicola Botta's avatar
Nicola Botta committed
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
  edition =	 {2001 Haskell Workshop},
}

@article{DBLP:journals/corr/abs-1904-08562,
  author =	 {Jonathan Sterling and Carlo Angiuli and Daniel
                  Gratzer},
  title =	 {Cubical Syntax for Reflection-Free Extensional
                  Equality},
  journal =	 {CoRR},
  volume =	 {abs/1904.08562},
  year =	 2019,
  url =		 {http://arxiv.org/abs/1904.08562},
  archivePrefix ={arXiv},
  eprint =	 {1904.08562},
  timestamp =	 {Fri, 26 Apr 2019 13:18:53 +0200},
Nicola Botta's avatar
Final.    
Nicola Botta committed
1150
  biburl =       {https://dblp.org/rec/journals/corr/abs-1904-08562.bib},
Nicola Botta's avatar
Nicola Botta committed
1151
1152
1153
1154
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org}
}

Nicola Botta's avatar
Final.    
Nicola Botta committed
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
@misc{hu2021formalizing_preprint,
  title =        {Formalizing of Category Theory in Agda},
  author =       {Jason Z. S. Hu and Jacques Carette},
  year =         2021,
  howpublished = {\url{https://arxiv.org/abs/2005.07059}},
  eprint =       {2005.07059},
  archivePrefix ={arXiv},
  primaryClass = {cs.LO}
}

@inproceedings{hu2021formalizing,
  author = 	 {Hu, Jason Z. S. and Carette, Jacques},
  title = 	 {Formalizing Category Theory in {Agda}},
  year = 	 2021,
  isbn = 	 {9781450382991},
  address = 	 {New York, NY, USA},
  url = 	 {https://doi.org/10.1145/3437992.3439922},
  doi = 	 {10.1145/3437992.3439922},
  abstract = 	 {The generality and pervasiveness of category theory in
	          modern mathematics makes it a frequent and useful target
	          of formalization. It is however quite challenging to formalize,
		  for a variety of reasons. Agda currently (i.e. in 2020) does not
	          have a standard, working formalization of category theory. We
		  document our work on solving this dilemma. The formalization
		  revealed a number of potential design choices, and we present,
		  motivate and explain the ones we picked. In particular, we find
	          that alternative definitions or alternative proofs from those
		  found in standard textbooks can be advantageous, as well as "fit"
		  Agda's type theory more smoothly. Some definitions regarded as
		  equivalent in standard textbooks turn out to make different
		  "universe level" assumptions, with some being more polymorphic
		  than others. We also pay close attention to engineering issues
		  so that the library integrates well with Agda's own standard
		  library, as well as being compatible with as many of supported
		  type theories in Agda as possible.},
  longbooktitle =    {Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs},
  booktitle =    {ACM SIGPLAN Conference on Certified Programs and Proofs},
  pages =        {327--342},
  numpages =     16,
  keywords =     {formal mathematics, Agda, category theory},
  location =     {Virtual, Denmark},
  series =       {CPP 2021}
Nicola Botta's avatar
Nicola Botta committed
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
}

@article{Carette_2014,
  title =	 {Realms: A Structure for Consolidating Knowledge
                  about Mathematical Theories},
  ISBN =	 9783319084343,
  ISSN =	 {1611-3349},
  url =		 {http://dx.doi.org/10.1007/978-3-319-08434-3_19},
  DOI =		 {10.1007/978-3-319-08434-3_19},
  journal =	 {Intelligent Computer Mathematics},
Nicola Botta's avatar
Final.    
Nicola Botta committed
1207
  publisher =	 {Springer},
Nicola Botta's avatar
Nicola Botta committed
1208
1209
1210
1211
1212
1213
  author =	 {Carette, Jacques and Farmer, William M. and
                  Kohlhase, Michael},
  year =	 2014,
  pages =	 {252--266}
}

Nicola Botta's avatar
Final.    
Nicola Botta committed
1214
1215
1216
1217
1218
1219
@phdthesis{vonGlehn_2015,
  author =       {Tamara von Glehn},
  school =       {University of Cambridge},
  howpublished = {https://doi.org/10.17863/CAM.16245},
  title =        {Polynomials and models of type theory},
  year =         {2015}
Nicola Botta's avatar
Nicola Botta committed
1220
1221
1222
}

@inproceedings{10.1145/3018610.3018620,
Nicola Botta's avatar
Final.    
Nicola Botta committed
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
  author =       {Boulier, Simon and P\'{e}drot, Pierre-Marie and Tabareau, Nicolas},
  title =        {The next 700 Syntactical Models of Type Theory},
  year =         {2017},
  isbn =         {9781450347051},
  publisher =    {ACM},
  address =      {New York, NY, USA},
  url =          {https://doi.org/10.1145/3018610.3018620},
  doi =          {10.1145/3018610.3018620},
  booktitle =    {ACM SIGPLAN Conference on Certified Programs and Proofs},
  longbooktitle =    {Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs},
  pages =        {182--194},
  numpages =     {13},
  keywords =     {Program translation, Dependent type theory},
  location =     {Paris, France},
  series =       {CPP 2017}
}

@misc{streicher1993investigations,
  title =        {Investigations into intensional type theory},
  author =       {Streicher, Thomas},
  howpublished = {Habilitiation Thesis, Ludwig-Maximilians-Universit{\"a}t M{\"u}nchen},
  year =         {1993}
Nicola Botta's avatar
Nicola Botta committed
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
}

@article{mcbride2008applicative,
  author =	 {McBride, Conor and Paterson, Ross},
  title =	 {Applicative Programming with Effects},
  year =	 2008,
  issue_date =	 {January 2008},
  publisher =	 {Cambridge University Press},
  volume =	 18,
  number =	 1,
  issn =	 {0956-7968},
  url =		 {https://doi.org/10.1017/S0956796807006326},
  doi =		 {10.1017/S0956796807006326},
  abstract =	 {In this article, we introduce Applicative functors –
                  an abstract characterisation of an applicative style
                  of effectful programming, weaker than Monads and
                  hence more widespread. Indeed, it is the ubiquity of
                  this programming pattern that drew us to the
                  abstraction. We retrace our steps in this article,
                  introducing the applicative pattern by diverse
                  examples, then abstracting it to define the
                  Applicative type class and introducing a bracket
                  notation that interprets the normal application
                  syntax in the idiom of an Applicative
                  functor. Furthermore, we develop the properties of
                  applicative functors and the generic operations they
                  support. We close by identifying the categorical
                  structure of applicative functors and examining
                  their relationship both with Monads and with Arrow.},
Nicola Botta's avatar
Final.    
Nicola Botta committed
1274
  journal =	 {Journal of Functional Programming},
Nicola Botta's avatar
Nicola Botta committed
1275
  month =	 jan,
Nicola Botta's avatar
Final.    
Nicola Botta committed
1276
  pages =	 {1--13},
Nicola Botta's avatar
Nicola Botta committed
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
  numpages =	 13
}

@inproceedings{DBLP:journals/corr/abs-1202-2919,
  author =	 {Mauro Jaskelioff and Ondrej Rypacek},
  editor =	 {James Chapman and Paul Blain Levy},
  title =	 {An Investigation of the Laws of Traversals},
  booktitle =	 {Proceedings Fourth Workshop on Mathematically
                  Structured Functional Programming, MSFP@ETAPS 2012,
                  Tallinn, Estonia, 25 March 2012},
  series =	 {{EPTCS}},
  volume =	 76,
  pages =	 {40--49},
  year =	 2012,
  url =		 {https://doi.org/10.4204/EPTCS.76.5},
  doi =		 {10.4204/EPTCS.76.5},
  timestamp =	 {Fri, 27 Dec 2019 21:15:10 +0100},
Nicola Botta's avatar
Final.    
Nicola Botta committed
1294
  biburl =       {https://dblp.org/rec/journals/corr/abs-1202-2919.bib},
Nicola Botta's avatar
Nicola Botta committed
1295
1296
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org}
1297
}