References

  1. Andreas Abel (2006): A Polymorphic Lambda-Calculus with Sized Higher-Order Types. Ludwig-Maximilians-Universität München. Available at http://www2.tcs.ifi.lmu.de/~ abel/publications.html.
  2. Andreas Abel (2016): Compositional Coinduction with Sized Types. In: Ichiro Hasuo: Coalgebraic Methods in Computer Science. Springer, pp. 5–10. Available at http://dx.doi.org/10.1007/978-3-319-40370-0_2.
  3. Andreas Abel, Stephan Adelsberger & Anton Setzer (2016): ooAgda. Agda library. Available at https://github.com/agda/ooAgda.
  4. Andreas Abel, Stephan Adelsberger & Anton Setzer (2017): Interactive programming in Agda – Objects and graphical user interfaces. Journal of Functional Programming 27, doi:10.1017/S0956796816000319.
  5. Andreas Abel, Brigitte Pientka, David Thibodeau & Anton Setzer (2013): Copatterns: Programming infinite structures by observations. In: Roberto Giacobazzi & Radhia Cousot: Proceedings of POPL'13. ACM, pp. 27–38, doi:10.1145/2429069.2429075.
  6. Agda Community (2017): Literal Agda. Available at http://agda.readthedocs.io/en/latest/tools/literate-programming.html.
  7. Stephen D Brookes & AW Roscoe (1984): An improved failures model for communicating processes. In: International Conference on Concurrency. Springer, pp. 281–305, doi:10.1007/3-540-15670-4_14. Available at https://link.springer.com/chapter/10.1007/3-540-15670-4_14.
  8. Neil C. C. Brown (2008): Communicating Haskell Processes: Composable Explicit Concurrency using Monads. In: The thirty-first Communicating Process Architectures Conference, CPA 2008, pp. 67–83, doi:10.3233/978-1-58603-907-3-67.
  9. Peter Dybjer (1991): Inductive sets and families in Martin-Löf's type theory and their set-theoretic semantics. In: Gérard Huet & Gordon Plotkin: Logical Frameworks. Cambridge University Press, pp. 280 – 306, doi:10.1017/CBO9780511569807.012.
  10. Peter Dybjer (1992): Universes and a General Notion of Simultaneous Inductive-Recursive Definition in Type Theory. Available at http://www.lfcs.inf.ed.ac.uk/research/types-bra/proc/proc92.ps.gz. In Bengt Nordström, Kent Petersson & Gordon Plotkin, editors : Proceedings of the 1992 workshop on types for proofs and programs, Båstad, pp. 106 – 114.
  11. Peter Dybjer (2000): A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic 65(2), pp. 525 – 549, doi:10.2307/2586554.
  12. Peter Dybjer & Anton Setzer (2003): Induction-Recursion and Initial Algebras. Annals of Pure and Applied Logic 124, pp. 1 – 47, doi:10.1016/S0168-0072(02)00096-9.
  13. ERTMS (2013): The European Rail Traffic Mangement System. Available at http://www.ertms.net/.
  14. P. Hancock & A. Setzer (1999): The IO monad in dependent type theory. Available at http://www.md.chalmers.se/Cs/Research/Semantics /APPSEM/dtp99.html. In: Electronic proceedings of the workshop on dependent types in programming, Göteborg, 27-28 March 1999, pp. 1 – 13..
  15. Peter Hancock & Anton Setzer (2000): Interactive programs in dependent type theory. In: P. Clote & H. Schwichtenberg: Computer Science Logic, LNCS, Vol. 1862, pp. 317 – 331, doi:10.1007/3-540-44622-2_21.
  16. Peter Hancock & Anton Setzer (2000): Specifying interactions with dependent types. Available at http://www-sop.inria.fr/oasis/DTP00/Proceedings/proceedings.html. In: Workshop on subtyping and dependent types in programming, Portugal,7 July 2000, electronic proceedings, pp. 1 – 13..
  17. C. A. R. Hoare (1978): Communicating Sequential Processes. Commun. ACM 21(8), pp. 666–677, doi:10.1145/359576.359585.
  18. Bashar Igried & Anton Setzer (2016): CSP-Agda. Agda-library. Available at https://github.com/csetzer/cspagdaPublic. \voidb@x.
  19. Bashar Igried & Anton Setzer (2016): Programming with Monadic CSP-style Processes in Dependent Type Theory. In: Proceedings of the 1st International Workshop on Type-Driven Development, TyDe 2016. ACM, New York, NY, USA, pp. 28–38, doi:10.1145/2976022.2976032.
  20. Yoshinao Isobe & Markus Roggenbach (2005): A generic theorem prover of CSP refinement. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, pp. 108–123, doi:10.1007/978-3-540-31980-1_8. Available at https://link.springer.com/chapter/10.1007/978-3-540-31980-1_8.
  21. Karim Kanso (2012): Agda as a Platform for the Development of Verified Railway Interlocking Systems. Dept. of Computer Science, Swansea University, Swansea, UK. Available at http://www.swan.ac.uk/csetzer/articlesFromOthers/index.html.
  22. Karim Kanso & Anton Setzer (2014): A light-weight integration of automated and interactive theorem proving. Mathematical Structures in Computer Science FirstView, pp. 1–25, doi:10.1017/S0960129514000140. Available at http://journals.cambridge.org/article_S0960129514000140.
  23. Per Martin-Löf (1984): Intuitionistic type theory. Bibliopolis, Naples.
  24. Eugenio Moggi (1991): Notions of computation and monads. Information and Computation 93(1), pp. 55 – 92, doi:10.1016/0890-5401(91)90052-4. Available at http://www.sciencedirect.com/science/article/pii/0890540191900524.
  25. Lawrence C Paulson (1986): Natural deduction as higher-order resolution. The Journal of Logic Programming 3(3), pp. 237–258, doi:10.1016/0743-1066(86)90015-4.
  26. Lawrence C Paulson (1988): A preliminary users manual for Isabelle. Technical Report. University of Cambridge, Computer Laboratory.
  27. Simon L. Peyton Jones & Philip Wadler (1993): Imperative Functional Programming. In: Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '93. ACM, New York, USA, pp. 71–84, doi:10.1145/158511.158524.
  28. A. W. Roscoe (1997): The Theory and Practice of Concurrency. Prentice Hall.
  29. Andrew William Roscoe (2010): Understanding concurrent systems. Springer Science & Business Media, doi:10.1007/978-1-84882-258-0.
  30. Steve Schneider (1999): Concurrent and Real Time Systems: The CSP Approach, 1st edition. John Wiley.
  31. Anton Setzer (2006): Object-oriented programming in dependent type theory. Available at http://www.cs.nott.ac.uk/~ nhn/TFP2006/TFP2006-Programme.html. In: Proceedings of TFP 2006, pp. 1 - 16..
  32. Anton Setzer, Andreas Abel, Brigitte Pientka & David Thibodeau (2014): Unnesting of Copatterns. In: Gilles Dowek: Rewriting and Typed Lambda Calculi, LNCS 8560. Springer, pp. 31–45, doi:10.1007/978-3-319-08918-8_3.
  33. Haykal Tej & Burkhart Wolff (1997): A corrected failure-divergence model for CSP in Isabelle/HOL. In: International Symposium of Formal Methods Europe. Springer, pp. 318–337, doi:10.1007/3-540-63533-5_17. Available at https://link.springer.com/chapter/10.1007/3-540-63533-5_17?LI=true.
  34. Philip Wadler (1990): Comprehending Monads. In: Proceedings of the 1990 ACM Conference on LISP and Functional Programming, LFP '90. ACM, New York, NY, USA, pp. 61–78, doi:10.1145/91556.91592.
  35. Philip Wadler (1995): Monads for functional programming. In: Johan Jeuring & Erik Meijer: Advanced Functional Programming: First International Spring School on Advanced Functional Programming Techniques Båstad, Sweden, May 24–30, 1995 Tutorial Text. Springer, pp. 24–52, doi:10.1007/3-540-59451-5_2.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org