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