Computer Science Department, Trinity College

Matthew Hennessy

Publications available online:

Matthew Hennessy. A coinductive equational characterisation of trace inclusion for regular processes
Lecture Notes in Computer Science, volume 10460, pages 449-465, Springer 2017. DOI 10.1007/978-3-319-63121-9.
Vasileios Koutavas, Maciej Gazda and Matthew Hennessy. Distinguishing between Communicating Transactions
To appear in Information and Computation, 2017.
Here is a talk on the subject given at Open Problems in Concurrency Theory II, Vienna, June, 2017.
Andrea Cerone and Matthew Hennessy. Characterising Testing Preorders for Broadcasting Distributed Systems
Presented at 9th International Symposioum on Trustworthy Computing, Rome, September, 2014.
Giovanni Bernardi and Matthew Hennessy. Using higher-order contracts to model sessions types (Extended Abstract)
Presented at Concur 2014, Rome, September, 2014.
The conference version is based on the orignal draft of a full paper, , from December, 2013.
The final version has been published in Logical Methods in Computer Science , Vol. 12(2:10): 1-43 (2016).
DOI: 10.2168/LMCS-12(2:10)2016.

Vasileios Koutavas, Carlo Spaccasassi and Matthew Hennessy. Bisimulations for Communicating Transactions (Extended abstract).
Presented at Fossacs 2014, Grenoble, April, 2014.
Edsko de Vries, Adrian Francalanza and Matthew Hennessy. Compositional Reasoning for Explicit Resource Management in Channel-Based Concurrency
Final version published in Logical Methods in Computer Science, Vol 10(2) pp 1-51, 2014.
DOI:10.2168/LMCS-10(2:15)2014.
Edsko de Vries, Adrian Francalanza and Matthew Hennessy. Uniqueness typing for resource management in message-passing concurrency
Final version published in Journal of Logic and Computation, 24(3):531-556, 2014.
DOI:dx.doi.org/10.1093/logcom/exs022.
Giovanni Bernardi and Matthew Hennessy. Compliance and testing preorders differ
Presented at Second International Workshop on Behavioural Types, Madrid, September, 2013.
Giovanni Bernardi and Matthew Hennessy. Mutually Testing Processes.
Presented at CONCUR 2013, Buenas Aires, August, 2013.
Here is the full version, December 2013.
Final version published in Logical Methods in Computer Science, 11(2):1-43, 2015.
DOI:10.2168/LMCS-11(2:1)2015.
Vasileios Koutavas and Matthew Hennessy. Symbolic Bisimulations for a Higher-Order Distributed Language with Passivation (Extended abstract).
Presented at CONCUR 2013, Buenas Aires, August, 2013.
Andrea Cerone, Matthew Hennessy and Massimo Merro. Modelling MAC-layer communications in wireless systems.
Presented at Coordination 2013, Firenze, Italy, June, 2013.
Here is the associated Technical report, September 2012.
Superceded by full version, December 2013.
Final version published in Logical Methods in Computer Science, 11(1):1-59, 2015.
DOI:10.2168/LMCS-11(2:1)2015.
Yuxin Deng and Matthew Hennessy. On the Semantics of Markov Automata,
Final version was published in Information and Computation. 222:139-168, 2013. DOI:10.1016/j.ic.2012.10.010
An extended abstract was presented at The 38th International Colloquium on Automata, Languages and Programming (ICALP11), Zurich, Switzerland, July 2011.
Here is a talk on the subject given to the Foundations and Methods Research Group at Trintiy College in March 2011.
Supercedes the original technical report.
Yuxin Deng, Rob vanGlabbeek, Matthew Hennessy and Carroll Morgan. Real-Reward Testing for Probabilistic Processes.
To appear in Theoretical Computer Science , 2013.
An extended abstract was presented at Ninth Workshop on Quantitative Aspects of Programming Languages (QAPL 2011) , Saarbrucken, Germany, April 2011.
Here is a talk on the subject given at the workshop.

