Formalizing O Notation in Isabelle/HOL. - Jeremy Avigad; Kevin Donnelly (IJCAR, 2004)

The Inverse Method for the Logic of Bunched Implications. - Kevin Donnelly; Tyler Gibson; Neel Krishnaswami; Stephen Magill; Sungwoo Park (LPAR, 2004)

ATS: A Language That Combines Programming with Theorem Proving. - Sa Cui; Kevin Donnelly; Hongwei Xi 001 (FroCoS, 2005)

Combining higher-order abstract syntax with first-order abstract syntax in ATS. - Kevin Donnelly; Hongwei Xi 001 (MERLIN, 2005)

Formal semantics of weak references. - Kevin Donnelly; J. J. Hallett; Assaf J. Kfoury (ISMM, 2006)

A Formalization of Strong Normalization for Simply-Typed Lambda-Calculus and System F. - Kevin Donnelly; Hongwei Xi 001 (LFMTP@FLoC, 2006)

System F with type equality coercions. - Martin Sulzmann; Manuel M. T. Chakravarty; Simon L. Peyton Jones; Kevin Donnelly (TLDI, 2007)

A Decision Procedure for Linear "Big O" Equations. - Jeremy Avigad; Kevin Donnelly (J. Autom. Reason., 2007)

A formally verified proof of the prime number theorem. - Jeremy Avigad; Kevin Donnelly; David Gray; Paul Raff (ACM Trans. Comput. Log., 2007)

Transactional events. - Kevin Donnelly; Matthew Fluet (J. Funct. Program., 2008)

apertium-cy - a collaboratively-developed free RBMT system for Welsh to English. - Francis M. Tyers; Kevin Donnelly (Prague Bull. Math. Linguistics, 2009)

The Complexity of Restricted Variants of the Stable Paths Problem. - Kevin Donnelly; Assaf J. Kfoury; Andrei Lapets (Fundam. Informaticae, 2010)

Leveraging Lexical Resources and Constraint Grammar for Rule-Based Part-of-Speech Tagging in Welsh. - Steven Neale; Kevin Donnelly; Gareth Watkins; Dawn Knight (LREC, 2018)