references.bib

@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}
}

@book{Baader1998,
author = {Baader, Franz and Nipkow, Tobias},
title = {Term rewriting and all that},
year = {1998},
isbn = {0521455200},
publisher = {Cambridge University Press},
address = {USA}
}

@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}
}

@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{        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{         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}
}

@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}
}

@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}
}