Assistant Research Professor

IMDEA Software Institute Edificio IMDEA Software, office 382 Campus Montegancedo UPM 28223 Pozuelo de Alarcon, Madrid SPAIN email: phone: +34-91-101-2202 (ext: 4107) fax: +34-91-101-1358 |

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.

**Professional activities**

- Program chair:
- Program committee (PC) member:
- Invited speaker:

**Publications**

Communicating State Transition Systems for Fine-Grained Concurrent Resources

Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey and German Andres Delbianco

Proceedings of ESOP'14, pages 290-310, 2014.

Associated Coq scripts can be downloaded here.

Modular Reasoning about Heap Paths via Effectively Propositional Formulas

Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski and Mooly Sagiv

Proceedings of POPL'14, pages 385-396, 2014.

Dependent Types for Enforcement of Information Flow and Erasure Policies in Heterogeneous Data Structures

Gordon Stewart, Anindya Banerjee and Aleksandar Nanevski

Proceedings of PPDP'13, pages 145-156, 2013.

Associated Coq scripts can be downloaded here.

Hoare-Style Reasoning with (Algebraic) Continuations

German Andres Delbianco and Aleksandar Nanevski

Proceedings of ICFP'13, pages 363-376, 2013.

Associated Coq scripts can be downloaded here.

Mtac: A Monad for Typed Tactic Programming in Coq

Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski and Viktor Vafeiadis

Proceedings of ICFP'13, pages 87-100, 2013.

Associated Coq scripts can be downloaded here.

Effectively-Propositional Reasoning about Reachability in Linked Data Structures

Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski and Mooly Sagiv

Proceedings of CAV'13, pages 756-772, 2013.

How to Make Ad Hoc Proof Automation Less Ad Hoc

Georges Gonthier, Beta Ziliani, Aleksandar Nanevski and Derek Dreyer

Journal of Functional Programming (JFP), 23(4):357-401, July 2013.

Associated Coq scripts can be downloaded here.

Subjective Auxiliary State for Coarse-Grained Concurrency

Ruy Ley-Wild and Aleksandar Nanevski

Proceedings of POPL'13, pages 561-574, 2013.

Associated Coq scripts can be downloaded here.

Dependent Type Theory for Verification of Information Flow and Access Control Policies

Aleksandar Nanevski, Anindya Banerjee, Deepak Garg

ACM Transactions on Programming Languages and Systems (TOPLAS), 35(2):6:1-6:41, July 2013.

Associated Coq scripts can be downloaded here.

Online appendix with the proof rules is here.

Denotation of contextual modal type theory (CMTT): syntax and metaprogramming

Murdoch J. Gabbay and Aleksandar Nanevski

Journal of Applied Logic (JAL), 11(1):1-29, March 2013.

How to Make Ad Hoc Proof Automation Less Ad Hoc

Georges Gonthier, Beta Ziliani, Aleksandar Nanevski and Derek Dreyer

Proceedings of ICFP'11, pages 163-175, 2011.

Associated Coq scripts and technical appendix can be downloaded here.

Verification of Information Flow and Access Control Policies with Dependent Types

Aleksandar Nanevski, Anindya Banerjee and Deepak Garg

Proceedings of S&P'11, pages 165-179, 2011.

Extended version available as a technical report.

Associated Coq scripts can be downloaded here.

Partiality, State and Dependent Types

Kasper Svendsen, Lars Birkedal and Aleksandar Nanevski

Proceedings of TLCA'11, pages 198-212, 2011.

Extended version available as a technical report.

Associated Coq scripts can be downloaded here.

Structuring the Verification of Heap-Manipulating Programs

Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine

Proceedings of POPL'10, pages 261-274, 2010.

Associated Coq scripts can be downloaded here.

Towards Type-theoretic Semantics
for Transactional Concurrency

Aleksandar Nanevski, Paul Govereau, Greg Morrisett

Proceedings of TLDI'09, pages 79-90, 2009.

Extended version available as technical report TR-09-07, Harvard
University.

Ynot: Dependent Types for Imperative Programs

Aleksandar Nanevski, Greg Morrisett, Avi Shinnar, Paul Govereau, Lars Birkedal.

Proceedings of ICFP'08, pages 229-240, 2008.

The examples from this paper can be downloaded from here.

A Realizability Model for
Impredicative Hoare Type Theory

Rasmus L. Petersen, Lars Birkedal, Aleksandar Nanevski, Greg Morrisett

Proceedings of ESOP'08, pages 337-352, 2008.

Contextual Modal Type Theory

Aleksandar Nanevski, Frank Pfenning, Brigitte Pientka

ACM Transactions on Computational Logic (TOCL), 9(3):1-49, June 2008.

Hoare Type Theory,
Polymorphism and Separation

Aleksandar Nanevski, Greg Morrisett, Lars Birkedal

Journal of Functional Programming (JFP), 18(5&6):865-911, September 2008.

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, 2007.

Extended version available as technical report TR-14-06,
Harvard University.

Polymorphism and
Separation in Hoare Type Theory

Aleksandar Nanevski, Greg Morrisett, Lars Birkedal

Proceedings of ICFP'06, pages 62-73, 2006.

Extended version available as technical report TR-10-06, 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, January 2006.

Dependent Type Theory of
Stateful Higher-Order Functions

Aleksandar Nanevski, Greg Morrisett

Extended version available as technical report TR-24-05, Harvard
University, 2005.

A Modal Calculus for Exception Handling

Aleksandar Nanevski

Proceedings of IMLA'05, June 2005.

Staged Computation with Names
and Necessity

Aleksandar Nanevski, Frank Pfenning

Journal of Functional Programming (JFP), 15(6):893-939, November 2005.

Functional Programming with Names and Necessity

Aleksandar Nanevski

PhD thesis, Carnegie Mellon University, 2004.

Automatic Generation of Staged Geometric
Predicates

Aleksandar Nanevski, Guy Blelloch, Robert Harper

Higher-Order and Symbolic Computation (HOSC), 16(4):379-400, December 2003.

A Modal Foundation for Meta-Variables

Aleksandar Nanevski, Brigitte Pientka, Frank Pfenning

Proceedings of MERLIN'03, pages 159-170, 2003.

From Dynamic Binding to State
via Modal Possibility

Aleksandar Nanevski

Proceedings of PPDP'03, pages 207-218, 2003.

A Nominal Modal Calculus of Effects

Aleksandar Nanevski

Technical Report CMU-CS-03-149, Carnegie Mellon University, June 2003.

Shorter version available here.

Interpreter for effect
systems presented in this report and the PPDP'03 paper.

Meta-Programming with Names and
Necessity

Aleksandar Nanevski

Proceedings of ICFP'02, pages 206-217, 2002. Slides.

Superseded by the technical report CMU-CS-02-123R, November 2002.

Automatic Generation of Staged
Geometric Predicates

Aleksandar Nanevski, Guy Blelloch, Robert Harper

Proceedings of ICFP'01, pages 217-228, 2001. Slides.

Extended version available as technical report CMU-CS-01-141, June 2001.