Publications

Kevin Donnelly
PhD Student
Computer Science Department
111 Cummington Street
Boston, MA 02215

Office: 177 MCS
Email: png of email address

Home

Classes

Publications

Publications:

Automated Reasoning

Jeremy Avigad and Kevin Donnelly, A Decision Procedure for Linear "Big O" Equations, Journal of Automated Reasoning, vol. 38, no. 4, pp353--373, 2007. SpringerLink
Jeremy Avigad, Kevin Donnelly, David Gray, and Paul Raff, A formally verified proof of the prime number theorem, to appear in the ACM Transactions on Computational Logic. [pdf]
Kevin Donnelly, Tyler Gibson, Neel Krishnaswami, Steven Magill and Sungwoo Park, The Inverse Method for the Logic of Bunched Implications, In Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2004), Springer-Verlag LNCS 3452, pp. 466--480, Montevideo, Uruguay, March 2005.
[ps, pdf] ©Springer-Verlag
Jeremy Avigad and Kevin Donnelly, Formalizing O Notation in Isabelle/HOL, In Proceedings of the 2nd International Joint Conference on Automated Reasoning (IJCAR 2004), Springer-Verlag LNCS 3097, pp. 357--371, Cork, Ireland, July 2004.
[pdf] ©Springer-Verlag

Programming Languages

Kevin Donnelly and Hongwei Xi, A Formalization of Strong Normalization for Simply-Typed Lambda Calculus and System F, Electronic Notes in Theoretical Computer Science, vol. 174, issue 5, pp109--125, June 2007. [pdf]
Martin Sulzmann, Manuel Chakravarty, Simon Peyton Jones and Kevin Donnelly, System F with Type Equality Coercions, In Proceedings of the Workshop on Types in Language Design and Implementation, Nice, France, pp 53--66, January, 2007.
Kevin Donnelly and Matthew Fluet, Transactional Events, In Proceedings of the International Conference on Functional Programming (ICFP'06), Portland, Oregon, September 2006. [pdf, ps]
Kevin Donnelly, Joe Hallett and Assaf Kfoury, Formal Semantics for Weak References. In Proceedings of International Symposium on Memory Management (ISMM 2006), Ottawa, Ontario, Canada, pages 126-137, June 2006. [This version coantains minor revisions] (ps.gz, pdf)
Kevin Donnelly and Hongwei Xi, Combining Higher-Order Abstract Syntax with First-Order Abstract Syntax in ATS, In Proceedings of the Workshop on Mechanized Reasoning about Languages with Variable Binding (MERLIN'05), Tallinn, Estonia, September 2005.
[pdf,ps]
Sa Cui, Kevin Donnelly and Hongwei Xi, ATS: A Language That Combines Programming with Theorem Proving, In Proceedings of the 5th International Workshop on Frontiers of Combining Systems (FroCos'05), Vienna, Austria, September 2005.
[pdf,ps]
Jonathan Aldrich and Kevin Donnelly, Selective Open Recursion: Modular Reasoning About Components and Inheritance, In Proceedings of Specification and Verification of Component Based Systems (SAVCBS'04), Newport Beach, CA, November 2004.
[pdf]