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 | 271 | 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 | 99 | 2007 |

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

Formalizing O notation in Isabelle/HOL J Avigad, K Donnelly International Joint Conference on Automated Reasoning, 357-371, 2004 | 42 | 2004 |

Ats: A language that combines programming with theorem proving S Cui, K Donnelly, H Xi International Workshop on Frontiers of Combining Systems, 310-320, 2005 | 25 | 2005 |

Ats: A language that combines programming with theorem proving S Cui, K Donnelly, H Xi International Workshop on Frontiers of Combining Systems, 310-320, 2005 | 25 | 2005 |

Transactional events K Donnelly, M Fluet Journal of Functional Programming 18 (5-6), 649, 2008 | 23 | 2008 |

The inverse method for the logic of bunched implications K Donnelly, T Gibson, N Krishnaswami, S Magill, S Park International Conference on Logic for Programming Artificial Intelligence …, 2005 | 19 | 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 | 18 | 2007 |

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

Selective open recursion: Modular reasoning about components and inheritance J Aldrich, K Donnelly SAVCBS 2004 Specification and Verification of Component-Based Systems, 26, 2004 | 14 | 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 (4), 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 Boston University Computer Science Department, 2008 | 2 | 2008 |

System F with constraint types K Donnelly Boston University, 2008 | 2 | 2008 |

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 |