@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},
)