@article(Allais:2018:TSS:3243631.3236785,
 author       = {Guillaume Allais and Robert Atkey and James Chapman and Conor McBride and James McKinna},
 year         = {2018},
 title        = {A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs},
 journal      = {Proc. ACM Program. Lang.},
 volume       = {2},
 number       = {ICFP},
 pages        = {90:1--90:30},
 doi          = {10.1145/3236785},
)
@inproceedings(DBLP:conf/ctcs/AltenkirchHS95,
 author       = {Thorsten Altenkirch and Martin Hofmann and Thomas Streicher},
 year         = {1995},
 title        = {Categorical Reconstruction of a Reduction Free Normalization Proof},
 editor       = {David H. Pitt and David E. Rydeheard and Peter T. Johnstone},
 booktitle    = {Category Theory and Computer Science, 6th International Conference, {CTCS} '95, Cambridge, UK, August 7-11, 1995, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {953},
 publisher    = {Springer},
 pages        = {182--199},
 doi          = {10.1007/3-540-60164-3\_27},
)
@article(Atkey2009pnc,
 author       = {Robert Atkey},
 year         = {2009},
 title        = {Parameterised notions of computation},
 journal      = {Journal of Functional Programming},
 volume       = {19},
 number       = {3-4},
 pages        = {335--376},
 doi          = {10.1017/S095679680900728X},
)
@inproceedings(Balzer2015osp,
 author       = {Stephanie Balzer and Frank Pfenning},
 year         = {2015},
 title        = {Objects as session-typed processes},
 editor       = {Elisa Gonzalez Boix and Philipp Haller and Alessandro Ricci and Carlos Varela},
 booktitle    = {Proceedings of the 5th International Workshop on Programming Based on Actors, Agents, and Decentralized Control, AGERE! 2015, Pittsburgh, PA, USA, October 26, 2015},
 publisher    = {{ACM}},
 pages        = {13--24},
 doi          = {10.1145/2824815.2824817},
)
@inproceedings(DBLP:conf/concur/BocchiHTY10,
 author       = {Laura Bocchi and Kohei Honda and Emilio Tuosto and Nobuko Yoshida},
 year         = {2010},
 title        = {A Theory of Design-by-Contract for Distributed Multiparty Interactions},
 editor       = {Paul Gastin and Fran{\c{c}}ois Laroussinie},
 booktitle    = {{CONCUR} 2010 - Concurrency Theory, 21th International Conference, {CONCUR} 2010, Paris, France, August 31-September 3, 2010. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {6269},
 publisher    = {Springer},
 pages        = {162--176},
 doi          = {10.1007/978-3-642-15375-4\_12},
)
@inproceedings(Borgstrom2011vsp,
 author       = {Johannes Borgstr{\"{o}}m and Juan Chen and Nikhil Swamy},
 year         = {2011},
 title        = {Verifying stateful programs with substructural state and hoare types},
 editor       = {Ranjit Jhala and Wouter Swierstra},
 booktitle    = {Proceedings of the 5th {ACM} Workshop Programming Languages meets Program Verification, {PLPV} 2011, Austin, TX, USA, January 29, 2011},
 publisher    = {{ACM}},
 pages        = {15--26},
 doi          = {10.1145/1929529.1929532},
)
@article(Brady2013igp,
 author       = {Edwin Brady},
 year         = {2013},
 title        = {Idris, a general-purpose dependently typed programming language: Design and implementation},
 journal      = {J. Funct. Program.},
 volume       = {23},
 number       = {5},
 pages        = {552--593},
 doi          = {10.1017/S095679681300018X},
)
@incollection(Brady2014rda,
 author       = {Edwin Brady},
 year         = {2014},
 title        = {Resource-Dependent Algebraic Effects},
 editor       = {Jurriaan Hage and Jay McCarthy},
 booktitle    = {Trends in Functional Programming - 15th International Symposium, {TFP} 2014, Soesterberg, The Netherlands, May 26-28, 2014. Revised Selected Papers},
 series       = {Lecture Notes in Computer Science},
 volume       = {8843},
 publisher    = {Springer},
 pages        = {18--33},
 doi          = {10.1007/978-3-319-14675-1\_2},
)
@unpublished(Brady2016sms,
 author       = {Edwin Brady},
 year         = {2016},
 title        = {{State Machines All The Way Down: An Architecture for Dependently Typed Applications}},
 url          = {https://eb.host.cs.st-andrews.ac.uk/drafts/states-all-the-way.pdf},
 note         = {Unpublished Draft.},
)
@book(Brady2016tdd,
 author       = {Edwin Brady},
 year         = {2016},
 title        = {{Type-Driven Devlopment with Idris}},
 edition      = {1st},
 publisher    = {Manning},
 url          = {https://www.manning.com/books/type-driven-development-with-idris},
)
@article(DBLP:journals/aghcs/Brady17,
 author       = {Edwin Brady},
 year         = {2017},
 title        = {Type-driven Development of Concurrent Communicating Systems},
 journal      = {Computer Science {(AGH)}},
 volume       = {18},
 number       = {3},
 doi          = {10.7494/csci.2017.18.3.1413},
)
@article(DBLP:journals/fuin/BradyH10,
 author       = {Edwin Brady and Kevin Hammond},
 year         = {2010},
 title        = {Correct-by-Construction Concurrency: Using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols},
 journal      = {Fundam. Inform.},
 volume       = {102},
 number       = {2},
 pages        = {145--176},
 doi          = {10.3233/FI-2010-303},
)
@inproceedings(Brady2012rsp,
 author       = {Edwin Brady and Kevin Hammond},
 year         = {2012},
 title        = {Resource-Safe Systems Programming with Embedded Domain Specific Languages},
 editor       = {Claudio V. Russo and Neng{-}Fa Zhou},
 booktitle    = {Practical Aspects of Declarative Languages - 14th International Symposium, {PADL} 2012, Philadelphia, PA, USA, January 23-24, 2012. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {7149},
 publisher    = {Springer},
 pages        = {242--257},
 doi          = {10.1007/978-3-642-27694-1\_18},
)
@article(Castro:2019:DPU:3302515.3290342,
 author       = {David Castro and Raymond Hu and Sung-Shik Jongmans and Nicholas Ng and Nobuko Yoshida},
 year         = {2019},
 title        = {Distributed Programming Using Role-parametric Session Types in Go: Statically-typed Endpoint APIs for Dynamically-instantiated Communication Structures},
 journal      = {Proc. ACM Program. Lang.},
 volume       = {3},
 number       = {POPL},
 pages        = {29:1--29:30},
 doi          = {10.1145/3290342},
)
@phdthesis(Chapman2009phdthesis,
 author       = {James Maitland Chapman},
 year         = {2009},
 title        = {Type checking and normalisation},
 school       = {School of Computer Science, University of Nottingham},
 url          = {http://eprints.nottingham.ac.uk/10824/},
)
@article(Fowler:2019:EAS:3302515.3290341,
 author       = {Simon Fowler and Sam Lindley and J. Garrett Morris and S\'{a}ra Decova},
 year         = {2019},
 title        = {Exceptional Asynchronous Session Types: Session Types Without Tiers},
 journal      = {Proc. ACM Program. Lang.},
 volume       = {3},
 number       = {POPL},
 pages        = {28:1--28:29},
 doi          = {10.1145/3290341},
)
@inproceedings(DBLP:conf/pldi/FreemanP91,
 author       = {Timothy S. Freeman and Frank Pfenning},
 year         = {1991},
 title        = {Refinement Types for {ML}},
 editor       = {David S. Wise},
 booktitle    = {Proceedings of the {ACM} SIGPLAN'91 Conference on Programming Language Design and Implementation (PLDI), Toronto, Ontario, Canada, June 26-28, 1991},
 publisher    = {{ACM}},
 pages        = {268--277},
 doi          = {10.1145/113445.113468},
)
@article(gordon2003authenticity,
 author       = {Andrew D. Gordon and Alan Jeffrey},
 year         = {2003},
 title        = {Authenticity by Typing for Security Protocols},
 journal      = {Journal of Computer Security},
 volume       = {11},
 number       = {4},
 pages        = {451--520},
 doi          = {10.3233/JCS-2003-11402},
 url          = {http://content.iospress.com/articles/journal-of-computer-security/jcs189},
)
@misc(Guenot2015,
 author       = {Nicolas Guenot and Daniel Gustafsson and Nicola Pouillard},
 year         = {2015},
 title        = {Dependent Communication in Type Theory},
 url          = {https://nicolaspouillard.fr/publis/ptt1.pdf},
)
@article(DBLP:journals/jacm/HondaYC16,
 author       = {Kohei Honda and Nobuko Yoshida and Marco Carbone},
 year         = {2016},
 title        = {Multiparty Asynchronous Session Types},
 journal      = {J. {ACM}},
 volume       = {63},
 number       = {1},
 pages        = {9:1--9:67},
 doi          = {10.1145/2827695},
)
@inproceedings(DBLP:conf/fase/HuY17,
 author       = {Raymond Hu and Nobuko Yoshida},
 year         = {2017},
 title        = {Explicit Connection Actions in Multiparty Session Types},
 editor       = {Marieke Huisman and Julia Rubin},
 booktitle    = {Fundamental Approaches to Software Engineering - 20th International Conference, {FASE} 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {10202},
 publisher    = {Springer},
 pages        = {116--133},
 doi          = {10.1007/978-3-662-54494-5\_7},
)
@inproceedings(session-rust,
 author       = {Thomas Bracht Laumann Jespersen and Philip Munksgaard and Ken Friis Larsen},
 year         = {2015},
 title        = {Session Types for Rust},
 booktitle    = {Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming},
 series       = {WGP 2015},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {13--22},
 doi          = {10.1145/2808098.2808100},
)
@inproceedings(DBLP:conf/uss/Kaloper-Mersinjak15,
 author       = {Kaloper{-}Mersinjak, David and Hannes Mehnert and Anil Madhavapeddy and Peter Sewell},
 year         = {2015},
 title        = {Not-Quite-So-Broken {TLS:} Lessons in Re-Engineering a Security Protocol Specification and Implementation},
 editor       = {Jaeyeon Jung and Thorsten Holz},
 booktitle    = {24th {USENIX} Security Symposium, {USENIX} Security 15, Washington, D.C., USA, August 12-14, 2015.},
 publisher    = {{USENIX} Association},
 pages        = {223--238},
 url          = {https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/kaloper-mersinjak},
)
@inproceedings(Kouzapas2016tpm,
 author       = {Dimitrios Kouzapas and Ornela Dardha and Roly Perera and Simon J. Gay},
 year         = {2016},
 title        = {Typechecking Protocols with Mungo and StMungo},
 booktitle    = {Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming},
 series       = {PPDP '16},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {146--159},
 doi          = {10.1145/2967973.2968595},
)
@inproceedings(DBLP:conf/popl/LangeNTY17,
 author       = {Julien Lange and Nicholas Ng and Bernardo Toninho and Nobuko Yoshida},
 year         = {2017},
 title        = {Fencing off go: liveness and safety for channel-based programming},
 editor       = {Giuseppe Castagna and Andrew D. Gordon},
 booktitle    = {Proceedings of the 44th {ACM} {SIGPLAN} Symposium on Principles of Programming Languages, {POPL} 2017, Paris, France, January 18-20, 2017},
 publisher    = {{ACM}},
 pages        = {748--761},
 doi          = {10.1145/3009837},
 url          = {http://dl.acm.org/citation.cfm?id=3009847},
)
@inbook(Lindley2017lfs,
 author       = {Sam Lindley and J Garrett Morris},
 year         = {2017},
 title        = {Behavioural Types: from Theory to Tools},
 chapter      = {Lightweight Functional Session Types},
 publisher    = {River Publishers},
 doi          = {10.13052/rp-9788793519817},
)
@inproceedings(DBLP:conf/cc/NeykovaHYA18,
 author       = {Rumyana Neykova and Raymond Hu and Nobuko Yoshida and Fahd Abdeljallal},
 year         = {2018},
 title        = {A session type provider: compile-time {API} generation of distributed protocols with refinements in F{\#}},
 editor       = {Christophe Dubach and Jingling Xue},
 booktitle    = {Proceedings of the 27th International Conference on Compiler Construction, {CC} 2018, February 24-25, 2018, Vienna, Austria},
 publisher    = {{ACM}},
 pages        = {128--138},
 doi          = {10.1145/3178372.3179495},
)
@inbook(Ng2012Msc,
 author       = {Nicholas Ng and Nobuko Yoshida and Kohei Honda},
 year         = {2012},
 title        = {Multiparty Session C: Safe Parallel Programming with Message Optimisation},
 pages        = {202--218},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 doi          = {10.1007/978-3-642-30561-0_15},
)
@inproceedings(Norell2009agda,
 author       = {Ulf Norell},
 year         = {2009},
 title        = {{Dependently Typed Programming in Agda}},
 booktitle    = {Proceedings of the $4^{th}$ International Workshop on Types in Language Design and Implementation},
 series       = {TLDI '09},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {1--2},
 doi          = {10.1145/1481861.1481862},
)
@article(Orchard2016ess,
 author       = {Dominic Orchard and Nobuko Yoshida},
 year         = {2016},
 title        = {Effects As Sessions, Sessions As Effects},
 journal      = {SIGPLAN Not.},
 volume       = {51},
 number       = {1},
 pages        = {568--581},
 doi          = {10.1145/2914770.2837634},
)
@inproceedings(DBLP:conf/pldi/PetricekGS16,
 author       = {Tomas Petricek and Gustavo Guerra and Don Syme},
 year         = {2016},
 title        = {Types from data: making structured data first-class citizens in F{\#}},
 editor       = {Chandra Krintz and Emery Berger},
 booktitle    = {Proceedings of the 37th {ACM} {SIGPLAN} Conference on Programming Language Design and Implementation, {PLDI} 2016, Santa Barbara, CA, USA, June 13-17, 2016},
 publisher    = {{ACM}},
 pages        = {477--490},
 doi          = {10.1145/2908080.2908115},
)
@misc(rfc347,
 author       = {J. Postel},
 year         = {1972},
 title        = {{Echo process}},
 howpublished = {RFC 347},
 url          = {http://www.ietf.org/rfc/rfc347.txt},
)
@misc(rfc793,
 author       = {J. Postel},
 year         = {1981},
 title        = {{Transmission Control Protocol}},
 howpublished = {RFC 793 (INTERNET STANDARD)},
 url          = {http://www.ietf.org/rfc/rfc793.txt},
 note         = {Updated by RFCs 1122, 3168, 6093, 6528},
)
@misc(rfc862,
 author       = {J. Postel},
 year         = {1983},
 title        = {{Echo Protocol}},
 howpublished = {RFC 862 (INTERNET STANDARD)},
 url          = {http://www.ietf.org/rfc/rfc862.txt},
)
@inproceedings(session-haskell,
 author       = {Riccardo Pucella and Jesse A. Tov},
 year         = {2008},
 title        = {Haskell Session Types with (Almost) No Class},
 booktitle    = {Proceedings of the First ACM SIGPLAN Symposium on Haskell},
 series       = {Haskell '08},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {25--36},
 doi          = {10.1145/1411286.1411290},
)
@techreport(Sackman2008sth,
 author       = {Matthew Sackman and Susan Eisenbach},
 year         = {2008},
 title        = {{Session Types in Haskell: Updating Message Passing for the 21st Century}},
 type         = {Technical Report},
 institution  = {Imperial College London},
 url          = {http://pubs.doc.ic.ac.uk/session-types-in-haskell/},
)
@article(Toninho2016,
 author       = {Bernardo Toninho and Nobuko Yoshida},
 year         = {2016},
 title        = {Certifying data in multiparty session types},
 journal      = {Journal of Logical and Algebraic Methods in Programming},
 doi          = {10.1016/j.jlamp.2016.11.005},
)
@inproceedings(DBLP:conf/fossacs/ToninhoY18,
 author       = {Bernardo Toninho and Nobuko Yoshida},
 year         = {2018},
 title        = {Depending on Session-Typed Processes},
 editor       = {Christel Baier and Ugo Dal Lago},
 booktitle    = {Foundations of Software Science and Computation Structures - 21st International Conference, {FOSSACS} 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {10803},
 publisher    = {Springer},
 pages        = {128--145},
 doi          = {10.1007/978-3-319-89366-2\_7},
)
@inbook(Yoshida2014spl,
 author       = {Nobuko Yoshida and Raymond Hu and Rumyana Neykova and Nicholas Ng},
 year         = {2014},
 title        = {The Scribble Protocol Language},
 pages        = {22--41},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 doi          = {10.1007/978-3-319-05119-2_3},
)