Aleksandar Nanevski

Publication Activity (10 Years)

Years Active: 2001-2023
Publications (10 Years): 19

Top Topics

Top Venues

Proc. ACM Program. Lang.

Publications

Jesús Domínguez, Aleksandar Nanevski
Declarative Linearizability Proofs for Descriptor-Based Concurrent Helping Algorithms. CoRR (2023)
Jesús Domínguez, Aleksandar Nanevski
Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack. CONCUR (2023)
Jesús Domínguez, Aleksandar Nanevski
Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack: Extended Version. CoRR (2023)
Joakim Öhman, Aleksandar Nanevski
Visibility reasoning for concurrent snapshot algorithms. Proc. ACM Program. Lang. 6 (POPL) (2022)
Nikita Zyuzin, Aleksandar Nanevski
Contextual modal types for algebraic effects and handlers. Proc. ACM Program. Lang. 5 (ICFP) (2021)
Joakim Öhman, Aleksandar Nanevski
Visibility Reasoning for Concurrent Snapshot Algorithms. CoRR (2021)
Nikita Zyuzin, Aleksandar Nanevski
Contextual Modal Types for Algebraic Effects and Handlers. CoRR (2021)
Frantisek Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, Ignacio Fábregas
On algebraic abstractions for concurrent separation logics. Proc. ACM Program. Lang. 5 (POPL) (2021)
Frantisek Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, Ignacio Fábregas
On Algebraic Abstractions for Concurrent Separation Logics. CoRR (2020)
Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, Sharon Shoham
Proving Highly-Concurrent Traversals Correct. CoRR (2020)
Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, Sharon Shoham
Proving highly-concurrent traversals correct. Proc. ACM Program. Lang. 4 (OOPSLA) (2020)
Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, Ignacio Fábregas
Specifying concurrent programs in separation logic: morphisms and simulations. Proc. ACM Program. Lang. 3 (OOPSLA) (2019)
Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, Ignacio Fábregas
Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations. CoRR (2019)
Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
Concurrent Data Structures Linked in Time (Artifact). Dagstuhl Artifacts Ser. 3 (2) (2017)
Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
Concurrent Data Structures Linked in Time. ECOOP (2017)
Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco
Subjective Simulation as a Notion of Morphism for Composing Concurrent Resources. CoRR (2017)
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco
Hoare-style specifications as correctness conditions for non-linearizable concurrent objects. OOPSLA (2016)
Anton Podkopaev, Ilya Sergey, Aleksandar Nanevski
Operational Aspects of C/C++ Concurrency. CoRR (2016)
Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
Concurrent Data Structures Linked in Time. CoRR (2016)
Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis
Mtac: A monad for typed tactic programming in Coq. J. Funct. Program. 25 (2015)
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco
Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects. CoRR (2015)
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. ESOP (2015)
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
Mechanized verification of fine-grained concurrent programs. PLDI (2015)
Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, Germán Andrés Delbianco
Communicating State Transition Systems for Fine-Grained Concurrent Resources. ESOP (2014)
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. CoRR (2014)
Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv
Modular reasoning about heap paths via effectively propositional formulas. POPL (2014)
Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv
Effectively-Propositional Reasoning about Reachability in Linked Data Structures. CAV (2013)
Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer
How to make ad hoc proof automation less ad hoc. J. Funct. Program. 23 (4) (2013)
Gordon Stewart, Anindya Banerjee, Aleksandar Nanevski
Dependent types for enforcement of information flow and erasure policies in heterogeneous data structures. PPDP (2013)
Germán Andrés Delbianco, Aleksandar Nanevski
Hoare-style reasoning with (algebraic) continuations. ICFP (2013)
Murdoch James Gabbay, Aleksandar Nanevski
Denotation of contextual modal type theory (CMTT): Syntax and meta-programming. J. Appl. Log. 11 (1) (2013)
Ruy Ley-Wild, Aleksandar Nanevski
Subjective auxiliary state for coarse-grained concurrency. POPL (2013)
Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis
Mtac: a monad for typed tactic programming in Coq. ICFP (2013)
Aleksandar Nanevski, Anindya Banerjee, Deepak Garg
Dependent Type Theory for Verification of Information Flow and Access Control Policies. ACM Trans. Program. Lang. Syst. 35 (2) (2013)
Murdoch Gabbay, Aleksandar Nanevski
Denotation of syntax and metaprogramming in contextual modal type theory (CMTT) CoRR (2012)
Kasper Svendsen, Lars Birkedal, Aleksandar Nanevski
Partiality, State and Dependent Types. TLCA (2011)
Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer
How to make ad hoc proof automation less ad hoc. ICFP (2011)
Aleksandar Nanevski, Anindya Banerjee, Deepak Garg
Verification of Information Flow and Access Control Policies with Dependent Types. IEEE Symposium on Security and Privacy (2011)
Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine
Structuring the verification of heap-manipulating programs. POPL (2010)
Aleksandar Nanevski, Paul Govereau, Greg Morrisett
Towards type-theoretic semantics for transactional concurrency. TLDI (2009)
Aleksandar Nanevski, Frank Pfenning, Brigitte Pientka
Contextual modal type theory. ACM Trans. Comput. Log. 9 (3) (2008)
Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, Lars Birkedal
Ynot: dependent types for imperative programs. ICFP (2008)
Aleksandar Nanevski, J. Gregory Morrisett, Lars Birkedal
Hoare type theory, polymorphism and separation. J. Funct. Program. 18 (5-6) (2008)
Rasmus Lerchedahl Petersen, Lars Birkedal, Aleksandar Nanevski, Greg Morrisett
A Realizability Model for Impredicative Hoare Type Theory. ESOP (2008)
Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, Lars Birkedal
Abstract Predicates and Mutable ADTs in Hoare Type Theory. ESOP (2007)
Aleksandar Nanevski, Greg Morrisett, Lars Birkedal
Polymorphism and separation in hoare type theory. ICFP (2006)
Aleksandar Nanevski, Frank Pfenning
Staged computation with names and necessity. J. Funct. Program. 15 (5) (2005)
Aleksandar Nanevski
From dynamic binding to state via modal possibility. PPDP (2003)
Aleksandar Nanevski, Guy E. Blelloch, Robert Harper
Automatic Generation of Staged Geometric Predicates. High. Order Symb. Comput. 16 (4) (2003)
Aleksandar Nanevski, Brigitte Pientka, Frank Pfenning
A modal foundation for meta-variables. MERLIN (2003)
Aleksandar Nanevski
Meta-programming with names and necessity. ICFP (2002)
Aleksandar Nanevski, Guy E. Blelloch, Robert Harper
Automatic Generation of Staged Geometric Predicates. ICFP (2001)