default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDAleksandar Nanevski
Person information
- affiliation: Edificio IMDEA Software, Madrid, Spain
- affiliation (former): Harvard University, Cambridge, MA, USA
- affiliation (former): Carnegie Mellon University, Pittsburgh, PA, USA
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
Journal Articles
- 2022
[j14]Joakim Öhman
, Aleksandar Nanevski:
Visibility reasoning for concurrent snapshot algorithms. Proc. ACM Program. Lang. 6(POPL): 1-30 (2022)- 2021
- [j13]Nikita Zyuzin, Aleksandar Nanevski:
Contextual modal types for algebraic effects and handlers. Proc. ACM Program. Lang. 5(ICFP): 1-29 (2021) - [j12]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): 1-32 (2021) - 2020
- [j11]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): 128:1-128:29 (2020) - 2019
- [j10]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): 161:1-161:30 (2019) - 2017
- [j9]Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee:
Concurrent Data Structures Linked in Time (Artifact). Dagstuhl Artifacts Ser. 3(2): 04:1-04:4 (2017) - 2015
- [j8]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) - 2013
- [j7]Murdoch James Gabbay, Aleksandar Nanevski:
Denotation of contextual modal type theory (CMTT): Syntax and meta-programming. J. Appl. Log. 11(1): 1-29 (2013) - [j6]Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer:
How to make ad hoc proof automation less ad hoc. J. Funct. Program. 23(4): 357-401 (2013) - [j5]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): 6:1-6:41 (2013) - 2008
- [j4]Aleksandar Nanevski, J. Gregory Morrisett, Lars Birkedal:
Hoare type theory, polymorphism and separation. J. Funct. Program. 18(5-6): 865-911 (2008) - [j3]Aleksandar Nanevski, Frank Pfenning, Brigitte Pientka:
Contextual modal type theory. ACM Trans. Comput. Log. 9(3): 23:1-23:49 (2008) - 2005
- [j2]Aleksandar Nanevski, Frank Pfenning:
Staged computation with names and necessity. J. Funct. Program. 15(5): 893-939 (2005) - 2003
- [j1]Aleksandar Nanevski, Guy E. Blelloch, Robert Harper:
Automatic Generation of Staged Geometric Predicates. High. Order Symb. Comput. 16(4): 379-400 (2003)
Conference and Workshop Papers
- 2023
- [c25]Jesús Domínguez, Aleksandar Nanevski:
Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack. CONCUR 2023: 30:1-30:16 - 2017
- [c24]Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee:
Concurrent Data Structures Linked in Time. ECOOP 2017: 8:1-8:30 - 2016
- [c23]Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco:
Hoare-style specifications as correctness conditions for non-linearizable concurrent objects. OOPSLA 2016: 92-110 - 2015
- [c22]Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee:
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. ESOP 2015: 333-358 - [c21]Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee:
Mechanized verification of fine-grained concurrent programs. PLDI 2015: 77-87 - 2014
- [c20]Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, Germán Andrés Delbianco:
Communicating State Transition Systems for Fine-Grained Concurrent Resources. ESOP 2014: 290-310 - [c19]Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv:
Modular reasoning about heap paths via effectively propositional formulas. POPL 2014: 385-396 - 2013
- [c18]Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv:
Effectively-Propositional Reasoning about Reachability in Linked Data Structures. CAV 2013: 756-772 - [c17]Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis:
Mtac: a monad for typed tactic programming in Coq. ICFP 2013: 87-100 - [c16]Germán Andrés Delbianco, Aleksandar Nanevski:
Hoare-style reasoning with (algebraic) continuations. ICFP 2013: 363-376 - [c15]Ruy Ley-Wild, Aleksandar Nanevski:
Subjective auxiliary state for coarse-grained concurrency. POPL 2013: 561-574 - [c14]Gordon Stewart, Anindya Banerjee, Aleksandar Nanevski:
Dependent types for enforcement of information flow and erasure policies in heterogeneous data structures. PPDP 2013: 145-156 - 2011
- [c13]Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer:
How to make ad hoc proof automation less ad hoc. ICFP 2011: 163-175 - [c12]Aleksandar Nanevski, Anindya Banerjee, Deepak Garg:
Verification of Information Flow and Access Control Policies with Dependent Types. IEEE Symposium on Security and Privacy 2011: 165-179 - [c11]Kasper Svendsen, Lars Birkedal, Aleksandar Nanevski:
Partiality, State and Dependent Types. TLCA 2011: 198-212 - 2010
- [c10]Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine:
Structuring the verification of heap-manipulating programs. POPL 2010: 261-274 - 2009
- [c9]Aleksandar Nanevski, Paul Govereau, Greg Morrisett:
Towards type-theoretic semantics for transactional concurrency. TLDI 2009: 79-90 - 2008
- [c8]Rasmus Lerchedahl Petersen, Lars Birkedal, Aleksandar Nanevski, Greg Morrisett:
A Realizability Model for Impredicative Hoare Type Theory. ESOP 2008: 337-352 - [c7]Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, Lars Birkedal:
Ynot: dependent types for imperative programs. ICFP 2008: 229-240 - 2007
- [c6]Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, Lars Birkedal:
Abstract Predicates and Mutable ADTs in Hoare Type Theory. ESOP 2007: 189-204 - 2006
- [c5]Aleksandar Nanevski, Greg Morrisett, Lars Birkedal:
Polymorphism and separation in hoare type theory. ICFP 2006: 62-73 - 2003
- [c4]Aleksandar Nanevski, Brigitte Pientka, Frank Pfenning:
A modal foundation for meta-variables. MERLIN 2003 - [c3]Aleksandar Nanevski:
From dynamic binding to state via modal possibility. PPDP 2003: 207-218 - 2002
- [c2]Aleksandar Nanevski:
Meta-programming with names and necessity. ICFP 2002: 206-217 - 2001
- [c1]Aleksandar Nanevski, Guy E. Blelloch, Robert Harper:
Automatic Generation of Staged Geometric Predicates. ICFP 2001: 217-228
Informal and Other Publications
- 2023
- [i13]Jesús Domínguez, Aleksandar Nanevski:
Declarative Linearizability Proofs for Descriptor-Based Concurrent Helping Algorithms. CoRR abs/2307.04653 (2023) - [i12]Jesús Domínguez, Aleksandar Nanevski:
Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack: Extended Version. CoRR abs/2307.04720 (2023) - 2021
- [i11]Nikita Zyuzin, Aleksandar Nanevski:
Contextual Modal Types for Algebraic Effects and Handlers. CoRR abs/2103.02976 (2021) - [i10]Joakim Öhman, Aleksandar Nanevski:
Visibility Reasoning for Concurrent Snapshot Algorithms. CoRR abs/2110.02769 (2021) - 2020
- [i9]Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, Sharon Shoham:
Proving Highly-Concurrent Traversals Correct. CoRR abs/2010.00911 (2020) - [i8]Frantisek Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, Ignacio Fábregas:
On Algebraic Abstractions for Concurrent Separation Logics. CoRR abs/2010.12686 (2020) - 2019
- [i7]Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, Ignacio Fábregas:
Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations. CoRR abs/1904.07136 (2019) - 2017
- [i6]Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco:
Subjective Simulation as a Notion of Morphism for Composing Concurrent Resources. CoRR abs/1709.07741 (2017) - 2016
- [i5]Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee:
Concurrent Data Structures Linked in Time. CoRR abs/1604.08080 (2016) - [i4]Anton Podkopaev, Ilya Sergey, Aleksandar Nanevski:
Operational Aspects of C/C++ Concurrency. CoRR abs/1606.01400 (2016) - 2015
- [i3]Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco:
Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects. CoRR abs/1509.06220 (2015) - 2014
- [i2]Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee:
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. CoRR abs/1410.0306 (2014) - 2012
- [i1]Murdoch Gabbay, Aleksandar Nanevski:
Denotation of syntax and metaprogramming in contextual modal type theory (CMTT). CoRR abs/1202.0904 (2012)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2025-01-21 00:15 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
