S. Abramsky (1994):
Proofs as processes.
Theoretical Computer Science 135(1),
pp. 5–9,
doi:10.1016/0304-3975(94)00103-0.
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.
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.
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.
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.
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.
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.
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.
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.
Jean-Yves Girard, Paul Taylor & Yves Lafont (1989):
Proofs and Types.
Cambridge University Press,
New York, NY, USA.
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.
Ferruccio Guidi, Claudio Sacerdoti Coen & Enrico Tassi (2016):
Implementing Type Theory in Higher Order Constraint Logic Programming.
Working paper or preprint.
J. Harrison (1996):
HOL Light: A tutorial introduction.
Lecture Notes in Computer Science,
pp. 265–269,
doi:10.1007/BFb0031814.
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.
Kohei Honda (1993):
Types for dyadic interaction,
pp. 509–523.
Springer,
Berlin, Heidelberg,
doi:10.1007/3-540-57208-2_35.
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.
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.
Joachim Lambek (1961):
On the calculus of syntactic types.
Structure of language and its mathematical aspects 166,
pp. C178,
doi:10.1090/psapm/012.
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.
Dale Miller & Gopalan Nadathur (2012):
Programming with Higher-Order Logic,
1st edition.
Cambridge University Press,
New York, NY, USA,
doi:10.1017/CBO9781139021326.
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.
Ulf Norell (2007):
Towards a practical programming language based on dependent type theory.
Chalmers University of Technology.
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.
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.
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.
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.
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.
Lawrence C. Paulson (1990):
Isabelle: The Next 700 Theorem Provers.
Logic and Computer Science 31,
pp. 361–386.
Lawrence C. Paulson (1994):
Isabelle: A Generic Theorem Prover.
Lecture Notes in Computer Science 828.
Springer,
doi:10.1007/BFb0030541.
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.
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.
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.
Philip Wadler (2014):
Propositions as sessions.
Journal of Functional Programming 24(2-3),
pp. 384–418,
doi:10.1017/S095679681400001X.
Philip Wadler (2015):
Propositions As Types.
Commun. ACM 58(12),
pp. 75–84,
doi:10.1145/2699407.