References

  1. S. Abramsky (1994): Proofs as processes. Theoretical Computer Science 135(1), pp. 5–9, doi:10.1016/0304-3975(94)00103-0.
  2. G. Bellin & PJ Scott (1994): On the π-calculus and linear logic. Theoretical Computer Science 135(1), pp. 11–65, doi:10.1016/0304-3975(94)00104-9.
  3. Y. Bertot, P. Castéran, G. Huet & C. Paulin-Mohring (2004): Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions. Springer-Verlag New York Inc, doi:10.1007/978-3-662-07964-5.
  4. Luís Caires & Frank Pfenning (2010): Session Types as Intuitionistic Linear Propositions. In: Paul Gastin & Francois Laroussinie: CONCUR 2010 - Concurrency Theory, Lecture Notes in Computer Science 6269. Springer Berlin Heidelberg, pp. 222–236, doi:10.1007/978-3-642-15375-4_16.
  5. Luís Caires, Frank Pfenning & Bernardo Toninho (2012): Towards concurrent type theory. In: Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation, TLDI '12. ACM, New York, NY, USA, pp. 1–12, doi:10.1145/2103786.2103788.
  6. Jeremy E. Dawson & Rajeev Goré (2010): Generic Methods for Formalising Sequent Calculi Applied to Provability Logic. In: Christian G. Fermüller & Andrei Voronkov: Logic for Programming, Artificial Intelligence, and Reasoning. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 263–277, doi:10.1007/978-3-642-16242-8_19.
  7. Henry DeYoung, Luís Caires, Frank Pfenning & Bernardo Toninho (2012): Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication. In: Patrick Cégielski & Arnaud Durand: Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, Leibniz International Proceedings in Informatics (LIPIcs) 16. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, pp. 228–242, doi:10.4230/LIPIcs.CSL.2012.228.
  8. Simon J. Gay, António Ravara & Vasco T. Vasconcelos (2003): Session Types for Inter-Process Communication. Technical Report TR-2003-133. Department of Computing Science, University of Glasgow.
  9. Jean-Yves Girard (1995): Linear Logic: its syntax and semantics. In: Jean-Yves Girard, Yves Lafont & Laurent Regnier: Advances in Linear Logic, London Mathematical Society Lecture Notes Series 222. Cambridge University Press, doi:10.1017/CBO9780511629150.
  10. Jean-Yves Girard, Paul Taylor & Yves Lafont (1989): Proofs and Types. Cambridge University Press, New York, NY, USA.
  11. M. Gordon, R. Milner & C. P. Wadsworth (1979): Edinburgh LCF: A Mechanized Logic of Computation (Lecture Notes in Computer Science), first edition 78. Springer-Verlag, doi:10.1007/3-540-09724-4_3.
  12. Ferruccio Guidi, Claudio Sacerdoti Coen & Enrico Tassi (2016): Implementing Type Theory in Higher Order Constraint Logic Programming. Working paper or preprint.
  13. J. Harrison (1996): HOL Light: A tutorial introduction. Lecture Notes in Computer Science, pp. 265–269, doi:10.1007/BFb0031814.
  14. Bas van den Heuvel & Jorge A. Pérez (2020): Session Type Systems based on Linear Logic: Classical versus Intuitionistic. Electronic Proceedings in Theoretical Computer Science 314, pp. 1–11, doi:10.4204/eptcs.314.1.
  15. Kohei Honda (1993): Types for dyadic interaction, pp. 509–523. Springer, Berlin, Heidelberg, doi:10.1007/3-540-57208-2_35.
  16. William A. Howard (1980): The formulas-as-types notion of construction. In: J. P. Seldin & J. R. Hindley: To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, pp. 479–490. Reprint of 1969 article.
  17. Deepak Kapur & Paliath Narendran (1992): Complexity of unification problems with associative-commutative operators. Journal of Automated Reasoning 9(2), pp. 261–288, doi:10.1007/BF00245463.
  18. Joachim Lambek (1961): On the calculus of syntactic types. Structure of language and its mathematical aspects 166, pp. C178, doi:10.1090/psapm/012.
  19. Dale Miller (1996): Forum: A multiple-conclusion specification logic. Theoretical Computer Science 165(1), pp. 201 – 232, doi:10.1016/0304-3975(96)00045-X.
  20. Dale Miller & Gopalan Nadathur (2012): Programming with Higher-Order Logic, 1st edition. Cambridge University Press, New York, NY, USA, doi:10.1017/CBO9781139021326.
  21. Robin Milner (1991): The polyadic n-calculus: a tutorial. Logic and Algebra of Specification 94, pp. 91–180, doi:10.1007/978-3-642-58041-3_6.
  22. Ulf Norell (2007): Towards a practical programming language based on dependent type theory. Chalmers University of Technology.
  23. Petros Papapanagiotou & Jacques Fleuriot (2010): An Isabelle-Like Procedural Mode for HOL Light. In: Christian G. Fermüller & Andrei Voronkov: Logic for Programming, Artificial Intelligence, and Reasoning, Lecture Notes in Computer Science 6397. Springer, pp. 565–580, doi:10.1007/978-3-642-16242-8_40.
  24. Petros Papapanagiotou & Jacques Fleuriot (2015): Modelling and Implementation of Correct by Construction Healthcare Workflows, pp. 28–39. Springer International Publishing, Cham, doi:10.1007/978-3-319-15895-2_3.
  25. Petros Papapanagiotou & Jacques Fleuriot (2019): A Pragmatic, Scalable Approach to Correct-by-Construction Process Composition Using Classical Linear Logic Inference. In: Fred Mesnard & Peter J. Stuckey: Logic-Based Program Synthesis and Transformation. Springer International Publishing, Cham, pp. 77–93, doi:10.1007/978-3-030-13838-7_5.
  26. Petros Papapanagiotou, Jacques Fleuriot & Sean Wilson (2012): Diagrammatically-Driven Formal Verification of Web-Services Composition. In: Philip Cox, Beryl Plimmer & Peter Rodgers: Diagrammatic Representation and Inference, Lecture Notes in Computer Science 7352. Springer Berlin Heidelberg, pp. 241–255, doi:10.1007/978-3-642-31223-6_25.
  27. Petros Papapanagiotou & Jacques D. Fleuriot (2013): Formal verification of collaboration patterns in healthcare. Behaviour & Information Technology, pp. 1–16, doi:10.1080/0144929X.2013.824506.
  28. Lawrence C. Paulson (1990): Isabelle: The Next 700 Theorem Provers. Logic and Computer Science 31, pp. 361–386.
  29. Lawrence C. Paulson (1994): Isabelle: A Generic Theorem Prover. Lecture Notes in Computer Science 828. Springer, doi:10.1007/BFb0030541.
  30. Frank Pfenning, Luis Caires & Bernardo Toninho (2011): Proof-Carrying Code in a Session-Typed Process Calculus. In: Jean-Pierre Jouannaud & Zhong Shao: Certified Programs and Proofs, Lecture Notes in Computer Science 7086. Springer Berlin Heidelberg, pp. 21–36, doi:10.1007/978-3-642-25379-9_4.
  31. J. Power, C. Webster, C. Maynooth & I. Kildare (1999): Working with Linear Logic in Coq. In: 12th International Conference on Theorem Proving in Higher Order Logics, Work-in-Progress Report.
  32. Bernardo Toninho, Luís Caires & Frank Pfenning (2011): Dependent session types via intuitionistic linear type theory. In: Proceedings of the 13th international ACM SIGPLAN symposium on Principles and practices of declarative programming, PPDP '11. ACM, New York, NY, USA, pp. 161–172, doi:10.1145/2003476.2003499.
  33. Philip Wadler (2014): Propositions as sessions. Journal of Functional Programming 24(2-3), pp. 384–418, doi:10.1017/S095679681400001X.
  34. Philip Wadler (2015): Propositions As Types. Commun. ACM 58(12), pp. 75–84, doi:10.1145/2699407.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org