33 Oxford Street
Division of Engineering and Applied Science
Harvard University
Cambridge, MA 02138
phone: (617) 496-0141
fax: (617) 495-2489
e-mail:
Postdoctoral researcher
| Maxwell Dworkin 307
33 Oxford Street Division of Engineering and Applied Science Harvard University Cambridge, MA 02138 phone: (617) 496-0141 fax: (617) 495-2489 e-mail: |
My research interest is in the design and implementation of programming languages and methodologies that facilitate specification and verification of various program properties. My recent focus has been on the design of a programming language which integrates the well-known program logics, like Hoare and Separation Logic, with modern programming features for abstraction, information hiding and code reuse, such as higher-order functions, monads, polymorphism and modules.
I am also interested in all aspects of compilation and optimization of such languages, and in other formal verification methods, such as interactive and automated theorem proving, decision procedures, program analysis and software model checking.
Personal: CV, Research statement, Teaching statement.
Supervisor: Greg Morrisett
Publications
Type-theoretic Semantics
for Transactional Concurrency
Aleksandar Nanevski, Paul Govereau, Greg Morrisett
Extended version available as technical report TR-09-07, Harvard
University, July 2007.
Hoare Type Theory,
Polymorphism and Separation
Aleksandar Nanevski, Greg Morrisett, Lars Birkedal
Invited for submission to Journal of Functional Programming, January 2007.
Extended version of the ICFP'06 paper.
Abstract Predicates and
Mutable ADTs in Hoare Type Theory
Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, Lars Birkedal
Proceedings of ESOP'07, pages 189-204, Braga, Portugal, March 2007.
Extended version available as technical report TR-14-06,
Harvard University, September 2006.
Polymorphism and
Separation in Hoare Type Theory
Aleksandar Nanevski, Greg Morrisett, Lars Birkedal
Proceedings of ICFP'06, pages 62-73, Portland, Oregon, September 2006.
Extended version available as technical report TR-10-06, Harvard University.
Dependent Type Theory of
Stateful Higher-Order Functions
Aleksandar Nanevski, Greg Morrisett
Extended version available as technical report TR-24-05, Harvard University.
Inferring Invariants in Separation Logic for Imperative List-processing Programs
Stephen Magill, Aleksandar Nanevski, Edmund Clarke and Peter Lee
Proceedings of SPACE'06, pages 47-60, Charleston, SC, January 2006.
Contextual Modal Type Theory
Aleksandar Nanevski, Frank Pfenning, Brigitte Pientka
Revised version to appear in ACM Transactions on Computational Logic.
(submitted September 2005, accepted May 2006)
A Modal Calculus for Exception Handling
Aleksandar Nanevski
Proceedings of IMLA'05, Chicago, June 2005.
Extended versions treating more general control effects available here
and here.
Functional Programming with Names and Necessity
Aleksandar Nanevski
PhD thesis, Carnegie Mellon University, 2004.
A Modal Foundation for Meta-Variables
Aleksandar Nanevski, Brigitte Pientka, Frank Pfenning
Proceedings of MERLIN'03,
pages 159-170, Uppsala, Sweden, 2003.
From Dynamic Binding to State
via Modal Possibility
Aleksandar Nanevski
Proceedings of PPDP'03, pages 207-218, Uppsala, Sweden, 2003.
Staged Computation with Names
and Necessity
Aleksandar Nanevski, Frank Pfenning
Journal of Functional Programming, 15(6):893-939, November 2005.
Meta-Programming with Names and
Necessity
Supersedes the paper published
in Proceedings of ICFP'02, Pittsburgh, PA, pages 206-217, October 2002.
Slides.
Automatic Generation of Staged Geometric
Predicates
Aleksandar Nanevski, Guy Blelloch, Robert Harper
Higher-Order and Symbolic Computation, 16(4):379-400, December 2003.
Conference version
appeared in Proceedings of ICFP 2001, Florence, Italy, pages 217-228, September 2001.
Slides. Extended version
available as technical report CMU-CS-01-141,
June 2001. PDF.
Software
Interpreter for effect systems presented in the papers on control flow effects and state.