Associate 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 is in the design and implementation of programming languages and logics for software verification. More specifically, I am interested in applying programming methodology to facilitate the construction of formal proofs in mathematics in general, and of program correctness in particular. My recent focus has been on designing methods for integrating programming with pointers, concurrency, and other important imperative features, into dependent type systems such as that of the proof assistant Coq. The goal of the integration is to leverage the proving power of Coq to obtain effective and scalable ways for reasoning about security and correctness of imperative programs.

I am also interested in all other aspects of formal mathematics and programming language theory and applications related to compilation, optimization, semantics, interactive theorem proving, program extraction, automated deduction, decision procedures, program analysis and model checking.

- Program chair:
- Program committee member:
- Invited keynotes:

**Separation Logic and Concurrency**

Aleksandar Nanevski

Lecture notes for Oregon Programming Languages Summer School (OPLSS), June 2016.

[PDF |
OPLSS16 page]

**Mtac: A Monad for Typed Tactic Programming in Coq**

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

Accepted by Journal of Functional Programming (JFP), April 2015.

[Final revision PDF |
ICFP13 version]

**Mechanized Verification of Fine-grained Concurrent Programs**

Ilya Sergey, Aleksandar Nanevski and Anindya Banerjee

Conference on Programming Language Design and Implementation (PLDI), pages 77-87, 2015.

[PDF |
Coq sources |
Project page]

**Specifying and Verifying Concurrent Algorithms with Histories
and Subjectivity**

Ilya Sergey, Aleksandar Nanevski and Anindya Banerjee

European Symposium on Programming (ESOP), pages 333-358, 2015.

[PDF |
Extended version |
Project page]

**Communicating State Transition Systems for Fine-Grained
Concurrent Resources**

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

European Symposium on Programming (ESOP), pages 290-310, 2014.

[PDF |
Coq cources |
Project page]

**Modular Reasoning about Heap Paths via Effectively
Propositional Formulas**

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

Symposium on Principles of Programming Languages (POPL), pages
385-396, 2014.

[PDF]

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

Gordon Stewart, Anindya Banerjee and Aleksandar Nanevski

Symposium on Principles and Practice of Declarative Programming
(PPDP), pages 145-156, 2013.

[PDF |
Coq sources |
Project page]

**Hoare-Style Reasoning with (Algebraic) Continuations**

German Andres Delbianco and Aleksandar Nanevski

International Conference on Functional Programming (ICFP), pages
363-376, 2013.

[PDF |
Coq sources]

**Mtac: A Monad for Typed Tactic Programming in Coq**

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

International Conference on Functional Programming (ICFP), pages
87-100, 2013.

[PDF |
Coq sources]

**Effectively-Propositional Reasoning about Reachability in
Linked Data Structures**

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

International Conference on Computer Aided Verification (CAV),
pages 756-772, 2013.

[PDF]

**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.

[PDF |
Coq sources |
ICFP11 version]

**Subjective Auxiliary State for Coarse-Grained
Concurrency**

Ruy Ley-Wild and Aleksandar Nanevski

Symposium on Principles of Programming Languages (POPL), pages
561-574, 2013.

[PDF |
Coq sources |
Online appendix |
Project page]

**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.

[PDF |
Coq sources |
Online appendix |
S&P11 version |
Project page]

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

Murdoch J. Gabbay and Aleksandar Nanevski

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

[PDF]

**How to Make Ad Hoc Proof Automation Less Ad Hoc**

Georges Gonthier, Beta Ziliani, Aleksandar Nanevski and Derek
Dreyer

International Conference on Functional Programming (ICFP), pages
163-175, 2011.

[PDF |
Coq sources]

**Verification of Information Flow and Access Control Policies
with Dependent Types**

Aleksandar Nanevski, Anindya Banerjee and Deepak Garg

IEEE Symposium on Security and Privacy (S&P), pages 165-179, 2011.

[PDF |
Extended version |
Coq sources |
Project page]

**Partiality, State and Dependent Types**

Kasper Svendsen, Lars Birkedal and Aleksandar Nanevski

