@incollection(cspgs, author = {Samson Abramsky}, year = {2010}, title = {From {CSP} to Game Semantics}, booktitle = {Reflections on the Work of C.A.R. Hoare}, publisher = {Springer}, address = {London}, pages = {33--45}, doi = {10.1007/978-1-84882-912-1_2}, ) @inproceedings(gsgr, author = {Samson Abramsky and Kohei Honda and Guy McCusker}, year = {1998}, title = {A Fully Abstract Game Semantics for General References}, booktitle = {Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science}, publisher = {Society Press}, pages = {334--344}, doi = {10.1109/LICS.1998.705669}, ) @article(gsllaj, author = {Samson Abramsky and Radha Jagadeesan}, year = {1994}, title = {Games and full completeness for multiplicative linear logic}, journal = {The Journal of Symbolic Logic}, volume = {59}, number = {2}, pages = {543--574}, doi = {10.2307/2275407}, ) @article(pcfajm, author = {Samson Abramsky and Radha Jagadeesan and Pasquale Malacaria}, year = {2000}, title = {Full Abstraction for {PCF}}, journal = {Information and Computation}, volume = {163}, number = {2}, pages = {409--470}, doi = {10.1006/inco.2000.2930}, ) @inproceedings(domth, author = {Samson Abramsky and Achim Jung}, year = {1994}, title = {Domain Theory}, editor = {S. Abramsky and D. Gabbay and T. S. E. Maibaum}, booktitle = {Handbook of Logic in Computer Science}, publisher = {Oxford University Press}, pages = {1--168}, url = {http://www.cs.ox.ac.uk/files/298/handbook.pdf}, ) @incollection(gsia, author = {Samson Abramsky and Guy McCusker}, year = {1997}, title = {Linearity, Sharing and State: A Fully Abstract Game Semantics for {I}dealized {A}lgol with Active Expressions}, booktitle = {Algol-like Languages}, publisher = {Birkh{\"a}user}, address = {Boston, MA}, pages = {297--329}, doi = {10.1007/978-1-4757-3851-3_10}, ) @inproceedings(gamesem99, author = {Samson Abramsky and Guy McCusker}, year = {1999}, title = {Game semantics}, booktitle = {Computational logic: Proceedings of the 1997 Marktoberdorf Summer School}, publisher = {Springer}, address = {Berlin, Heidelberg}, pages = {1--55}, doi = {10.1007/978-3-642-58622-4_1}, ) @inproceedings(cgames, author = {Samson Abramsky and Paul-Andr\'{e} Melli\`{e}s}, year = {1999}, title = {Concurrent Games and Full Completeness}, booktitle = {Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science}, series = {LICS '99}, publisher = {IEEE Computer Society}, address = {USA}, pages = {431--442}, doi = {10.1109/LICS.1999.782638}, ) @article(adamek95, author = {Ad\IeC{\'a}mek, Ji\IeC{\v r}\IeC{\'\i}}, year = {1995}, title = {Recursive Data Types in Algebraically $\omega$-Complete Categories}, journal = {Information and Computation}, volume = {118}, number = {2}, pages = {181--190}, doi = {10.1006/inco.1995.1061}, ) @article(coalgideal, author = {Ad\IeC{\'a}mek, Ji\IeC{\v r}\IeC{\'\i}}, year = {2002}, title = {Final Coalgebras are Ideal Completions of Initial Algebras}, journal = {Journal of Logic and Computation}, volume = {12}, number = {2}, pages = {217--242}, doi = {10.1093/logcom/12.2.217}, ) @inproceedings(safe, author = {Azevedo de Amorim, Arthur and Nathan Collins and Andr{\'e} DeHon and Delphine Demange and Hri{\c{t}}cu, C{\u{a}}t{\u{a}}lin and David Pichardie and Benjamin C Pierce and Randy Pollack and Andrew Tolmach}, year = {2014}, title = {A verified information-flow architecture}, booktitle = {Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, series = {POPL'14}, publisher = {ACM}, address = {New York, NY, USA}, pages = {165--178}, doi = {10.1145/2535838.2535839}, ) @article(deepspec, author = {Andrew W. Appel and Lennart Beringer and Adam Chlipala and Benjamin C Pierce and Zhong Shao and Stephanie Weirich and Steve Zdancewic}, year = {2017}, title = {Position paper: the science of deep specification}, journal = {Philosophical Transactions of the Royal Society A}, volume = {375}, number = {2104}, pages = {20160331}, doi = {10.1098/rsta.2016.0331}, ) @article(dcpoalg, author = {Ingo Battenfeld}, year = {2013}, title = {Comparing approaches to free dcpo-algebra constructions}, journal = {The Journal of Logic and Algebraic Programming}, volume = {82}, number = {1}, pages = {53--70}, doi = {10.1016/j.jlap.2012.10.001}, ) @misc(bazbl, author = {Gershom Bazerman and Raymond Puzio}, year = {2020}, title = {The Topological and Logical Structure of Concurrency and Dependency via Distributive Lattices}, url = {https://arxiv.org/abs/2004.05688}, ) @article(gsll, author = {Andreas Blass}, year = {1992}, title = {A game semantics for linear logic}, journal = {Annals of Pure and Applied Logic}, volume = {56}, number = {1--3}, pages = {183--220}, doi = {10.1016/0168-0072(92)90073-9}, ) @article(ifcastrat, author = {Nathan Bowler and Paul Blain Levy and Gordon Plotkin}, year = {2018}, title = {Initial Algebras and Final Coalgebras Consisting of Nondeterministic Finite Trace Strategies}, journal = {Electronic Notes in Theoretical Computer Science}, volume = {341}, pages = {23--44}, doi = {10.1016/j.entcs.2018.11.003}, note = {Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIV)}, ) @article(cohgs, author = {Ana C. Calderon and Guy McCusker}, year = {2010}, title = {Understanding Game Semantics Through Coherence Spaces}, journal = {Electronic Notes in Theoretical Computer Science}, volume = {265}, pages = {231--244}, doi = {10.1016/j.entcs.2010.08.014}, note = {Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2010)}, ) @inproceedings(nacgs, author = {Simon Castellan and Pierre Clairambault and Jonathan Hayman and Glynn Winskel}, year = {2018}, title = {Non-angelic concurrent game semantics}, booktitle = {Proceedings of the 21st International Conference on Foundations of Software Science and Computation Structures}, series = {FoSSaCS 2018}, publisher = {Springer}, address = {Cham, Switzerland}, pages = {3--19}, doi = {10.1007/978-3-319-89366-2_1}, ) @article(kami, author = {Joonwon Choi and Muralidaran Vijayaraghavan and Benjamin Sherman and Adam Chlipala and Arvind}, year = {2017}, title = {Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification}, journal = {Proceedings of the ACM on Programming Languages}, volume = {1}, number = {ICFP}, doi = {10.1145/3110268}, ) @article(coalgmon, author = {Neil Ghani and L\IeC{\"u}th, Christoph and {de Marchi}, Federico and John Power}, year = {2001}, title = {Algebras, Coalgebras, Monads and Comonads}, journal = {Electronic Notes in Theoretical Computer Science}, volume = {44}, number = {1}, pages = {128--145}, doi = {10.1016/S1571-0661(04)80905-8}, note = {CMCS 2001, Coalgebraic Methods in Computer Science (a Satellite Event of ETAPS 2001)}, ) @inproceedings(asfgc, author = {Dan R. Ghica and Andrzej S. Murawski}, year = {2004}, title = {Angelic Semantics of Fine-Grained Concurrency}, booktitle = {Proceedings of the 7th International Conference on Foundations of Software Science and Computation Structures}, series = {FoSSaCS 2004}, publisher = {Springer}, address = {Berlin, Heidelberg}, pages = {211--225}, doi = {10.1007/978-3-540-24727-2_16}, ) @inproceedings(gscnd, author = {W. John Gowers and James D. Laird}, year = {2018}, title = {A Fully Abstract Game Semantics for Countable Nondeterminism}, editor = {Dan Ghica and Achim Jung}, booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, volume = {119}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}, address = {Dagstuhl, Germany}, pages = {24:1--24:18}, doi = {10.4230/LIPIcs.CSL.2018.24}, ) @inproceedings(popl15, author = {Ronghui Gu and J{\'e}r{\'e}mie Koenig and Tahina Ramananandro and Zhong Shao and Xiongnan (Newman) Wu and Shu-Chun Weng and Haozhong Zhang and Yu Guo}, year = {2015}, title = {Deep Specifications and Certified Abstraction Layers}, booktitle = {Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, series = {POPL '15}, publisher = {ACM}, address = {New York, NY, USA}, pages = {595--608}, doi = {10.1145/2676726.2676975}, ) @inproceedings(osdi16, author = {Ronghui Gu and Zhong Shao and Hao Chen and Xiongnan Wu and Jieung Kim and Vilhelm Sj\"{o}berg and David Costanzo}, year = {2016}, title = {CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels}, booktitle = {Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation}, series = {OSDI'16}, publisher = {USENIX Association}, address = {Berkeley, CA, USA}, pages = {653--669}, doi = {10.5555/3026877.3026928}, ) @inproceedings(gsfnd, author = {Russell Harmer and Guy McCusker}, year = {1999}, title = {A fully abstract game semantics for finite nondeterminism}, booktitle = {Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science}, series = {LICS '99}, publisher = {IEEE Computer Society}, address = {USA}, pages = {422--430}, doi = {10.1109/LICS.1999.782637}, ) @article(adjtrans, author = {Claudio Hermida and Bart Jacobs}, year = {1998}, title = {Structural Induction and Coinduction in a Fibrational Setting}, journal = {Information and Computation}, volume = {145}, number = {2}, pages = {107--152}, doi = {10.1006/inco.1998.2725}, ) @article(pcfho, author = {J. M. E. Hyland and C.-H. L. Ong}, year = {2000}, title = {On Full Abstraction for {PCF}: {I}, {II}, and {III}}, journal = {Information and Computation}, volume = {163}, number = {2}, pages = {285--408}, doi = {10.1006/inco.2000.2917}, ) @article(effcomb, author = {Martin Hyland and Gordon Plotkin and John Power}, year = {2006}, title = {Combining effects: Sum and tensor}, journal = {Theoretical Computer Science}, volume = {357}, number = {1}, pages = {70--99}, doi = {10.1016/j.tcs.2006.03.013}, note = {Clifford Lectures and the Mathematical Foundations of Programming Semantics}, ) @misc(hyvernat-ext, author = {Pierre Hyvernat}, year = {2013}, title = {A linear category of polynomial functors (extensional part)}, url = {https://arxiv.org/abs/1403.0833}, ) @article(hyvernat-diag, author = {Pierre Hyvernat}, year = {2014}, title = {A linear category of polynomial diagrams}, journal = {Mathematical Structures in Computer Science}, volume = {24}, number = {1}, doi = {10.1017/S0960129512001016}, ) @inproceedings(sel4, author = {Gerwin Klein and Kevin Elphinstone and Gernot Heiser and June Andronick and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish}, year = {2009}, title = {{seL4}: formal verification of an {OS} kernel}, booktitle = {Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles}, series = {SOSP '09}, publisher = {ACM}, address = {New York, NY, USA}, pages = {207--220}, doi = {10.1145/1629575.1629596}, ) @inproceedings(rbgs-cal, author = {J\'{e}r\'{e}mie Koenig and Zhong Shao}, year = {2020}, title = {Refinement-Based Game Semantics for Certified Abstraction Layers}, booktitle = {Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science}, series = {LICS '20}, publisher = {ACM}, address = {New York, NY, USA}, pages = {633\IeC{\textendash}647}, doi = {10.1145/3373718.3394799}, ) @inproceedings(itrees, author = {Nicolas Koh and Yao Li and Yishuai Li and Li-yao Xia and Lennart Beringer and Wolf Honor{\'e} and William Mansky and Benjamin C Pierce and Steve Zdancewic}, year = {2019}, title = {From C to interaction trees: specifying, verifying, and testing a networked server}, booktitle = {Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs}, organization = {ACM}, pages = {234--248}, doi = {10.1145/3293880.3294106}, ) @inproceedings(koind, author = {Dexter Kozen}, year = {2011}, title = {Realization of Coinductive Types}, editor = {Michael Mislove and Jo{\"e}l Ouaknine}, booktitle = {Proceedings of the 27th Conference on Mathematical Foundations of Programming Semantics}, series = {MFPS XXVII}, publisher = {Elsevier}, address = {Pittsburgh, PA}, pages = {148--155}, doi = {10.1016/j.entcs.2011.09.024}, ) @inproceedings(cakeml, author = {Ramana Kumar and Magnus Myreen and Michael Norrish and Scott Owens}, year = {2014}, title = {{CakeML}: A Verified Implementation of {ML}}, booktitle = {Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, series = {POPL'14}, publisher = {ACM}, address = {New York, NY, USA}, pages = {179--191}, doi = {10.1145/2578855.2535841}, ) @inproceedings(gscontrol, author = {James Laird}, year = {1997}, title = {Full abstraction for functional languages with control}, booktitle = {Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science}, series = {LICS '97}, publisher = {IEEE Computer Society}, address = {USA}, pages = {58--67}, doi = {10.1109/LICS.1997.614931}, ) @article(compcert, author = {Xavier Leroy}, year = {2009}, title = {Formal Verification of a Realistic Compiler}, journal = {Communications of the ACM}, volume = {52}, number = {7}, pages = {107--115}, doi = {10.1145/1538788.1538814}, ) @inproceedings(tsg, author = {Paul Blain Levy and Sam Staton}, year = {2014}, title = {Transition Systems over Games}, booktitle = {Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)}, series = {CSL-LICS '14}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, doi = {10.1145/2603088.2603150}, ) @inproceedings(agames2, author = {Paul-Andr{\'e} Melli{\`e}s}, year = {2004}, title = {Asynchronous games 2: the true concurrency of innocence}, booktitle = {Proceedings of the 15th International Conference on Concurrency Theory}, series = {CONCUR 2004}, publisher = {Springer}, address = {Berlin, Heidelberg}, pages = {448--465}, doi = {10.1016/j.tcs.2006.01.016}, ) @article(tgames, author = {Paul-Andr{\'e} Melli{\`e}s}, year = {2019}, title = {Categorical combinatorics of scheduling and synchronization in game semantics}, journal = {Proceedings of the ACM on Programming Languages}, volume = {3}, number = {POPL}, pages = {1--30}, doi = {10.1145/3290336}, ) @inproceedings(agames, author = {Paul-Andr{\'e} Melli{\`e}s and Samuel Mimram}, year = {2007}, title = {Asynchronous Games: Innocence Without Alternation}, booktitle = {Proceedings of the 18th International Conference on Concurrency Theory}, series = {CONCUR 2007}, publisher = {Springer}, address = {Berlin, Heidelberg}, pages = {395--411}, doi = {10.1007/978-3-540-74407-8_27}, ) @article(monads, author = {Eugenio Moggi}, year = {1991}, title = {Notions of computation and monads}, journal = {Information and computation}, volume = {93}, number = {1}, pages = {55--92}, doi = {10.1016/0890-5401(91)90052-4}, ) @inproceedings(gseia, author = {Andrzej S. Murawski}, year = {2008}, title = {Reachability Games and Game Semantics: Comparing Nondeterministic Programs}, booktitle = {Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science}, series = {LICS 2008}, publisher = {IEEE Computer Society}, address = {USA}, pages = {353--363}, doi = {10.1109/LICS.2008.24}, ) @inproceedings(effadq, author = {Gordon Plotkin and John Power}, year = {2001}, title = {Adequacy for Algebraic Effects}, booktitle = {Proceedings of the 4th International Conference on Foundations of Software Science and Computation Structures}, series = {FoSSaCS 2001}, publisher = {Springer}, address = {Berlin, Heidelberg}, pages = {1--24}, doi = {10.1007/3-540-45315-6_1}, ) @inproceedings(eff, author = {Gordon Plotkin and Matija Pretnar}, year = {2009}, title = {Handlers of algebraic effects}, booktitle = {Proceedings of the 18th European Symposium on Programming}, series = {ESOP 2009}, publisher = {Springer}, address = {Berlin, Heidelberg}, pages = {80--94}, doi = {10.1007/978-3-642-00590-9_7}, ) @article(shao10, author = {Zhong Shao}, year = {2010}, title = {Certified Software}, journal = {Communications of the {ACM}}, volume = {53}, number = {12}, pages = {56--66}, doi = {10.1145/1859204.1859226}, ) @misc(poly, author = {David I. Spivak}, year = {2020}, title = {Poly: An abundant categorical setting for mode-dependent dynamics}, url = {https://arxiv.org/abs/2005.01894}, ) @article(freemon, author = {V{\v{e}}ra Trnkov{\'a} and Ji{\v{r}}{\'\i} Ad{\'a}mek and V{\'a}clav Koubek and Jan Reiterman}, year = {1975}, title = {Free algebras, input processes and free monads}, journal = {Commentationes Mathematicae Universitatis Carolinae}, volume = {16}, number = {2}, pages = {339--351}, url = {http://hdl.handle.net/10338.dmlcz/105628}, ) @inproceedings(gsndsheaves, author = {Takeshi Tsukada and C.-H. Luke Ong}, year = {2015}, title = {Nondeterminism in game semantics via sheaves}, booktitle = {Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science}, series = {LICS 2015}, publisher = {IEEE Computer Society}, address = {USA}, pages = {220--231}, doi = {10.1109/LICS.2015.30}, ) @inproceedings(vellvm, author = {Jianzhou Zhao and Santosh Nagarakatte and Milo MK Martin and Steve Zdancewic}, year = {2012}, title = {Formalizing the LLVM intermediate representation for verified program transformations}, booktitle = {Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, series = {POPL'12}, publisher = {ACM}, address = {New York, NY, USA}, pages = {427--440}, doi = {10.1145/2103621.2103709}, )