{{ message }}
Repository navigation
Expand file tree
/
Copy pathreferences.bib
More file actions
486 lines (449 loc) · 19.8 KB
/
Copy pathreferences.bib
File metadata and controls
486 lines (449 loc) · 19.8 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
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
156
157
158
159
160
161
162
163
164
165
166
167
168
169
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
203
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
237
238
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
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
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
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
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
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
@inproceedings{Aceto1999,
author = {Luca Aceto and
Anna Ing{\'{o}}lfsd{\'{o}}ttir},
editor = {Wolfgang Thomas},
title = {Testing Hennessy-Milner Logic with Recursion},
booktitle = {Foundations of Software Science and Computation Structure, Second
International Conference, FoSSaCS'99, Held as Part of the European
Joint Conferences on the Theory and Practice of Software, ETAPS'99,
Amsterdam, The Netherlands, March 22-28, 1999, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1578},
pages = {41--55},
publisher = {Springer},
year = {1999},
url = {https://doi.org/10.1007/3-540-49019-1\_4},
doi = {10.1007/3-540-49019-1\_4},
timestamp = {Tue, 14 May 2019 10:00:55 +0200},
biburl = {https://dblp.org/rec/conf/fossacs/AcetoI99.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{AngluinLaird1988,
author = {Angluin, Dana and Laird, Philip},
title = {Learning from Noisy Examples},
journal = {Machine Learning},
volume = {2},
number = {4},
pages = {343--370},
year = {1988},
doi = {10.1007/BF00116829}
}
@book{Baader1998,
author = {Baader, Franz and Nipkow, Tobias},
title = {Term rewriting and all that},
year = {1998},
isbn = {0521455200},
publisher = {Cambridge University Press},
address = {USA}
}
@book{Blackburn2001,
place={Cambridge},
series={Cambridge Tracts in Theoretical Computer Science},
title={Modal Logic},
publisher={Cambridge University Press},
author={Blackburn, Patrick and Rijke, Maarten de and Venema, Yde},
year={2001},
collection={Cambridge Tracts in Theoretical Computer Science}
}
@misc{Burghardt2018,
title = {Simple {Laws} about {Nonprominent} {Properties} of {Binary} {Relations}},
url = {https://arxiv.org/abs/1806.05036v2},
abstract = {We checked each binary relation on a 5-element set for a given set of properties, including usual ones like asymmetry and less known ones like Euclideanness. Using a poor man's Quine-McCluskey algorithm, we computed prime implicants of non-occurring property combinations, like "not irreflexive, but asymmetric". We considered the non-trivial laws obtained this way, and manually proved them true for binary relations on arbitrary sets, thus contributing to the encyclopedic knowledge about less known properties.},
language = {en},
urldate = {2026-05-19},
journal = {arXiv.org},
author = {Burghardt, Jochen},
month = jun,
year = {2018},
}
@inproceedings{Danielsson2008,
author = {Danielsson, Nils Anders},
title = {Lightweight semiformal time complexity analysis for purely functional data structures},
year = {2008},
isbn = {9781595936899},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/1328438.1328457},
doi = {10.1145/1328438.1328457},
abstract = {Okasaki and others have demonstrated how purely functional data structures that are efficient even in the presence of persistence can be constructed. To achieve good time bounds essential use is often made of laziness. The associated complexity analysis is frequently subtle, requiring careful attention to detail, and hence formalising it is valuable. This paper describes a simple library which can be used to make the analysis of a class of purely functional data structures and algorithms almost fully formal. The basic idea is to use the type system to annotate every function with the time required to compute its result. An annotated monad is used to combine time complexity annotations. The library has been used to analyse some existing data structures, for instance the deque operations of Hinze and Paterson's finger trees.},
booktitle = {Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
pages = {133–144},
numpages = {12},
keywords = {purely functional data structures, lazy evaluation, dependent types, amortised time complexity},
location = {San Francisco, California, USA},
series = {POPL '08}
}
@article{ Barendregt1984,
title={Introduction to Lambda Calculus},
year={1984}
}
@book{ Hopcroft2006,
author = {Hopcroft, John E. and Motwani, Rajeev and Ullman, Jeffrey D.},
title = {Introduction to Automata Theory, Languages, and Computation (3rd Edition)},
year = {2006},
isbn = {0321455363},
publisher = {Addison-Wesley Longman Publishing Co., Inc.},
address = {USA}
}
@misc{ Malkin2024,
author = {Tal Malkin},
title = {{COMS W3261: Computer Science Theory, Handout 3: The Myhill-Nerode Theorem and Implications}},
howpublished = {Columbia University Course Handout},
year = {2024},
month = {September},
url = {https://www.cs.columbia.edu/~tal/3261/fall24/Handouts/3_Myhill_Nerode.pdf}
}
@misc{ WikipediaMyhillNerode2026,
author = {{Wikipedia contributors}},
title = {{Myhill--Nerode theorem}},
howpublished = {Wikipedia, The Free Encyclopedia},
year = {2026},
url = {https://en.wikipedia.org/wiki/Myhill%E2%80%93Nerode_theorem},
note = {[Online; accessed 9-April-2026]}
}
@article{ Chargueraud2012,
title = {The {Locally} {Nameless} {Representation}},
volume = {49},
issn = {1573-0670},
url = {https://doi.org/10.1007/s10817-011-9225-2},
doi = {10.1007/s10817-011-9225-2},
abstract = {This paper provides an introduction to the locally nameless approach to the representation of syntax with variable binding, focusing in particular on the use of this technique in formal proofs. First, we explain the benefits of representing bound variables with de Bruijn indices while retaining names for free variables. Then, we explain how to describe and manipulate syntax in that form, and show how to define and reason about judgments on locally nameless terms.},
language = {en},
number = {3},
urldate = {2025-07-13},
journal = {Journal of Automated Reasoning},
author = {Charguéraud, Arthur},
month = oct,
year = {2012},
keywords = {Binders, C++, Cofinite quantification, Convention Theory, Data Structures, Formal proofs, Functions of a Complex Variable, Lisp, Locally nameless, Metatheory, Syntax},
pages = {363--408},
file = {Full Text PDF:/home/chenson/mount/Zotero/storage/WBJWAZGI/Charguéraud - 2012 - The Locally Nameless Representation.pdf:application/pdf},
}
@article{ FLP1985,
author = {Fischer, Michael J. and Lynch, Nancy A. and Paterson, Michael S.},
title = {Impossibility of Distributed Consensus with One Faulty Process},
year = {1985},
issue_date = {April 1985},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {32},
number = {2},
issn = {0004-5411},
url = {https://doi.org/10.1145/3149.214121},
doi = {10.1145/3149.214121},
journal = {J. ACM},
month = {apr},
pages = {374–382},
numpages = {9}
}
@article{ Girard1987,
title={Linear logic},
author={Girard, Jean-Yves},
journal={Theoretical Computer Science},
volume={50},
number={1},
year={1987},
pages={1--101},
issn={0304-3975},
doi={10.1016/0304-3975(87)90045-4},
url={https://www.sciencedirect.com/science/article/pii/0304397587900454},
abstract={The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality "of course" which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.}
}
@inbook{ Girard1995,
place={Cambridge},
series={London Mathematical Society Lecture Note Series},
title={Linear Logic: its syntax and semantics},
booktitle={Advances in Linear Logic},
publisher={Cambridge University Press},
author={Girard, J.-Y.},
editor={Girard, Jean-Yves and Lafont, Yves and Regnier, LaurentEditors},
year={1995},
pages={1–42},
collection={London Mathematical Society Lecture Note Series}
}
@article{Haussler1992,
author = {Haussler, David},
title = {Decision Theoretic Generalizations of the {PAC} Model for Neural Net and Other Learning Applications},
journal = {Information and Computation},
volume = {100},
number = {1},
pages = {78--150},
year = {1992},
issn = {0890-5401},
doi = {10.1016/0890-5401(92)90010-D}
}
@article{ Hennessy1985,
author = {Matthew Hennessy and
Robin Milner},
title = {Algebraic Laws for Nondeterminism and Concurrency},
journal = {J. {ACM}},
volume = {32},
number = {1},
pages = {137--161},
year = {1985},
url = {https://doi.org/10.1145/2455.2460},
doi = {10.1145/2455.2460},
timestamp = {Tue, 06 Nov 2018 12:51:45 +0100},
biburl = {https://dblp.org/rec/journals/jacm/HennessyM85.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@book{ KatzLindell2020,
author = {Jonathan Katz and
Yehuda Lindell},
title = {Introduction to Modern Cryptography},
edition = {3rd},
publisher = {CRC Press},
year = {2020},
isbn = {9780815354369}
}
@article{ Shamir1979,
author = {Adi Shamir},
title = {How to Share a Secret},
journal = {Communications of the ACM},
volume = {22},
number = {11},
pages = {612--613},
year = {1979},
month = nov,
url = {https://doi.org/10.1145/359168.359176},
doi = {10.1145/359168.359176}
}
@inproceedings{ Kiselyov2015,
author = {Kiselyov, Oleg and Ishii, Hiromi},
title = {Freer Monads, More Extensible Effects},
booktitle = {Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell},
series = {Haskell 2015},
year = {2015},
pages = {94--105},
publisher = {ACM},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/2804302.2804319},
doi = {10.1145/2804302.2804319},
isbn = {978-1-4503-3808-0}
}
@book{ MilewskiDao,
author = {Milewski, Bartosz},
title = {The Dao of Functional Programming},
publisher = {Self-published},
year = {2018},
note = {Available online at \url{https://bartoszmilewski.com}},
}
@book{ Milner80,
author = {Robin Milner},
title = {A Calculus of Communicating Systems},
series = {Lecture Notes in Computer Science},
volume = {92},
publisher = {Springer},
year = {1980},
url = {https://doi.org/10.1007/3-540-10235-3},
doi = {10.1007/3-540-10235-3},
isbn = {3-540-10235-3},
timestamp = {Tue, 14 May 2019 10:00:35 +0200},
biburl = {https://dblp.org/rec/books/sp/Milner80.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@Book{ Montesi2023,
title = {Introduction to {Choreographies}},
author = {Montesi, Fabrizio},
year = {2023},
publisher = {Cambridge University Press},
address = {Cambridge},
url = {https://www.cambridge.org/core/books/introduction-to-choreographies/65D3DA3CFF11AB835452CBC97FAE4830},
urldate = {2023-02-02},
doi = {10.1017/9781108981491},
abstract = {In concurrent and distributed systems, processes can
complete tasks together by playing their parts in a joint
plan. The plan, or protocol, can be written as a
choreography: a formal description of overall behaviour
that processes should collaborate to implement, like
authenticating a user or purchasing an item online.
Formality brings clarity, but not only that: choreographies
can contribute to important safety and liveness properties.
This book is an ideal introduction to theory of
choreographies for students, researchers, and professionals
in computer science and applied mathematics. It covers
languages for writing choreographies, their semantics, and
principles for implementing choreographies correctly. The
text treats the study of choreographies as a discipline in
its own right, following a systematic approach that starts
from simple foundations and proceeds to more advanced
features in incremental steps. Each chapter includes
examples and exercises aimed at helping with understanding
the theory and its relation to practice.},
isbn = {978-1-108-83376-9},
keywords = {choreographic-programming,choreographic-language,choreography,concurrency-theory}
}
@article{ Nipkow2001,
title = {More {Church-Rosser} Proofs (in {Isabelle/HOL})},
author = {Nipkow, Tobias},
journal = {Journal of Automated Reasoning},
volume = {26},
pages = {51--66},
year = {2001},
publisher = {Kluwer Academic Publishers}
}
@Book{ Sangiorgi2011,
location = {Cambridge},
title = {Introduction to Bisimulation and Coinduction},
isbn = {978-1-107-00363-7},
url = {https://www.cambridge.org/core/books/introduction-to-bisimulation-and-coinduction/8B54001CB763BAE9C4BA602C0A341D60},
abstract = {Induction is a pervasive tool in computer science and
mathematics for defining objects and reasoning on them.
Coinduction is the dual of induction and as such it brings
in quite different tools. Today, it is widely used in
computer science, but also in other fields, including
artificial intelligence, cognitive science, mathematics,
modal logics, philosophy and physics. The best known
instance of coinduction is bisimulation, mainly employed to
define and prove equalities among potentially infinite
objects: processes, streams, non-well-founded sets, etc.
This book presents bisimulation and coinduction: the
fundamental concepts and techniques and the duality with
induction. Each chapter contains exercises and selected
solutions, enabling students to connect theory with
practice. A special emphasis is placed on bisimulation as a
behavioural equivalence for processes. Thus the book serves
as an introduction to models for expressing processes (such
as process calculi) and to the associated techniques of
operational and algebraic analysis.},
publisher = {Cambridge University Press},
author = {Sangiorgi, Davide},
urldate = {2025-06-16},
date = {2011},
doi = {10.1017/CBO9780511777110}
}
@incollection{ Thomas1990,
author = {Wolfgang Thomas},
editor = {Jan van Leeuwen},
title = {Automata on Infinite Objects},
booktitle = {Handbook of Theoretical Computer Science, Volume {B:} Formal Models and Semantics},
pages = {133--191},
publisher = {Elsevier and {MIT} Press},
year = {1990}
}
@book{ Cutland1980,
author = {Cutland, Nigel J.},
title = {Computability: An Introduction to Recursive Function Theory},
year = {1980},
publisher = {Cambridge University Press},
address = {Cambridge},
isbn = {978-0-521-29465-2}
}
@article{ ShepherdsonSturgis1963,
author = {Shepherdson, J. C. and Sturgis, H. E.},
title = {Computability of Recursive Functions},
journal = {Journal of the ACM},
volume = {10},
number = {2},
year = {1963},
pages = {217--255},
doi = {10.1145/321160.321170},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA}
}
@inproceedings{Valiant1984,
author = {Valiant, L. G.},
title = {A Theory of the Learnable},
year = {1984},
isbn = {0-89791-133-4},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/800057.808710},
doi = {10.1145/800057.808710},
booktitle = {Proceedings of the Sixteenth Annual ACM Symposium on Theory of Computing},
pages = {436--445},
series = {STOC '84}
}
@article{EHKV1989,
author = {Ehrenfeucht, Andrzej and Haussler, David and Kearns, Michael and Valiant, Leslie},
title = {A General Lower Bound on the Number of Examples Needed for Learning},
journal = {Information and Computation},
volume = {82},
number = {3},
pages = {247--261},
year = {1989},
issn = {0890-5401},
url = {https://doi.org/10.1016/0890-5401(89)90002-3},
doi = {10.1016/0890-5401(89)90002-3},
publisher = {Academic Press}
}
@book{KearnsVazirani1994,
author = {Kearns, Michael J. and Vazirani, Umesh V.},
title = {An Introduction to Computational Learning Theory},
year = {1994},
isbn = {978-0-262-11193-5},
publisher = {MIT Press},
address = {Cambridge, MA, USA}
}
@article{ Volzer2004,
title = {A constructive proof for {FLP}},
author = {V{\"o}lzer, Hagen},
journal = {Information Processing Letters},
volume = {92},
number = {2},
pages = {83--87},
year = {2004},
publisher = {Elsevier},
doi = {10.1016/j.ipl.2004.06.008},
url = {https://doi.org/10.1016/j.ipl.2004.06.008}
}
@incollection{WinskelNielsen1995,
author = {Winskel, Glynn and Nielsen, Mogens},
isbn = {9780198537809},
title = {Models for concurrency},
booktitle = {Handbook of Logic in Computer Science},
publisher = {Oxford University Press},
year = {1995},
month = {05},
doi = {10.1093/oso/9780198537809.003.0001},
url = {https://doi.org/10.1093/oso/9780198537809.003.0001},
eprint = {https://academic.oup.com/book/0/chapter/421962123/chapter-pdf/52352653/isbn-9780198537809-book-part-1.pdf},
}
@inproceedings{Mitchell1977,
author = {Mitchell, Tom M.},
title = {Version Spaces: A Candidate Elimination Approach to Rule Learning},
booktitle = {Proceedings of the 5th International Joint Conference on Artificial Intelligence},
volume = {1},
pages = {305--310},
year = {1977}
}
@article{Mitchell1982,
author = {Mitchell, Tom M.},
title = {Generalization as Search},
journal = {Artificial Intelligence},
volume = {18},
number = {2},
pages = {203--226},
year = {1982},
doi = {10.1016/0004-3702(82)90040-6}
}
@article{Angluin1980,
author = {Angluin, Dana},
title = {Inductive Inference of Formal Languages from Positive Data},
journal = {Information and Control},
volume = {45},
number = {2},
pages = {117--135},
year = {1980},
doi = {10.1016/S0019-9958(80)90285-5}
}
@book{Mitchell1997,
author = {Mitchell, Tom M.},
title = {Machine Learning},
year = {1997},
publisher = {McGraw-Hill},
isbn = {0070428077}
}
@mastersthesis{Calisto2022,
author = {Calisto, Bruna},
title = {Formalization in {Coq} of the {Standardization Theorem} for {$\lambda$}-calculus},
school = {Universidade do Minho},
year = {2022}
}
@book{Sipser2013,
author = {Sipser, Michael},
title = {Introduction to the Theory of Computation},
edition = {3rd},
publisher = {Cengage Learning},
year = {2013}
}
You can’t perform that action at this time.