System F with type equality coercions M Sulzmann, MMT Chakravarty, SP Jones, K Donnelly Proceedings of the 2007 ACM SIGPLAN international workshop on Types in …, 2007 | 326 | 2007 |

A formally verified proof of the prime number theorem J Avigad, K Donnelly, D Gray, P Raff ACM Transactions on Computational Logic (TOCL) 9 (1), 2-es, 2007 | 111 | 2007 |

Transactional events K Donnelly, M Fluet ACM SIGPLAN Notices 41 (9), 124-135, 2006 | 47 | 2006 |

Formalizing *O* Notation in Isabelle/HOLJ Avigad, K Donnelly International Joint Conference on Automated Reasoning, 357-371, 2004 | 47 | 2004 |

Transactional events1 K Donnelly, M Fluet Journal of Functional Programming 18 (5-6), 649-706, 2008 | 27 | 2008 |

Ats: A language that combines programming with theorem proving S Cui, K Donnelly, H Xi Frontiers of Combining Systems: 5th International Workshop, FroCoS 2005 …, 2005 | 26 | 2005 |

A formalization of strong normalization for simply-typed lambda-calculus and system F K Donnelly, H Xi Electronic Notes in Theoretical Computer Science 174 (5), 109-125, 2007 | 25 | 2007 |

Formal semantics of weak references K Donnelly, JJ Hallett, A Kfoury Proceedings of the 5th international symposium on Memory management, 126-137, 2006 | 24 | 2006 |

The inverse method for the logic of bunched implications K Donnelly, T Gibson, N Krishnaswami, S Magill, S Park Logic for Programming, Artificial Intelligence, and Reasoning: 11th …, 2005 | 24 | 2005 |

Selective open recursion: Modular reasoning about components and inheritance J Aldrich, K Donnelly SAVCBS 2004 Specification and Verification of Component-Based Systems, 26, 2004 | 15 | 2004 |

Combining higher-order abstract syntax with first-order abstract syntax in ATS K Donnelly, H Xi Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about …, 2005 | 10 | 2005 |

A decision procedure for linear “big O” equations J Avigad, K Donnelly Journal of Automated Reasoning 38, 353-373, 2007 | 3 | 2007 |

The complexity of restricted variants of the stable paths problem K Donnelly, A Kfoury, A Lapets Fundamenta Informaticae 103 (1-4), 69-87, 2010 | 2 | 2010 |

On the stable paths problem and a restricted variant K Donnelly, A Kfoury Technical Report BUCS-TR-2008-001, CS Dept., Boston University, 2008 | 2 | 2008 |

System F with constraint types K Donnelly Boston University Computer Science Department, 2007 | 1 | 2007 |

GRADUATE SCHOOL OF ARTS AND SCIENCES K DONNELLY SCHOOL OF ARTS AND SCIENCES Thesis SYSTEM F WITH CONSTRAINT TYPES by KEVIN …, 2008 | | 2008 |

A formally verified proof of the prime number theorem (draft) J Avigad, K Donnelly, D Gray, P Raff | | 2005 |

Some Considerations on a Calculus with Weak References K Donnelly, AJ Kfoury Boston University Computer Science Department, 2005 | | 2005 |

Number Theory J Avigad, K Donnelly, D Gray, A Kramer, LC Paulson, P Raff, ... | | 2004 |

Formalization of O Notation in Isabelle/HOL K Donnelly | | 2004 |