Meta-programming with names and necessity. - Aleksandar Nanevski (ICFP, 2002)

A modal foundation for meta-variables. - Aleksandar Nanevski; Brigitte Pientka; Frank Pfenning (MERLIN, 2003)

From dynamic binding to state via modal possibility. - Aleksandar Nanevski (PPDP, 2003)

Automatic Generation of Staged Geometric Predicates. - Aleksandar Nanevski; Guy E. Blelloch; Robert Harper 001 (High. Order Symb. Comput., 2003)

Staged computation with names and necessity. - Aleksandar Nanevski; Frank Pfenning (J. Funct. Program., 2005)

Polymorphism and separation in hoare type theory. - Aleksandar Nanevski; Greg Morrisett; Lars Birkedal (ICFP, 2006)

Abstract Predicates and Mutable ADTs in Hoare Type Theory. - Aleksandar Nanevski; Amal Ahmed 001; Greg Morrisett; Lars Birkedal (ESOP, 2007)

A Realizability Model for Impredicative Hoare Type Theory. - Rasmus Lerchedahl Petersen; Lars Birkedal; Aleksandar Nanevski; Greg Morrisett (ESOP, 2008)

Ynot: dependent types for imperative programs. - Aleksandar Nanevski; Greg Morrisett; Avraham Shinnar; Paul Govereau; Lars Birkedal (ICFP, 2008)

Hoare type theory, polymorphism and separation. - Aleksandar Nanevski; J. Gregory Morrisett; Lars Birkedal (J. Funct. Program., 2008)

Contextual modal type theory. - Aleksandar Nanevski; Frank Pfenning; Brigitte Pientka (ACM Trans. Comput. Log., 2008)

Towards type-theoretic semantics for transactional concurrency. - Aleksandar Nanevski; Paul Govereau; Greg Morrisett (TLDI, 2009)

Structuring the verification of heap-manipulating programs. - Aleksandar Nanevski; Viktor Vafeiadis; Josh Berdine (POPL, 2010)

Verification of Information Flow and Access Control Policies with Dependent Types. - Aleksandar Nanevski; Anindya Banerjee 001; Deepak Garg 001 (IEEE Symposium on Security and Privacy, 2011)

Partiality, State and Dependent Types. - Kasper Svendsen; Lars Birkedal; Aleksandar Nanevski (TLCA, 2011)

Denotation of syntax and metaprogramming in contextual modal type theory (CMTT) - Murdoch Gabbay; Aleksandar Nanevski (CoRR, 2012)

Effectively-Propositional Reasoning about Reachability in Linked Data Structures. - Shachar Itzhaky; Anindya Banerjee 001; Neil Immerman; Aleksandar Nanevski; Mooly Sagiv (CAV, 2013)

Hoare-style reasoning with (algebraic) continuations. - Germán Andrés Delbianco; Aleksandar Nanevski (ICFP, 2013)

Subjective auxiliary state for coarse-grained concurrency. - Ruy Ley-Wild; Aleksandar Nanevski (POPL, 2013)

Dependent types for enforcement of information flow and erasure policies in heterogeneous data structures. - Gordon Stewart 001; Anindya Banerjee 001; Aleksandar Nanevski (PPDP, 2013)

Denotation of contextual modal type theory (CMTT): Syntax and meta-programming. - Murdoch James Gabbay; Aleksandar Nanevski (J. Appl. Log., 2013)

How to make ad hoc proof automation less ad hoc. - Georges Gonthier; Beta Ziliani; Aleksandar Nanevski; Derek Dreyer (J. Funct. Program., 2013)

Dependent Type Theory for Verification of Information Flow and Access Control Policies. - Aleksandar Nanevski; Anindya Banerjee 001; Deepak Garg 001 (ACM Trans. Program. Lang. Syst., 2013)

Communicating State Transition Systems for Fine-Grained Concurrent Resources. - Aleksandar Nanevski; Ruy Ley-Wild; Ilya Sergey; Germán Andrés Delbianco (ESOP, 2014)

Modular reasoning about heap paths via effectively propositional formulas. - Shachar Itzhaky; Anindya Banerjee 001; Neil Immerman; Ori Lahav 001; Aleksandar Nanevski; Mooly Sagiv (POPL, 2014)

Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. - Ilya Sergey; Aleksandar Nanevski; Anindya Banerjee 001 (ESOP, 2015)

Mechanized verification of fine-grained concurrent programs. - Ilya Sergey; Aleksandar Nanevski; Anindya Banerjee 001 (PLDI, 2015)

Mtac: A monad for typed tactic programming in Coq. - Beta Ziliani; Derek Dreyer; Neelakantan R. Krishnaswami; Aleksandar Nanevski; Viktor Vafeiadis (J. Funct. Program., 2015)

Hoare-style specifications as correctness conditions for non-linearizable concurrent objects. - Ilya Sergey; Aleksandar Nanevski; Anindya Banerjee 001; Germán Andrés Delbianco (OOPSLA, 2016)

Operational Aspects of C/C++ Concurrency. - Anton Podkopaev; Ilya Sergey; Aleksandar Nanevski (CoRR, 2016)

Concurrent Data Structures Linked in Time. - Germán Andrés Delbianco; Ilya Sergey; Aleksandar Nanevski; Anindya Banerjee 001 (ECOOP, 2017)

Subjective Simulation as a Notion of Morphism for Composing Concurrent Resources. - Aleksandar Nanevski; Anindya Banerjee 001; Germán Andrés Delbianco (CoRR, 2017)

Concurrent Data Structures Linked in Time (Artifact). - Germán Andrés Delbianco; Ilya Sergey; Aleksandar Nanevski; Anindya Banerjee 001 (Dagstuhl Artifacts Ser., 2017)

Specifying concurrent programs in separation logic: morphisms and simulations. - Aleksandar Nanevski; Anindya Banerjee 001; Germán Andrés Delbianco; Ignacio Fábregas (Proc. ACM Program. Lang., 2019)

Proving highly-concurrent traversals correct. - Yotam M. Y. Feldman; Artem Khyzha; Constantin Enea; Adam Morrison 001; Aleksandar Nanevski; Noam Rinetzky; Sharon Shoham (Proc. ACM Program. Lang., 2020)

On algebraic abstractions for concurrent separation logics. - Frantisek Farka; Aleksandar Nanevski; Anindya Banerjee 001; Germán Andrés Delbianco; Ignacio Fábregas (Proc. ACM Program. Lang., 2021)

Contextual modal types for algebraic effects and handlers. - Nikita Zyuzin; Aleksandar Nanevski (Proc. ACM Program. Lang., 2021)

Visibility reasoning for concurrent snapshot algorithms. - Joakim Öhman; Aleksandar Nanevski (Proc. ACM Program. Lang., 2022)

Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack. - Jesús Domínguez; Aleksandar Nanevski (CONCUR, 2023)

Declarative Linearizability Proofs for Descriptor-Based Concurrent Helping Algorithms. - Jesús Domínguez; Aleksandar Nanevski (CoRR, 2023)

Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack: Extended Version. - Jesús Domínguez; Aleksandar Nanevski (CoRR, 2023)

Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version). - Marcos Grandury; Aleksandar Nanevski; Alexander Gryzlov (CoRR, 2025)