International Conference on Typed Lambda Calculi and Applications
(TLCA), pages 198-212, 2011.

[PDF |
Extended version |
Coq sources |
Project page]

**Structuring the Verification of Heap-Manipulating Programs**

Aleksandar Nanevski, Viktor Vafeiadis and Josh Berdine

Symposium on Principles of Programming Languages (POPL), pages
261-274, 2010.

[PDF |
Coq sources |
Project page]

**Towards Type-theoretic Semantics for Transactional Concurrency**

Aleksandar Nanevski, Paul Govereau and Greg Morrisett

Workshop on Types in Language Design and Implementation (TLDI),
pages 79-90, 2009.

[PDF |
Extended version]

**A Realizability Model for Impredicative Hoare Type
Theory**

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

European Symposium on Programming (ESOP), pages 337-352, 2008.

[PDF |
Project page]

**Ynot: Dependent Types for Imperative Programs**

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

International Conference on Functional Programming (ICFP), pages
229-240, 2008.

[PDF |
Examples
in Coq |
Project page]

**Contextual Modal Type Theory**

Aleksandar Nanevski, Frank Pfenning and Brigitte Pientka

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

[PDF]

**Hoare Type Theory, Polymorphism and Separation**

Aleksandar Nanevski, Greg Morrisett and Lars Birkedal

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

[PDF |
ICFP06 version |
Project page]

**Abstract Predicates and Mutable ADTs in Hoare Type
Theory**

Aleksandar Nanevski, Amal Ahmed, Greg Morrisett and Lars Birkedal

European Symposium on Programming (ESOP), pages 189-204,
2007.

[PDF |
TR-14-06 |
Project page]

**Polymorphism and Separation in Hoare Type Theory**

Aleksandar Nanevski, Greg Morrisett and Lars Birkedal

International Conference on Functional Programming (ICFP), pages
62-73, 2006.

[PDF |
TR-10-06 |
Project page]

**Inferring Invariants in Separation Logic for Imperative
List-processing Programs**

Stephen Magill, Aleksandar Nanevski, Edmund Clarke and Peter
Lee

Workshop on Semantics, Program Analysis, and Computing Environments for
Memory Management (SPACE), pages 47-60, 2006.

[PDF]

**Dependent Type Theory of Stateful Higher-Order
Functions**

Aleksandar Nanevski and Greg Morrisett

Technical report TR-24-05, Harvard University, 2005.

[PDF |
Extended version |
Project page]

**A Modal Calculus for Exception Handling**

Aleksandar Nanevski

Workshop on Intuitionistic Modal Logic and Applications (IMLA),
2005.

[PDF]

**Staged Computation with Names and Necessity**

Aleksandar Nanevski and Frank Pfenning

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

[PDF]

**Functional Programming with Names and Necessity**

Aleksandar Nanevski

PhD thesis, Carnegie Mellon University, 2004.

[PDF]

**Automatic Generation of Staged Geometric Predicates**

Aleksandar Nanevski, Guy Blelloch and Robert Harper

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

[PDF |
ICFP01 version]

**A Modal Foundation for Meta-Variables**

Aleksandar Nanevski, Brigitte Pientka and Frank Pfenning

Workshop on Mechanized reasoning about languages with variable
binding (MERLIN), pages 159-170, 2003.

[PDF]

**From Dynamic Binding to State via Modal Possibility**

Aleksandar Nanevski

Symposium on Principles and Practice of Declarative Programming
(PPDP), pages 207-218, 2003.

[PDF]

**A Modal Calculus for Effect Handling**

Aleksandar Nanevski

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

[PDF |
Long version |
Short version |
Interpreter]

**Meta-Programming with Names and Necessity**

Aleksandar Nanevski

International Conference on Functional Programming (ICFP), pages
206-217, 2002.

[PDF |
Superseding TR |
Slides]

**Automatic Generation of Staged Geometric Predicates**

Aleksandar Nanevski, Guy Blelloch and Robert Harper

International Conference on Functional Programming (ICFP), pages
217-228, 2001.

[PDF |
Extended version |
Slides]