Papers

Journal papers:

  • Permissive nominal terms and their unification: an infinite, coinfinite approach to nominal techniques, Gilles Dowek, Murdoch J. Gabbay and Dominic P. Mulligan, Logic Journal of the Interest Group in Pure Logic, volume 18, issue 6, pages 769–822, 2011. (PDF)
  • 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 (PDF)

Workshop and conference papers:

  • The missing link: explaining ELF linking, semantically, Stephen Kell, Dominic P. Mulligan, and Peter Sewell.  Accepted at SPLASH 2016 OOPSLA, 2016 (in submission).  (PDF)
  • An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors, Kathryn Gray, Gabriel Kerneis, Dominic P. Mulligan, Christopher Pulte, Susmit Sarkar and Peter Sewell.  Accepted to the 48th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO 48), 2015.  (PDF)
  • Lem: reusable engineering of real world semantics, Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge and Peter Sewell, proceedings of the 19th International Conference on Functional Programming (ICFP 2014), pages 175–188.  (PDF)
  • Certified Complexity (CerCo), Roberto M. Amadio, Nicolas Ayache, Francois Bobot, Jaap P. Boender, Brian Campbell, Ilias Garnier, Antoine Madet, James McKinna, Dominic P. Mulligan, Mauro Piccolo, Randy Pollack, Yann Régis-Gianas, Claudio Sacerdoti Coen, Ian Stark, and Paolo Tranquilli, proceedings of the 3rd International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA 2013), pages 1–18.  (PDF)
  • On the correctness of an assembler for the MCS-51 microprocessor, Dominic P. Mulligan and Claudio Sacerdoti Coen, proceedings of the 2nd International Conference on Certified Proofs and Programs (CPP 2012), pages 43–59.  (PDF)
  • Nominal Henkin Semantics: simply typed lambda-calculus in Nominal Sets, Murdoch J. Gabbay and Dominic P. Mulligan, proceedings of the 6th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2011), pages 58–75.  (PDF)
  • 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, proceedings of the 4th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2009), pages 64–73.  (PDF)
  • The two-level lambda-calculus, Murdoch J. Gabbay and Dominic P. Mulligan, Electronic Notes in Theoretical Computer Science, Volume 246, pages 107–129. 2009.  (PDF)
  • 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).  (PDF)
  • 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).  (PDF)
  • 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), pages 179–193.  (PDF)

Thesis:

  • Extensions of nominal terms, Dominic P. Mulligan, PhD thesis, Heriot-Watt University. 2011.  (PDF)

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.  (PDF)

Technical reports and manuscripts:

  • Permissive nominal terms, Gilles Dowek, Murdoch J. Gabbay and Dominic P. Mulligan. INRIA technical report 6682. 2008.  (PDF)