Dominic Mulligan
Research
In September 2010 I took up a postdoctoral position in the
Department of Computer Science at the
University of Bologna.
Here, I am employed by the European Union's FET-Open funded
CerCo (Certified Complexity) project, a collaboration between the Universities of Bologna,
Edinburgh and
Paris 7 (Diderot).
CerCo aims to produce a certified concrete complexity preserving compiler for a large subset of the C programming language, suitable for use in embedded systems development.
Prior to my move to Italy, I was a PhD student in the
Dependable Systems Group of the
Department of Mathematical and Computer Sciences at
Heriot-Watt University, Edinburgh.
There, I studed under the supervision of
Dr. Murdoch J. Gabbay and
Prof. Phil W. Trinder.
My doctoral research was related to nominal techniques, specifically studying calculi with internalised notions of metavariable, and a novel nominal unification algorithm.
I passed my
viva in Autumn 2010, examined by
Dr. Maribel Fernandez and
Prof. Greg Michaelson.
Contact
My e-mail address is dominic DOT p DOT mulligan AT gmail DOT com.
Publications
Journal papers
-
Permissive nominal terms and their unification: an infinite, coinfinite approach to nominal techniques,
Gilles Dowek, Murdoch J. Gabbay and Dominic P. Mulligan,
Accepted for publication in the Logic Journal of the Interest Group in Pure Logic.
-
Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms,
Murdoch J. Gabbay and Dominic P. Mulligan,
Journal of Information and Computation,
Volume 208, issue 3, pages 230–258. 2010.
Workshop proceedings
-
Universal algebra over lambda-terms and nominal terms: the connection in logic between nominal techniques and higher-order variables,
Murdoch J. Gabbay and Dominic P. Mulligan,
Presented at the 4th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2009).
-
The two-level lambda-calculus,
Murdoch J. Gabbay and Dominic P. Mulligan,
Electronic Notes in Theoretical Computer Science,
Volume 246, pages 107–129. 2009.
-
Permissive nominal terms and their unification,
Gilles Dowek, Murdoch J. Gabbay and Dominic P. Mulligan,
Presented at the 24th Convegno Italiano di Logica Computazionale (CILC 2009).
-
Semantic nominal terms,
Murdoch J. Gabbay and Dominic P. Mulligan,
Presented at the 2nd International Workshop on the Theory and Applications of Abstraction, Substitution and Naming (TAASN 2009).
-
One-and-a-half level terms: Curry-Howard for incomplete derivations,
Murdoch J. Gabbay and Dominic P. Mulligan,
Proceedings of the 15th International Workshop on Logic, Language, Information and Computation (WoLLIC 2008),
Lecture Notes in Artificial Intelligence 5110, pgs. 179–193.
Thesis
-
Extensions of nominal terms,
Dominic P. Mulligan,
PhD thesis, Heriot-Watt University. 2011.
Posters
-
Certified complexity,
Roberto Amadio, Andrea Asperti, Nicolas Ayache, Brian Campbell, Dominic P. Mulligan, Randy Pollack, Yann Regis-Giannas, Claudio Sacerdoti Coen and Ian Stark.
Presented at the EU Future and Emerging Technologies Exhibition. 2011.
Technical reports
-
Permissive nominal terms,
Gilles Dowek, Murdoch J. Gabbay and Dominic P. Mulligan.
INRIA technical report 6682. 2008.
Under construction or consideration
-
Nominal semantics of simply typed lambda-calculus,
Murdoch J. Gabbay and Dominic P. Mulligan,
submitted to Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2011),
-
On the correctness of an assembler for the MCS-51 microprocessor,
Dominic P. Mulligan and Claudio Sacerdoti Coen,
submitted to Certified Proofs and Programs (CPP 2011),
-
A formalisation of the MCS-51 microprocessor in Matita,
Dominic P. Mulligan and Claudio Sacerdoti Coen,
submitted to Formal Methods in Computer Aided Design (FMCAD 2011).
-
Certified complexity,
Roberto Amadio, Andrea Asperti, Nicolas Ayache, Brian Campbell, Dominic P. Mulligan, Randy Pollack, Yann Regis-Giannas, Claudio Sacerdoti Coen and Ian Stark.
submitted to FET-Essence. 2011.