Andrea Cerone and Matthew Hennessy. Modelling probabilistic wireless networks (Extended Abstract).
Presented at 7th International Federated Conference on Distributed Computing Techniques, Stockholm, Italy, 13-16 June 2012.
An associated technical report, February 2012.
This is now superceded by the final version which has been published in Logical Methods in Computer Science. 9(3):1-68, 2013.
DOI: dx.doi.org/10.2168/LMCS-9(3:26)2013.
Vasileios Koutavas and Matthew Hennessy. First-Order Reasoning for Higher-Order Concurrency.
Final version published in Journal of Computer Languages. 38(3) 242-277, 2012.
DOI: dx.doi.org/10.1016/j.cl.2012.04.003.
Supercedes Technical Report, July 2009:

Giovanni Bernardi and Matthew Hennessy. Modelling session types using contracts,
An extended abstract was presented at 27th ACM Symposium on Applied Computing, Riva del Garda, Italy, 26-30 March 2012.
A technical report on the same subject, August 2011.
The final version has been published in Mathematical Structures in Computer Science , 26(3): 510-560 (2016).
DOI: dx.doi.org/10.1017/S0960129514000243.

Matthew Hennessy. Exploring probabilistic bisimulations, part I, 2012
The final version has been published in Formal Aspects of Computing, 2012.
Here is a talk on the subject given at IMT Lucca, Italy, November 2012.

Vasileios Koutavas and Matthew Hennessy. A Testing Theory for a Higher-Order Cryptographic Language (Extended Abstract),

