Aleksandar Nanevski

According to our database, Aleksandar Nanevski authored at least 41 papers between 2002 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2023

Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack: Extended Version.

Jesús Domínguez, Aleksandar Nanevski

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

Jesús Domínguez, Aleksandar Nanevski

Proceedings of the 34th International Conference on Concurrency Theory, 2023

2022

Visibility reasoning for concurrent snapshot algorithms.

Joakim Öhman, Aleksandar Nanevski

Proc. ACM Program. Lang., 2022

2021

Contextual modal types for algebraic effects and handlers.

Nikita Zyuzin, Aleksandar Nanevski

Proc. ACM Program. Lang., 2021

On algebraic abstractions for concurrent separation logics.

Frantisek Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, Ignacio Fábregas

Proc. ACM Program. Lang., 2021

2020

Proving highly-concurrent traversals correct.

Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, Sharon Shoham

Proc. ACM Program. Lang., 2020

2019

Specifying concurrent programs in separation logic: morphisms and simulations.

Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, Ignacio Fábregas

Proc. ACM Program. Lang., 2019

2017

Concurrent Data Structures Linked in Time (Artifact).

Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee

Dagstuhl Artifacts Ser., 2017

Subjective Simulation as a Notion of Morphism for Composing Concurrent Resources.

Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco

CoRR, 2017

Concurrent Data Structures Linked in Time.

Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee

Proceedings of the 31st European Conference on Object-Oriented Programming, 2017

2016

Operational Aspects of C/C++ Concurrency.

Anton Podkopaev, Ilya Sergey, Aleksandar Nanevski

CoRR, 2016

Hoare-style specifications as correctness conditions for non-linearizable concurrent objects.

Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco

Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, 2016

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

Mechanized verification of fine-grained concurrent programs.

Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee

Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity.

Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee

Proceedings of the Programming Languages and Systems, 2015

2014

Modular reasoning about heap paths via effectively propositional formulas.

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

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Communicating State Transition Systems for Fine-Grained Concurrent Resources.

Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, Germán Andrés Delbianco

Proceedings of the Programming Languages and Systems, 2014

2013

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

Aleksandar Nanevski, Anindya Banerjee, Deepak Garg

ACM Trans. Program. Lang. Syst., 2013

How to make ad hoc proof automation less ad hoc.

Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer

J. Funct. Program., 2013

Denotation of contextual modal type theory (CMTT): Syntax and meta-programming.

Murdoch James Gabbay, Aleksandar Nanevski

J. Appl. Log., 2013

Dependent types for enforcement of information flow and erasure policies in heterogeneous data structures.

Gordon Stewart, Anindya Banerjee, Aleksandar Nanevski

Proceedings of the 15th International Symposium on Principles and Practice of Declarative Programming, 2013

Subjective auxiliary state for coarse-grained concurrency.

Ruy Ley-Wild, Aleksandar Nanevski

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

Hoare-style reasoning with (algebraic) continuations.

Germán Andrés Delbianco, Aleksandar Nanevski

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2013

Effectively-Propositional Reasoning about Reachability in Linked Data Structures.

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

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

2012

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

Murdoch Gabbay, Aleksandar Nanevski

CoRR, 2012

2011

Partiality, State and Dependent Types.

Kasper Svendsen, Lars Birkedal, Aleksandar Nanevski

Proceedings of the Typed Lambda Calculi and Applications - 10th International Conference, 2011

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

Aleksandar Nanevski, Anindya Banerjee, Deepak Garg

Proceedings of the 32nd IEEE Symposium on Security and Privacy, 2011

2010

Structuring the verification of heap-manipulating programs.

Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine

Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

2009

Towards type-theoretic semantics for transactional concurrency.

Aleksandar Nanevski, Paul Govereau, Greg Morrisett

Proceedings of TLDI'09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2009

2008

Contextual modal type theory.

Aleksandar Nanevski, Frank Pfenning, Brigitte Pientka

ACM Trans. Comput. Log., 2008

Hoare type theory, polymorphism and separation.

Aleksandar Nanevski, J. Gregory Morrisett, Lars Birkedal

J. Funct. Program., 2008

Ynot: dependent types for imperative programs.

Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, Lars Birkedal

Proceedings of the Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, 2008

A Realizability Model for Impredicative Hoare Type Theory.

Rasmus Lerchedahl Petersen, Lars Birkedal, Aleksandar Nanevski, Greg Morrisett

Proceedings of the Programming Languages and Systems, 2008

2007

Abstract Predicates and Mutable ADTs in Hoare Type Theory.

Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, Lars Birkedal

Proceedings of the Programming Languages and Systems, 2007

2006

Polymorphism and separation in hoare type theory.

Aleksandar Nanevski, Greg Morrisett, Lars Birkedal

Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, 2006

2005

Staged computation with names and necessity.

Aleksandar Nanevski, Frank Pfenning

J. Funct. Program., 2005

2003

Automatic Generation of Staged Geometric Predicates.

Aleksandar Nanevski, Guy E. Blelloch, Robert Harper

High. Order Symb. Comput., 2003

From dynamic binding to state via modal possibility.

Aleksandar Nanevski

Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2003

A modal foundation for meta-variables.

Aleksandar Nanevski, Brigitte Pientka, Frank Pfenning

Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, 2003

2002

Meta-programming with names and necessity.

Aleksandar Nanevski

Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02), 2002