@phdthesis(abel:PhD,
 author       = {Andreas Abel},
 year         = {2006},
 title        = {A Polymorphic Lambda-Calculus with Sized Higher-Order Types},
 school       = {Ludwig-Maximilians-Universit\"at M\"unchen},
 url          = {http://www2.tcs.ifi.lmu.de/~ abel/publications.html},
)
@inproceedings(Abel:CALCO2016,
 author       = {Andreas Abel},
 year         = {2016},
 title        = {Compositional Coinduction with Sized Types},
 editor       = {Ichiro Hasuo},
 booktitle    = {{Coalgebraic Methods in Computer Science}},
 publisher    = {Springer},
 pages        = {5--10},
 url          = {http://dx.doi.org/10.1007/978-3-319-40370-0_2},
)
@unpublished(ooAgda:Library,
 author       = {Andreas Abel and Stephan Adelsberger and Anton Setzer},
 year         = {2016},
 title        = {{ooAgda. Agda library}},
 url          = {https://github.com/agda/ooAgda},
)
@article(abelAdeslberger:Setzer:InteractiveProgrammingAgda,
 author       = {Andreas Abel and Stephan Adelsberger and Anton Setzer},
 year         = {2017},
 title        = {Interactive programming in {A}gda -- Objects and graphical user interfaces},
 journal      = {Journal of Functional Programming},
 volume       = {27},
 doi          = {10.1017/S0956796816000319},
)
@inproceedings(AbelPientkaThibodeauSetzer:POPL:2013,
 author       = {Andreas Abel and Brigitte Pientka and David Thibodeau and Anton Setzer},
 year         = {2013},
 title        = {Copatterns: {P}rogramming infinite structures by observations},
 editor       = {Roberto Giacobazzi and Radhia Cousot},
 booktitle    = {Proceedings of POPL'13},
 publisher    = {ACM},
 pages        = {27--38},
 doi          = {10.1145/2429069.2429075},
)
@unpublished(literalAgda,
 author       = {{Agda Community}},
 year         = {2017},
 title        = {{Literal Agda}},
 url          = {http://agda.readthedocs.io/en/latest/tools/literate-programming.html},
)
@inproceedings(brookes1984improved,
 author       = {Stephen D Brookes and AW Roscoe},
 year         = {1984},
 title        = {An improved failures model for communicating processes},
 booktitle    = {International Conference on Concurrency},
 organization = {Springer},
 pages        = {281--305},
 doi          = {10.1007/3-540-15670-4_14},
 url          = {https://link.springer.com/chapter/10.1007/3-540-15670-4_14},
)
@inproceedings(brown2008communicating,
 author       = {Neil C. C. Brown},
 year         = {2008},
 title        = {Communicating {H}askell Processes: Composable Explicit Concurrency using Monads},
 booktitle    = {The thirty-first Communicating Process Architectures Conference, {CPA} 2008},
 pages        = {67--83},
 doi          = {10.3233/978-1-58603-907-3-67},
)
@inproceedings(dybjer:InductiveSetsAndFamilies:huet1991logical:officialproceedings,
 author       = {Peter Dybjer},
 year         = {1991},
 title        = {Inductive sets and families in {M}artin-{L}{\"o}f's type theory and their set-theoretic semantics},
 editor       = {G{\'e}rard Huet and Gordon Plotkin},
 booktitle    = {Logical Frameworks},
 publisher    = {Cambridge University Press},
 pages        = {280 -- 306},
 doi          = {10.1017/CBO9780511569807.012},
)
@unpublished(dybjer:universesGeneralNotionInductiveRecursive,
 author       = {Peter Dybjer},
 year         = {1992},
 title        = {Universes and a General Notion of Simultaneous Inductive-Recursive Definition in Type Theory},
 url          = {http://www.lfcs.inf.ed.ac.uk/research/types-bra/proc/proc92.ps.gz},
 note         = {In Bengt Nordstr{\"o}m, Kent Petersson \& Gordon Plotkin, editors : Proceedings of the 1992 workshop on types for proofs and programs, B{\r a}stad, pp. 106 -- 114},
)
@article(dybjerjslinductionrecursion,
 author       = {Peter Dybjer},
 year         = {2000},
 title        = {A general formulation of simultaneous inductive-recursive definitions in type theory},
 journal      = {Journal of Symbolic Logic},
 volume       = {65},
 number       = {2},
 pages        = {525 -- 549},
 doi          = {10.2307/2586554},
)
@article(dybjersetzer:2003:indrekjour,
 author       = {Peter Dybjer and Anton Setzer},
 year         = {2003},
 title        = {Induction-Recursion and Initial Algebras},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {124},
 pages        = {1 -- 47},
 doi          = {10.1016/S0168-0072(02)00096-9},
)
@unpublished(ERTMS:webpage,
 author       = {{ERTMS}},
 year         = {2013},
 title        = {{The European Rail Traffic Mangement System}},
 url          = {http://www.ertms.net/},
)
@unpublished(hancocksetzer:electronicproceedings,
 author       = {P. Hancock and A. Setzer},
 year         = {1999},
 title        = {The {IO} monad in dependent type theory},
 url          = {http://www.md.chalmers.se/Cs/Research/Semantics /APPSEM/dtp99.html},
 note         = {In: Electronic proceedings of the workshop on dependent types in programming, {G}{\"o}teborg, 27-28 March 1999, pp. 1 -- 13.},
)
@inproceedings(hancockSetzer:InteractivePrograms:CSL2000,
 author       = {Peter Hancock and Anton Setzer},
 year         = {2000},
 title        = {Interactive programs in dependent type theory},
 editor       = {P. Clote and H. Schwichtenberg},
 booktitle    = {Computer Science Logic},
 series       = {LNCS, Vol. 1862},
 pages        = {317 -- 331},
 doi          = {10.1007/3-540-44622-2_21},
)
@unpublished(hancocksetzer:pontedelima:2000,
 author       = {Peter Hancock and Anton Setzer},
 year         = {2000},
 title        = {Specifying interactions with dependent types},
 url          = {http://www-sop.inria.fr/oasis/DTP00/Proceedings/proceedings.html},
 note         = {In: Workshop on subtyping and dependent types in programming, Portugal,7 July 2000, electronic proceedings, pp. 1 -- 13.},
)
@article(hoare1978communicating,
 author       = {C. A. R. Hoare},
 year         = {1978},
 title        = {Communicating Sequential Processes},
 journal      = {Commun. ACM},
 volume       = {21},
 number       = {8},
 pages        = {666--677},
 doi          = {10.1145/359576.359585},
)
@unpublished(basharIgriedAntonSetzer:CSP-Agda,
 author       = {Bashar Igried and Anton Setzer},
 year         = {2016},
 title        = {{CSP-Agda. Agda-library}},
 url          = {https://github.com/csetzer/cspagdaPublic},
 note         = {\unhbox\voidb@x \hbox{}},
)
@inproceedings(Igried:2016:PMC:2976022.2976032,
 author       = {Bashar Igried and Anton Setzer},
 year         = {2016},
 title        = {Programming with Monadic CSP-style Processes in Dependent Type Theory},
 booktitle    = {Proceedings of the 1st International Workshop on Type-Driven Development},
 series       = {TyDe 2016},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {28--38},
 doi          = {10.1145/2976022.2976032},
)
@inproceedings(isobe2005generic,
 author       = {Yoshinao Isobe and Markus Roggenbach},
 year         = {2005},
 title        = {A generic theorem prover of CSP refinement},
 booktitle    = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
 organization = {Springer},
 pages        = {108--123},
 doi          = {10.1007/978-3-540-31980-1_8},
 url          = {https://link.springer.com/chapter/10.1007/978-3-540-31980-1_8},
)
@phdthesis(kanso:PhdThesis:2013,
 author       = {Karim Kanso},
 year         = {2012},
 title        = {Agda as a Platform for the Development of Verified Railway Interlocking Systems},
 school       = {Dept.~ of Computer Science},
 address      = {Swansea University, Swansea, UK},
 url          = {http://www.swan.ac.uk/csetzer/articlesFromOthers/index.html},
)
@article(MSC:9412594,
 author       = {Karim Kanso and Anton Setzer},
 year         = {2014},
 title        = {A light-weight integration of automated and interactive theorem proving},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {FirstView},
 pages        = {1--25},
 doi          = {10.1017/S0960129514000140},
 url          = {http://journals.cambridge.org/article_S0960129514000140},
)
@book(martin1984intuitionistic,
 author       = {Martin-L{\"o}f, Per},
 year         = {1984},
 title        = {Intuitionistic type theory},
 publisher    = {Bibliopolis},
 address      = {Naples},
)
@article(moggi:IOMonad,
 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},
 url          = {http://www.sciencedirect.com/science/article/pii/0890540191900524},
)
@article(paulson1986natural,
 author       = {Lawrence C Paulson},
 year         = {1986},
 title        = {Natural deduction as higher-order resolution},
 journal      = {The Journal of Logic Programming},
 volume       = {3},
 number       = {3},
 pages        = {237--258},
 doi          = {10.1016/0743-1066(86)90015-4},
)
@techreport(paulson1988preliminary,
 author       = {Lawrence C Paulson},
 year         = {1988},
 title        = {A preliminary users manual for Isabelle},
 type         = {Technical Report},
 institution  = {University of Cambridge, Computer Laboratory},
)
@inproceedings(PeytonJones:1993:IFP:158511.158524,
 author       = {Peyton Jones, Simon L. and Philip Wadler},
 year         = {1993},
 title        = {Imperative Functional Programming},
 booktitle    = {Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 series       = {POPL '93},
 publisher    = {ACM},
 address      = {New York, USA},
 pages        = {71--84},
 doi          = {10.1145/158511.158524},
)
@book(roscoe1998theory,
 author       = {A. W. Roscoe},
 year         = {1997},
 title        = {The Theory and Practice of Concurrency},
 publisher    = {Prentice Hall},
)
@book(roscoe2010understanding,
 author       = {Andrew William Roscoe},
 year         = {2010},
 title        = {Understanding concurrent systems},
 publisher    = {Springer Science \& Business Media},
 doi          = {10.1007/978-1-84882-258-0},
)
@book(schneider2000concurrent,
 author       = {Steve Schneider},
 year         = {1999},
 title        = {Concurrent and Real Time Systems: The {CSP} Approach},
 edition      = {1st},
 publisher    = {John Wiley},
)
@unpublished(setzer:objectorientedprogrammingDepTypeTheory:Tfp:2006,
 author       = {Anton Setzer},
 year         = {2006},
 title        = {Object-oriented programming in dependent type theory},
 url          = {http://www.cs.nott.ac.uk/~ nhn/TFP2006/TFP2006-Programme.html},
 note         = {In: Proceedings of TFP 2006, pp. 1 - 16.},
)
@incollection(setzerAbelPientkaThibodeau:UnnestingCopatterns:RTALCA2014,
 author       = {Anton Setzer and Andreas Abel and Brigitte Pientka and David Thibodeau},
 year         = {2014},
 title        = {Unnesting of Copatterns},
 editor       = {Gilles Dowek},
 booktitle    = {Rewriting and Typed Lambda Calculi},
 series       = {LNCS},
 volume       = {8560},
 publisher    = {Springer},
 pages        = {31--45},
 doi          = {10.1007/978-3-319-08918-8_3},
)
@inproceedings(tej1997corrected,
 author       = {Haykal Tej and Burkhart Wolff},
 year         = {1997},
 title        = {A corrected failure-divergence model for CSP in Isabelle/HOL},
 booktitle    = {International Symposium of Formal Methods Europe},
 organization = {Springer},
 pages        = {318--337},
 doi          = {10.1007/3-540-63533-5_17},
 url          = {https://link.springer.com/chapter/10.1007/3-540-63533-5_17?LI=true},
)
@inproceedings(Wadler:ComprehendingMonads:1990,
 author       = {Philip Wadler},
 year         = {1990},
 title        = {Comprehending Monads},
 booktitle    = {Proceedings of the 1990 ACM Conference on LISP and Functional Programming},
 series       = {LFP '90},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {61--78},
 doi          = {10.1145/91556.91592},
)
@inproceedings(Wadler:MOnadsFunctionalProgramming:1995,
 author       = {Philip Wadler},
 year         = {1995},
 title        = {Monads for functional programming},
 editor       = {Johan Jeuring and Erik Meijer},
 booktitle    = {Advanced Functional Programming: First International Spring School on Advanced Functional Programming Techniques B{\r a}stad, Sweden, May 24--30, 1995 Tutorial Text},
 publisher    = {Springer},
 pages        = {24--52},
 doi          = {10.1007/3-540-59451-5_2},
)