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.
Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack Jesús Domínguez and Aleksandar Nanevski International Conference on Concurrency Theory (CONCUR), 2023. [pdf | doi | extended version]
Declarative Linearizability Proofs for Descriptor-Based Concurrent Helping Algorithms Jesús Domínguez and Aleksandar Nanevski [arxiv]
Visibility Reasoning for Concurrent Snapshot Algorithms Joakim Öhman and Aleksandar Nanevski Symposium on Principles of Programming Languages (POPL), 2022. [pdf | doi | extended version]
Contextual Modal Types for Algebraic Effects and Handlers Nikita Zyuzin and Aleksandar Nanevski International Conference on Functional Programming (ICFP), 2021. [pdf | doi | extended version]
On Algebraic Abstractions for Concurrent Separation Logics František Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco and Ignacio Fábregas Symposium on Principles of Programming Languages (POPL), 2021. [pdf | doi | extended version | project page]
Proving Highly-Concurrent Traversals Correct Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky and Sharon Shoham International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 128:1--128:29, 2020. [pdf | doi]
Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco and Ignacio Fábregas International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 161:1-161:30, 2019. [pdf | doi | extended version | project page]
Concurrent Data Structures Linked in Time Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski and Anindya Banerjee European Conference on Object-Oriented Programming (ECOOP), pages 8:1-8:30, 2017 [pdf | doi | project page]
Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee and Germán Andrés Delbianco International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 92-110, 2016. [pdf | doi | project page]
Separation Logic and Concurrency Aleksandar Nanevski Lecture notes for Oregon Programming Languages Summer School (OPLSS), June 2016. [pdf | oplss16 page]
Operational Aspects of C/C++ Concurrency Anton Podkopaev, Ilya Sergey and Aleksandar Nanevski [arxiv]
Mtac: A Monad for Typed Tactic Programming in Coq Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski and Viktor Vafeiadis Journal of Functional Programming (JFP), April 2015. [pdf | doi | 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 |
doi |
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 |
doi |
extended version |
project page]
Communicating State Transition Systems for Fine-Grained
Concurrent Resources
Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey and Germán Andrés Delbianco
European Symposium on Programming (ESOP), pages 290-310, 2014.
[pdf |
doi |
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 |
doi]
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 |
doi |
coq sources |
project page]
Hoare-Style Reasoning with (Algebraic) Continuations Germán Andrés Delbianco and Aleksandar Nanevski International Conference on Functional Programming (ICFP), pages 363-376, 2013. [pdf | doi | ]
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 | doi | 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 |
doi]
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 |
doi |
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 |
doi |
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 |
doi |
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 |
doi]
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 |
doi |
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 |
doi |
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 |
doi |
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 |
doi |
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 |
doi |
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 |
doi |
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 |
doi |
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 |
doi]
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 |
doi |
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 |
doi |
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 |
doi |
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 |
doi]
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 |
doi |
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 |
doi]
From Dynamic Binding to State via Modal Possibility
Aleksandar Nanevski
Symposium on Principles and Practice of Declarative Programming
(PPDP), pages 207-218, 2003.
[pdf |
doi]
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 |
doi |
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 |
doi |
extended version |
slides]