20th European Symposium on Programming (ESOP'11)

Matthew Hennessy. Exploring probabilistic bisimulations, part I, 2012
The final version has been published in Formal Aspects of Computing, 2012.
Here is a talk on the subject given at IMT Lucca, Italy, November 2012.

Vasileios Koutavas and Matthew Hennessy. A Testing Theory for a Higher-Order Cryptographic Language (Extended Abstract),

20th European Symposium on Programming (ESOP'11)

Yuxin Deng and Matthew Hennessy. Compositional Reasoning for Markov Decision Processes, . Published in Science of Computer Programming, 2013.
An extended abstract was presented at Fundamentals of Software Engineering (FSEN 2011), Tehran, Iran, April 2011.
Here is a talk on the subject given as an invited talk at Fundamentals of Software Engineering (FSEN 2011), Tehran, Iran, April 2011.

Edsko de Vries, Vasileios Koutavas and Matthew Hennessy. Liveness of Communicating Transactions (Extended Abstract), 2010.
Presented at The Eight ASIAN Symposium on Programming Languages and Systems , Shanghai, November 2010.
DOI: dx.doi.org/10.1007/978-3-642-17164-2_27.

Edsko de Vries, Vasileios Koutavas and Matthew Hennessy. Communicating Transactions (Extended Abstract).
Presented at 21st International Conference on Concurrency Theory (CONCUR 2010), Paris, France, September 2010.
DOI: dx.doi.org/10.1007/978-3-642-15375-4_39.

Andrea Cerone and Matthew Hennessy. Process Behaviour: Formulae vs. Tests (Extended Abstract).
Presented at 17th International Workshop on Expressiveness in Concurrency (Express'10) , Paris, France, August 2010.
In Sibylle Froschle and Frank D. Valencia (Eds.): Proceedings 17th International Workshop on Expressiveness in Concurrency,
Electronic Proceedings in Theoretical Computer Science, Vol. 41, pp. 31-45, 2010.
DOI:10.4204/EPTCS.41.3
A technical report: the full-version of the paper.

Yuxin Deng and Rob van Glabbeek and Matthew Hennessy and Carroll Morgan. Testing Finitary Probabilistic Processes (Extended Abstract).
Presented at 20th International Conference on Concurrency Theory (CONCUR'09) , Bologna, Italy, September 2009.
Here is a draft full version of the paper

Edsko de Vries, Adrian Francalanza and Matthew Hennessy. Uniqueness Typing for Resource Management in Message-Passing Concurrency.
Presented at First International Workshop on Linearity (LINEARITY 2009) , Coimbra, Portugal September 2009.
In M. Florido and I. Mackie (Eds.): First International Workshop on Linearity (LINEARITY 2009). Electronic Proceedings in Theoretical Computer Science, Vol. 22, pp. 26-37, 2010.

Matthew Hennessy. A calculus for costed computations, 2009
Final version appeared in Logical Methods in Computer Science, Volume 7, issue 1, paper 9, 2011. DOI: 10.2168/LMCS-7(1:7)2011.

Matthew Hennessy and Manish Gaur. Counting the cost in the picalculus.
Presented at 1st Interaction and Concurrency Experience (ICE'08) , Reykjavik, Iceland, July 2008.
The final version appeared in Proceedings of 1st Interaction and Concurrency Experience (ICE'08) , Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers B. V., Vol. 229, no. 3, pp 117-129, 2009.
DOI: dx.doi.org/10.1016/j.entcs.2009.06.042

Gerard Boudol and Ilaria Castellani and Matthew Hennessy and Mogens Nielsen and Glynn Winskel. Twenty years on: Reflections on the CEDISYS project. Combining true concurrency with process algebra.
The final version appeared in Lecture Notes in Computer Science, Vol. 5065, pp 757-777, 2008.

Yuxin Deng and Rob van Glabbeek and Matthew Hennessy and Carroll Morgan and Chenyi Zhang. Characterising Testing Preorders for Finite Probabilistic Processes.
Logical Methods in Computer Science, Vol 4(4:4), pp 1-33, 2008.
The latest version:
An extended abstract has been presented at 22nd Annual IEEE Symposium on Logic in Computer Science (LICS'07) , July 2007.
Adrian Francalanza a and Matthew Hennessy. A Fault Tolerance Bisimulation Proof for Consensus.
An extended abstract has been presented at ESOP'07 16th European Symposium on Programming , March 2007.
Yuxin Deng and Rob van Glabbeek and Matthew Hennessy and Carroll Morgan and Chenyi Zhang. Remarks on Testing Probabilistic Processes.
The latest version.
Here is a talk on the subject given at Symposium for Gordon Plotkin , September 2006.
The final version appeared in Electronic Notes in Theoretical Computer Science, Vol. 171, pp 359-397, 2007.
Daniele Gorla and Matthew Hennessy and Vladimiro Sassone. Inferring Dynamic Credentials for Role-based Trust Management.
An extended abstract has been presented at the conference PPDP 2006.
Here is a talk on the subject by Vladimiro Sassone.
Adrian Francalanza and Matthew Hennessy. A Theory for Observational Fault Tolerance.
An extended abstract has been presented at the conference Fossacs 2006. SConf
Here is a talk on the subject by Adrian.
The latest version. The final version has appeared in the Journal of Logic and Algebraic Programming
Alberto Ciaffaglione, Matthew Hennessy and Julian Rathke. Proof methodologies for behavioural equivalence in distributed pi-calculus .
Sussex Technical Report cs03:2005 .
An extended abstract has been presented at the conference FORTE 2005.
Samuel Hym and Matthew Hennessy. Adding recursion to dpi.
An extended abstract was presented at the workshop Structural Operational Semantics 2005.
The latest version.
The final version has been published in Theoretical Computer Science, 2007.
Adrian Francalanza and Matthew Hennessy. A Theory of System Behaviour in the Presence of Node and Link Failures.
Originally published as Sussex Technical Report cs01:2005.
See slides for a talk on the subject.
An extended abstract has been presented at the conference CONCUR 2005.
The latest version.
The final version has appeared in Information and Computation, Vol. 206, No. 6, pp 711-759, 2008.
Daniele Gorla and Matthew Hennessy and Vladimiro Sassone. Security Policies as Membranes in Systems for Global Computing.
The latest version supercedes Sussex Technical Report CS02:2004.
An extended abstract has been presented at the conference Foundations of Global Ubiquitous Computing, 2004.
Final version has been published in Logical Methods in Computer Science, 2005.
Matthew Hennessy and Julian Rathke and Nobuko Yoshida. Safedpi: a language for controlling mobile code.
The latest version supercedes the original Sussex Technical Report cs02:2003 (in ps)
and the extended abstract which was presented at the conference FOSSACS04.
Final version is published in Acta Informatica, 2005.
These slides covers some of the material.
Matthew Hennessy . The Security Picalculus and Non-interference.
Final version appeared in Journal of Logic and Algebraic Programming, 63:1,3-34, 2004.
The latest version supercedes both the extended abstract , which was presented at the conference MFPSXIX, and the original Sussex Technical Report cs2000::05.
See slides (in pdf) for an (introductory) talk.
Matthew Hennessy and Massimo Merro and Julian Rathke. Towards a Behavioural Theory of Access and Mobility Control in Distributed Systems.
The final version appeared in Theoretical Computer Science, 322:615-669, 2003.
The latest version supercedes the original Sussex Technical Report cs2002::01 and the extended abstract , which was presented at the conference FOSSACS03.
These slides covers some of the material.
Massimo Merro and Matthew Hennessy. Bisimulation Congruences in Safe Ambients.
Final version has been published in ACM Transactions on Programming Languages and Systems, 2005.
An extended abstract was presented at the conference POPL02.
The latest version supercedes the original Sussex Technical Report cs2001::05.
Matthew Hennessy and Julian Rathke. Typed behavioural equivalences for processes in the presence of subtyping.
Final version appeared in Mathematical Structures in Computer Science, 14:5:651-684, 2003.
The latest version supercedes both the extended abstract , which was presented at the conference CATS02, and the original Sussex Technical Report cs2001::02.
James Riely and Matthew Hennessy. Trust and partial typing in open systems of mobile agents.
Final version appeared in Journal of Automated Reasoning, 31:335-370, 2003.
The latest version (Supersedes University of Sussex Technical Report cs1998:04)
Matthew Hennessy and James Riely. Information flow vs resource access in the asynchronous pi-calculus.
Final in ACM Transactions on Programming Languages and Systems, 5:566-591, 2003.
The latest version supersedes University of Sussex Technical Report cs2000:03.
An extended abstract has been presented at the conference ICALP2000.
See slides (in postscript format) for an (introductory) talk.
Nobuko Yoshida and Matthew Hennessy. Assigning types to processes.
Final version appeared in Information and Computation, 173:82-120, 2002.
The latest version supersedes University of Sussex Technical Report cs1999:02.
An extended abstract has been presented at LICS2000.
See slides (in postscript format) for an (introductory) talk.
Nobuko Yoshida and Matthew Hennessy. Subtyping and Locality in Distributed Higher Order Mobile Processes .
An extended abstract was presented at Concur99.
The complete version is Sussex Technical Report cs1999:01
Matthew Hennessy and James Riely. Resource access control in systems of mobile agents.
Final version appeared in Information and Computation, 173:82-120, 2002.
The latest version supersedes University of Sussex Technical Report cs1998:02.
An extended abstract has been presented at the 3rd international workshop on High-Level Concurrent Languages , a satellite workshop of CONCUR98.
See slides (in postscript format) for an introductory talk.
Matthew Hennessy and James Riely. Type-safe execution of mobile agents in anonymous networks .
The latest version was published in the proceedings of Secure Internet Programming: Proc. of 4th Workshop on Mobile Object Systems, at ECOOP98.
At the workshop an extended abstract was presented. (Supersedes University of Sussex Technical Report cs1998:03)
Matthew Hennessy. A fully abstract denotational semantics for the pi-calculus.
Final version appeared in Theoretical Computer Science, pages 53-89, 2001.
The latest version supersedes University of Sussex Technical Report cs1996:04.
James Riely and Matthew Hennessy. Distributed Processes and Location Failures.
Final version appeared in Theoretical Computer Science, 226:693-735, 2001.
The latest version supersedes University of Sussex Technical Report cs1997:02.
An extended abstract has been presented at ICALP97 .
Matthew Hennessy, Huimin Lin and Julian Rathke. Unique Fixpoint Induction for Message-Passing Process Calculi.
Final version appeared in Science of Computer Programming. 41:241-275, 2001.
The latest version supersedes University of Sussex Technical Report cs1996:05.
An extended abstract of a previous version has been presented at CATS97.
William Ferreira and Matthew Hennessy. A Behavioural theory of first-order cml.
Final version appeared in Theoretical Computer Science. 145(1-2):55-107, 1999.
The latest version supersedes University of Sussex Technical Report cs1995:02.
Chrysafis Hartonas and Matthew Hennessy. Full abstractness for a functional/concurrent language with higher-order value-passing.
Final version appeared in Information and Computation. 145(1):64-106, August 1998.
The latest version supersedes University of Sussex Technical Report cs1997:01.
An extended abstract of a previous version has been presented at CSL97.
Ilaria Castellani and Matthew Hennessy. Testing Theories for Asynchronous Languages.
An extended abstract was presented at FST-TCS98.
M. Hennessy and J. Rathke. Bisimulations for a calculus of broadcasting systems.
Final version appeared in Theoretical Computer Science, 200(1-2):225-260, 28 June 1998.
The latest version supersedes University of Sussex Technical Report cs1995:03.
A. Kiehn and M. Hennessy. On the decidability of non-interleaving process equivalences.
Final version appeared in Fundamenta Informaticae, 30(1):18-33, April 1997.
The latest version supersedes University of Sussex Technical Report cs1994:09.
M Hennessy and H Lin. Proof systems for message-passing process algebras.
Final version appeared in Formal Aspects of Computing, 8(4):379-407, 1996.
The latest version supersedes University of Sussex Technical Report cs1989:05.
Matthew Hennessy and Tim Regan. A process algebra for timed systems.
Final version appeared in Information and Computation, 117(2):221-239, March 1995.
The latest version supersedes University of Sussex Technical Report cs1993:02.
Matthew Hennessy. Concurrent testing of processes.
Final version appeared in Acta Informatica, 32(6):509-543, 1995.
The latest version (Supersedes University of Sussex Technical Report cs1991:11)
M. Hennessy and H. Lin. Symbolic bisimulations.
Final version appeared in Theoretical Computer Science, 138(2):353-389, 20 February 1995.
The latest version supersedes University of Sussex Technical Report cs1992:01.
L. Aceto and M. Hennessy. Adding action refinement to a finite process algebra.
The latest version.
Final version appeared in Information and Computation, 115(2):179-247, December 1994.
M. Hennessy and A. Ing'olfsd'ottir. A theory of communicating processes with value passing.
The latest version.
Final version appeared in Information and Computation, 107(2):202-236, December 1993.
L. Aceto and M. Hennessy. Towards action-refinement in process algebras.
The latest version.
Final version appeared in Information and Computation, 103(2):204-269, April 1993.
L. Aceto and M. Hennessy. Termination, deadlock, and divergence.
The latest version.
Final version appeared in Journal of the ACM, 39(1):147-187, January 1992.
M Hennessy. A proof system for communicating processes with value-passing.
Final version appeared in Formal Aspects of Computing, 3(4):346-366, 1991.
R. Cleaveland and M. Hennessy. Testing equivalence as a bisimulation equivalence.
In J. Sifakis, editor, Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, volume 407 of LNCS, pages 11-23, Berlin, June 1990. Springer.
The latest version.
Final version appeared in Formal Aspects of Computing, 5(1):1-20, 1993.
M Hennessy. Acceptance Trees. The latest version.
Final version appeared in Journal of ACM, 32(4):896-928, October 1985.
Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. The latest version.
Final version appeared in Journal of the ACM, 32(1):137-161, January 1985.
R. De Nicola and M. C. B. Hennessy. Testing equivalences for processes. The latest version.
Final version appeared in Theoretical Computer Science, 34(1-2):83-133, November 1984.
Matthew C. B. Hennessy and Gordon D. Plotkin. A term model for CCS. The latest version.
Published in Mathematical Foundations of Computer Science 1980, Proceedings of the 9th Symposium, volume 88 of Lecture Notes in Computer Science, pages 261-274, Rydzyna, Poland, 1-5 September 1980. Springer.
M. C. B. Hennessy and G. D. Plotkin. Full abstraction for a simple parallel programming language . The latest version.
Published in J. Bečv'ař, editor, Mathematical Foundations of Computer Science 1979, volume 74 of Lecture Notes in Computer Science, pages 108-120, Olomouc, Czechoslovakia, 3-7 September 1979. Springer-Verlag.

Last modified: Wed Jan 23 15:33:46 GMT 2013