Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDBibTeX records: Aleksandar Nanevski
@inproceedings{DBLP:conf/concur/DominguezN23,
author = {Jes{\'{u}}s Dom{\'{\i}}nguez and
Aleksandar Nanevski},
editor = {Guillermo A. P{\'{e}}rez and
Jean{-}Fran{\c{c}}ois Raskin},
title = {Visibility and Separability for a Declarative Linearizability Proof
of the Timestamped Stack},
booktitle = {34th International Conference on Concurrency Theory, {CONCUR} 2023,
September 18-23, 2023, Antwerp, Belgium},
series = {LIPIcs},
volume = {279},
pages = {30:1--30:16},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2023},
url = {https://doi.org/10.4230/LIPIcs.CONCUR.2023.30},
doi = {10.4230/LIPICS.CONCUR.2023.30},
timestamp = {Sat, 09 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/concur/DominguezN23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2307-04653,
author = {Jes{\'{u}}s Dom{\'{\i}}nguez and
Aleksandar Nanevski},
title = {Declarative Linearizability Proofs for Descriptor-Based Concurrent
Helping Algorithms},
journal = {CoRR},
volume = {abs/2307.04653},
year = {2023},
url = {https://doi.org/10.48550/arXiv.2307.04653},
doi = {10.48550/ARXIV.2307.04653},
eprinttype = {arXiv},
eprint = {2307.04653},
timestamp = {Mon, 24 Jul 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2307-04653.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2307-04720,
author = {Jes{\'{u}}s Dom{\'{\i}}nguez and
Aleksandar Nanevski},
title = {Visibility and Separability for a Declarative Linearizability Proof
of the Timestamped Stack: Extended Version},
journal = {CoRR},
volume = {abs/2307.04720},
year = {2023},
url = {https://doi.org/10.48550/arXiv.2307.04720},
doi = {10.48550/ARXIV.2307.04720},
eprinttype = {arXiv},
eprint = {2307.04720},
timestamp = {Mon, 24 Jul 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2307-04720.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/pacmpl/OhmanN22,
author = {Joakim {\"{O}}hman and
Aleksandar Nanevski},
title = {Visibility reasoning for concurrent snapshot algorithms},
journal = {Proc. {ACM} Program. Lang.},
volume = {6},
number = {{POPL}},
pages = {1--30},
year = {2022},
url = {https://doi.org/10.1145/3498694},
doi = {10.1145/3498694},
timestamp = {Mon, 05 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/pacmpl/OhmanN22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/pacmpl/ZyuzinN21,
author = {Nikita Zyuzin and
Aleksandar Nanevski},
title = {Contextual modal types for algebraic effects and handlers},
journal = {Proc. {ACM} Program. Lang.},
volume = {5},
number = {{ICFP}},
pages = {1--29},
year = {2021},
url = {https://doi.org/10.1145/3473580},
doi = {10.1145/3473580},
timestamp = {Sat, 08 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/pacmpl/ZyuzinN21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/pacmpl/FarkaN0DF21,
author = {Frantisek Farka and
Aleksandar Nanevski and
Anindya Banerjee and
Germ{\'{a}}n Andr{\'{e}}s Delbianco and
Ignacio F{\'{a}}bregas},
title = {On algebraic abstractions for concurrent separation logics},
journal = {Proc. {ACM} Program. Lang.},
volume = {5},
number = {{POPL}},
pages = {1--32},
year = {2021},
url = {https://doi.org/10.1145/3434286},
doi = {10.1145/3434286},
timestamp = {Sat, 08 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/pacmpl/FarkaN0DF21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2103-02976,
author = {Nikita Zyuzin and
Aleksandar Nanevski},
title = {Contextual Modal Types for Algebraic Effects and Handlers},
journal = {CoRR},
volume = {abs/2103.02976},
year = {2021},
url = {https://arxiv.org/abs/2103.02976},
eprinttype = {arXiv},
eprint = {2103.02976},
timestamp = {Mon, 15 Mar 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2103-02976.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2110-02769,
author = {Joakim {\"{O}}hman and
Aleksandar Nanevski},
title = {Visibility Reasoning for Concurrent Snapshot Algorithms},
journal = {CoRR},
volume = {abs/2110.02769},
year = {2021},
url = {https://arxiv.org/abs/2110.02769},
eprinttype = {arXiv},
eprint = {2110.02769},
timestamp = {Thu, 21 Oct 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2110-02769.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/pacmpl/FeldmanKE0NRS20,
author = {Yotam M. Y. Feldman and
Artem Khyzha and
Constantin Enea and
Adam Morrison and
Aleksandar Nanevski and
Noam Rinetzky and
Sharon Shoham},
title = {Proving highly-concurrent traversals correct},
journal = {Proc. {ACM} Program. Lang.},
volume = {4},
number = {{OOPSLA}},
pages = {128:1--128:29},
year = {2020},
url = {https://doi.org/10.1145/3428196},
doi = {10.1145/3428196},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/pacmpl/FeldmanKE0NRS20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2010-00911,
author = {Yotam M. Y. Feldman and
Artem Khyzha and
Constantin Enea and
Adam Morrison and
Aleksandar Nanevski and
Noam Rinetzky and
Sharon Shoham},
title = {Proving Highly-Concurrent Traversals Correct},
journal = {CoRR},
volume = {abs/2010.00911},
year = {2020},
url = {https://arxiv.org/abs/2010.00911},
eprinttype = {arXiv},
eprint = {2010.00911},
timestamp = {Mon, 12 Oct 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2010-00911.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2010-12686,
author = {Frantisek Farka and
Aleksandar Nanevski and
Anindya Banerjee and
Germ{\'{a}}n Andr{\'{e}}s Delbianco and
Ignacio F{\'{a}}bregas},
title = {On Algebraic Abstractions for Concurrent Separation Logics},
journal = {CoRR},
volume = {abs/2010.12686},
year = {2020},
url = {https://arxiv.org/abs/2010.12686},
eprinttype = {arXiv},
eprint = {2010.12686},
timestamp = {Mon, 02 Nov 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2010-12686.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/pacmpl/Nanevski0DF19,
author = {Aleksandar Nanevski and
Anindya Banerjee and
Germ{\'{a}}n Andr{\'{e}}s Delbianco and
Ignacio F{\'{a}}bregas},
title = {Specifying concurrent programs in separation logic: morphisms and
simulations},
journal = {Proc. {ACM} Program. Lang.},
volume = {3},
number = {{OOPSLA}},
pages = {161:1--161:30},
year = {2019},
url = {https://doi.org/10.1145/3360587},
doi = {10.1145/3360587},
timestamp = {Mon, 05 Feb 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/pacmpl/Nanevski0DF19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1904-07136,
author = {Aleksandar Nanevski and
Anindya Banerjee and
Germ{\'{a}}n Andr{\'{e}}s Delbianco and
Ignacio F{\'{a}}bregas},
title = {Specifying Concurrent Programs in Separation Logic: Morphisms and
Simulations},
journal = {CoRR},
volume = {abs/1904.07136},
year = {2019},
url = {http://arxiv.org/abs/1904.07136},
eprinttype = {arXiv},
eprint = {1904.07136},
timestamp = {Sat, 23 Jan 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-1904-07136.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/darts/DelbiancoSNB17,
author = {Germ{\'{a}}n Andr{\'{e}}s Delbianco and
Ilya Sergey and
Aleksandar Nanevski and
Anindya Banerjee},
title = {Concurrent Data Structures Linked in Time (Artifact)},
journal = {Dagstuhl Artifacts Ser.},
volume = {3},
number = {2},
pages = {04:1--04:4},
year = {2017},
url = {https://doi.org/10.4230/DARTS.3.2.4},
doi = {10.4230/DARTS.3.2.4},
timestamp = {Tue, 01 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/darts/DelbiancoSNB17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ecoop/DelbiancoSNB17,
author = {Germ{\'{a}}n Andr{\'{e}}s Delbianco and
Ilya Sergey and
Aleksandar Nanevski and
Anindya Banerjee},
editor = {Peter M{\"{u}}ller},
title = {Concurrent Data Structures Linked in Time},
booktitle = {31st European Conference on Object-Oriented Programming, {ECOOP} 2017,
June 19-23, 2017, Barcelona, Spain},
series = {LIPIcs},
volume = {74},
pages = {8:1--8:30},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2017},
url = {https://doi.org/10.4230/LIPIcs.ECOOP.2017.8},
doi = {10.4230/LIPICS.ECOOP.2017.8},
timestamp = {Tue, 21 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/ecoop/DelbiancoSNB17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1709-07741,
author = {Aleksandar Nanevski and
Anindya Banerjee and
Germ{\'{a}}n Andr{\'{e}}s Delbianco},
title = {Subjective Simulation as a Notion of Morphism for Composing Concurrent
Resources},
journal = {CoRR},
volume = {abs/1709.07741},
year = {2017},
url = {http://arxiv.org/abs/1709.07741},
eprinttype = {arXiv},
eprint = {1709.07741},
timestamp = {Sat, 23 Jan 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-1709-07741.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/oopsla/SergeyNBD16,
author = {Ilya Sergey and
Aleksandar Nanevski and
Anindya Banerjee and
Germ{\'{a}}n Andr{\'{e}}s Delbianco},
editor = {Eelco Visser and
Yannis Smaragdakis},
title = {Hoare-style specifications as correctness conditions for non-linearizable
concurrent objects},
booktitle = {Proceedings of the 2016 {ACM} {SIGPLAN} International Conference on
Object-Oriented Programming, Systems, Languages, and Applications,
{OOPSLA} 2016, part of {SPLASH} 2016, Amsterdam, The Netherlands,
October 30 - November 4, 2016},
pages = {92--110},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2983990.2983999},
doi = {10.1145/2983990.2983999},
timestamp = {Tue, 21 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/oopsla/SergeyNBD16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/DelbiancoSNB16,
author = {Germ{\'{a}}n Andr{\'{e}}s Delbianco and
Ilya Sergey and
Aleksandar Nanevski and
Anindya Banerjee},
title = {Concurrent Data Structures Linked in Time},
journal = {CoRR},
volume = {abs/1604.08080},
year = {2016},
url = {http://arxiv.org/abs/1604.08080},
eprinttype = {arXiv},
eprint = {1604.08080},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/DelbiancoSNB16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/PodkopaevSN16,
author = {Anton Podkopaev and
Ilya Sergey and
Aleksandar Nanevski},
title = {Operational Aspects of {C/C++} Concurrency},
journal = {CoRR},
volume = {abs/1606.01400},
year = {2016},
url = {http://arxiv.org/abs/1606.01400},
eprinttype = {arXiv},
eprint = {1606.01400},
timestamp = {Tue, 17 Sep 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/PodkopaevSN16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfp/ZilianiDKNV15,
author = {Beta Ziliani and
Derek Dreyer and
Neelakantan R. Krishnaswami and
Aleksandar Nanevski and
Viktor Vafeiadis},
title = {Mtac: {A} monad for typed tactic programming in Coq},
journal = {J. Funct. Program.},
volume = {25},
year = {2015},
url = {https://doi.org/10.1017/S0956796815000118},
doi = {10.1017/S0956796815000118},
timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jfp/ZilianiDKNV15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/esop/SergeyNB15,
author = {Ilya Sergey and
Aleksandar Nanevski and
Anindya Banerjee},
editor = {Jan Vitek},
title = {Specifying and Verifying Concurrent Algorithms with Histories and
Subjectivity},
booktitle = {Programming Languages and Systems - 24th European Symposium on Programming,
{ESOP} 2015, Held as Part of the European Joint Conferences on Theory
and Practice of Software, {ETAPS} 2015, London, UK, April 11-18, 2015.
Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9032},
pages = {333--358},
publisher = {Springer},
year = {2015},
url = {https://doi.org/10.1007/978-3-662-46669-8\_14},
doi = {10.1007/978-3-662-46669-8\_14},
timestamp = {Tue, 20 Aug 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/esop/SergeyNB15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/pldi/SergeyNB15,
author = {Ilya Sergey and
Aleksandar Nanevski and
Anindya Banerjee},
editor = {David Grove and
Stephen M. Blackburn},
title = {Mechanized verification of fine-grained concurrent programs},
booktitle = {Proceedings of the 36th {ACM} {SIGPLAN} Conference on Programming
Language Design and Implementation, Portland, OR, USA, June 15-17,
2015},
pages = {77--87},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2737924.2737964},
doi = {10.1145/2737924.2737964},
timestamp = {Tue, 21 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/pldi/SergeyNB15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/SergeyNBD15,
author = {Ilya Sergey and
Aleksandar Nanevski and
Anindya Banerjee and
Germ{\'{a}}n Andr{\'{e}}s Delbianco},
title = {Hoare-style Specifications as Correctness Conditions for Non-linearizable
Concurrent Objects},
journal = {CoRR},
volume = {abs/1509.06220},
year = {2015},
url = {http://arxiv.org/abs/1509.06220},
eprinttype = {arXiv},
eprint = {1509.06220},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/SergeyNBD15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/esop/NanevskiLSD14,
author = {Aleksandar Nanevski and
Ruy Ley{-}Wild and
Ilya Sergey and
Germ{\'{a}}n Andr{\'{e}}s Delbianco},
editor = {Zhong Shao},
title = {Communicating State Transition Systems for Fine-Grained Concurrent
Resources},
booktitle = {Programming Languages and Systems - 23rd European Symposium on Programming,
{ESOP} 2014, Held as Part of the European Joint Conferences on Theory
and Practice of Software, {ETAPS} 2014, Grenoble, France, April 5-13,
2014, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8410},
pages = {290--310},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-642-54833-8\_16},
doi = {10.1007/978-3-642-54833-8\_16},
timestamp = {Thu, 14 Oct 2021 10:31:33 +0200},
biburl = {https://dblp.org/rec/conf/esop/NanevskiLSD14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/popl/ItzhakyBILNS14,
author = {Shachar Itzhaky and
Anindya Banerjee and
Neil Immerman and
Ori Lahav and
Aleksandar Nanevski and
Mooly Sagiv},
editor = {Suresh Jagannathan and
Peter Sewell},
title = {Modular reasoning about heap paths via effectively propositional formulas},
booktitle = {The 41st Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of
Programming Languages, {POPL} '14, San Diego, CA, USA, January 20-21,
2014},
pages = {385--396},
publisher = {{ACM}},
year = {2014},
url = {https://doi.org/10.1145/2535838.2535854},
doi = {10.1145/2535838.2535854},
timestamp = {Fri, 22 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/popl/ItzhakyBILNS14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/SergeyNB14,
author = {Ilya Sergey and
Aleksandar Nanevski and
Anindya Banerjee},
title = {Specifying and Verifying Concurrent Algorithms with Histories and
Subjectivity},
journal = {CoRR},
volume = {abs/1410.0306},
year = {2014},
url = {http://arxiv.org/abs/1410.0306},
eprinttype = {arXiv},
eprint = {1410.0306},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/SergeyNB14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/japll/GabbayN13,
author = {Murdoch James Gabbay and
Aleksandar Nanevski},
title = {Denotation of contextual modal type theory {(CMTT):} Syntax and meta-programming},
journal = {J. Appl. Log.},
volume = {11},
number = {1},
pages = {1--29},
year = {2013},
url = {https://doi.org/10.1016/j.jal.2012.07.002},
doi = {10.1016/J.JAL.2012.07.002},
timestamp = {Tue, 16 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/japll/GabbayN13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfp/GonthierZND13,
author = {Georges Gonthier and
Beta Ziliani and
Aleksandar Nanevski and
Derek Dreyer},
title = {How to make ad hoc proof automation less ad hoc},
journal = {J. Funct. Program.},
volume = {23},
number = {4},
pages = {357--401},
year = {2013},
url = {https://doi.org/10.1017/S0956796813000051},
doi = {10.1017/S0956796813000051},
timestamp = {Sat, 27 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jfp/GonthierZND13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/toplas/NanevskiBG13,
author = {Aleksandar Nanevski and
Anindya Banerjee and
Deepak Garg},
title = {Dependent Type Theory for Verification of Information Flow and Access
Control Policies},
journal = {{ACM} Trans. Program. Lang. Syst.},
volume = {35},
number = {2},
pages = {6:1--6:41},
year = {2013},
url = {https://doi.org/10.1145/2491522.2491523},
doi = {10.1145/2491522.2491523},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/toplas/NanevskiBG13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/ItzhakyBINS13,
author = {Shachar Itzhaky and
Anindya Banerjee and
Neil Immerman and
Aleksandar Nanevski and
Mooly Sagiv},
editor = {Natasha Sharygina and
Helmut Veith},
title = {Effectively-Propositional Reasoning about Reachability in Linked Data
Structures},
booktitle = {Computer Aided Verification - 25th International Conference, {CAV}
2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8044},
pages = {756--772},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-39799-8\_53},
doi = {10.1007/978-3-642-39799-8\_53},
timestamp = {Wed, 07 Dec 2022 23:12:58 +0100},
biburl = {https://dblp.org/rec/conf/cav/ItzhakyBINS13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icfp/ZilianiDKNV13,
author = {Beta Ziliani and
Derek Dreyer and
Neelakantan R. Krishnaswami and
Aleksandar Nanevski and
Viktor Vafeiadis},
editor = {Greg Morrisett and
Tarmo Uustalu},
title = {Mtac: a monad for typed tactic programming in Coq},
booktitle = {{ACM} {SIGPLAN} International Conference on Functional Programming,
ICFP'13, Boston, MA, {USA} - September 25 - 27, 2013},
pages = {87--100},
publisher = {{ACM}},
year = {2013},
url = {https://doi.org/10.1145/2500365.2500579},
doi = {10.1145/2500365.2500579},
timestamp = {Thu, 24 Jun 2021 16:19:30 +0200},
biburl = {https://dblp.org/rec/conf/icfp/ZilianiDKNV13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icfp/DelbiancoN13,
author = {Germ{\'{a}}n Andr{\'{e}}s Delbianco and
Aleksandar Nanevski},
editor = {Greg Morrisett and
Tarmo Uustalu},
title = {Hoare-style reasoning with (algebraic) continuations},
booktitle = {{ACM} {SIGPLAN} International Conference on Functional Programming,
ICFP'13, Boston, MA, {USA} - September 25 - 27, 2013},
pages = {363--376},
publisher = {{ACM}},
year = {2013},
url = {https://doi.org/10.1145/2500365.2500593},
doi = {10.1145/2500365.2500593},
timestamp = {Thu, 24 Jun 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/icfp/DelbiancoN13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/popl/Ley-WildN13,
author = {Ruy Ley{-}Wild and
Aleksandar Nanevski},
editor = {Roberto Giacobazzi and
Radhia Cousot},
title = {Subjective auxiliary state for coarse-grained concurrency},
booktitle = {The 40th Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of
Programming Languages, {POPL} '13, Rome, Italy - January 23 - 25,
2013},
pages = {561--574},
publisher = {{ACM}},
year = {2013},
url = {https://doi.org/10.1145/2429069.2429134},
doi = {10.1145/2429069.2429134},
timestamp = {Thu, 24 Jun 2021 16:19:31 +0200},
biburl = {https://dblp.org/rec/conf/popl/Ley-WildN13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ppdp/StewartBN13,
author = {Gordon Stewart and
Anindya Banerjee and
Aleksandar Nanevski},
editor = {Ricardo Pe{\~{n}}a and
Tom Schrijvers},
title = {Dependent types for enforcement of information flow and erasure policies
in heterogeneous data structures},
booktitle = {15th International Symposium on Principles and Practice of Declarative
Programming, {PPDP} '13, Madrid, Spain, September 16-18, 2013},
pages = {145--156},
publisher = {{ACM}},
year = {2013},
url = {https://doi.org/10.1145/2505879.2505895},
doi = {10.1145/2505879.2505895},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/ppdp/StewartBN13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1202-0904,
author = {Murdoch Gabbay and
Aleksandar Nanevski},
title = {Denotation of syntax and metaprogramming in contextual modal type
theory {(CMTT)}},
journal = {CoRR},
volume = {abs/1202.0904},
year = {2012},
url = {http://arxiv.org/abs/1202.0904},
eprinttype = {arXiv},
eprint = {1202.0904},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1202-0904.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icfp/GonthierZND11,
author = {Georges Gonthier and
Beta Ziliani and
Aleksandar Nanevski and
Derek Dreyer},
editor = {Manuel M. T. Chakravarty and
Zhenjiang Hu and
Olivier Danvy},
title = {How to make ad hoc proof automation less ad hoc},
booktitle = {Proceeding of the 16th {ACM} {SIGPLAN} international conference on
Functional Programming, {ICFP} 2011, Tokyo, Japan, September 19-21,
2011},
pages = {163--175},
publisher = {{ACM}},
year = {2011},
url = {https://doi.org/10.1145/2034773.2034798},
doi = {10.1145/2034773.2034798},
timestamp = {Thu, 24 Jun 2021 16:19:30 +0200},
biburl = {https://dblp.org/rec/conf/icfp/GonthierZND11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sp/NanevskiBG11,
author = {Aleksandar Nanevski and
Anindya Banerjee and
Deepak Garg},
title = {Verification of Information Flow and Access Control Policies with
Dependent Types},
booktitle = {32nd {IEEE} Symposium on Security and Privacy, {SP} 2011, 22-25 May
2011, Berkeley, California, {USA}},
pages = {165--179},
publisher = {{IEEE} Computer Society},
year = {2011},
url = {https://doi.org/10.1109/SP.2011.12},
doi = {10.1109/SP.2011.12},
timestamp = {Thu, 21 Sep 2023 16:14:16 +0200},
biburl = {https://dblp.org/rec/conf/sp/NanevskiBG11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tlca/SvendsenBN11,
author = {Kasper Svendsen and
Lars Birkedal and
Aleksandar Nanevski},
editor = {C.{-}H. Luke Ong},
title = {Partiality, State and Dependent Types},
booktitle = {Typed Lambda Calculi and Applications - 10th International Conference,
{TLCA} 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6690},
pages = {198--212},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-21691-6\_17},
doi = {10.1007/978-3-642-21691-6\_17},
timestamp = {Tue, 14 May 2019 10:00:41 +0200},
biburl = {https://dblp.org/rec/conf/tlca/SvendsenBN11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/popl/NanevskiVB10,
author = {Aleksandar Nanevski and
Viktor Vafeiadis and
Josh Berdine},
editor = {Manuel V. Hermenegildo and
Jens Palsberg},
title = {Structuring the verification of heap-manipulating programs},
booktitle = {Proceedings of the 37th {ACM} {SIGPLAN-SIGACT} Symposium on Principles
of Programming Languages, {POPL} 2010, Madrid, Spain, January 17-23,
2010},
pages = {261--274},
publisher = {{ACM}},
year = {2010},
url = {https://doi.org/10.1145/1706299.1706331},
doi = {10.1145/1706299.1706331},
timestamp = {Tue, 22 Jun 2021 17:10:57 +0200},
biburl = {https://dblp.org/rec/conf/popl/NanevskiVB10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tldi/NanevskiGM09,
author = {Aleksandar Nanevski and
Paul Govereau and
Greg Morrisett},
editor = {Andrew Kennedy and
Amal Ahmed},
title = {Towards type-theoretic semantics for transactional concurrency},
booktitle = {Proceedings of TLDI'09: 2009 {ACM} {SIGPLAN} International Workshop
on Types in Languages Design and Implementation, Savannah, GA, USA,
January 24, 2009},
pages = {79--90},
publisher = {{ACM}},
year = {2009},
url = {https://doi.org/10.1145/1481861.1481872},
doi = {10.1145/1481861.1481872},
timestamp = {Tue, 05 Jul 2022 08:30:25 +0200},
biburl = {https://dblp.org/rec/conf/tldi/NanevskiGM09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfp/NanevskiMB08,
author = {Aleksandar Nanevski and
J. Gregory Morrisett and
Lars Birkedal},
title = {Hoare type theory, polymorphism and separation},
journal = {J. Funct. Program.},
volume = {18},
number = {5-6},
pages = {865--911},
year = {2008},
url = {https://doi.org/10.1017/S0956796808006953},
doi = {10.1017/S0956796808006953},
timestamp = {Wed, 14 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/jfp/NanevskiMB08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tocl/NanevskiPP08,
author = {Aleksandar Nanevski and
Frank Pfenning and
Brigitte Pientka},
title = {Contextual modal type theory},
journal = {{ACM} Trans. Comput. Log.},
volume = {9},
number = {3},
pages = {23:1--23:49},
year = {2008},
url = {https://doi.org/10.1145/1352582.1352591},
doi = {10.1145/1352582.1352591},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/tocl/NanevskiPP08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/esop/PetersenBNM08,
author = {Rasmus Lerchedahl Petersen and
Lars Birkedal and
Aleksandar Nanevski and
Greg Morrisett},
editor = {Sophia Drossopoulou},
title = {A Realizability Model for Impredicative Hoare Type Theory},
booktitle = {Programming Languages and Systems, 17th European Symposium on Programming,
{ESOP} 2008, Held as Part of the Joint European Conferences on Theory
and Practice of Software, {ETAPS} 2008, Budapest, Hungary, March 29-April
6, 2008. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4960},
pages = {337--352},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-540-78739-6\_26},
doi = {10.1007/978-3-540-78739-6\_26},
timestamp = {Sun, 02 Jun 2019 21:23:56 +0200},
biburl = {https://dblp.org/rec/conf/esop/PetersenBNM08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icfp/NanevskiMSGB08,
author = {Aleksandar Nanevski and
Greg Morrisett and
Avraham Shinnar and
Paul Govereau and
Lars Birkedal},
editor = {James Hook and
Peter Thiemann},
title = {Ynot: dependent types for imperative programs},
booktitle = {Proceeding of the 13th {ACM} {SIGPLAN} international conference on
Functional programming, {ICFP} 2008, Victoria, BC, Canada, September
20-28, 2008},
pages = {229--240},
publisher = {{ACM}},
year = {2008},
url = {https://doi.org/10.1145/1411204.1411237},
doi = {10.1145/1411204.1411237},
timestamp = {Fri, 25 Jun 2021 14:48:54 +0200},
biburl = {https://dblp.org/rec/conf/icfp/NanevskiMSGB08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/esop/NanevskiAMB07,
author = {Aleksandar Nanevski and
Amal Ahmed and
Greg Morrisett and
Lars Birkedal},
editor = {Rocco De Nicola},
title = {Abstract Predicates and Mutable ADTs in Hoare Type Theory},
booktitle = {Programming Languages and Systems, 16th European Symposium on Programming,
{ESOP} 2007, Held as Part of the Joint European Conferences on Theory
and Practics of Software, {ETAPS} 2007, Braga, Portugal, March 24
- April 1, 2007, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4421},
pages = {189--204},
publisher = {Springer},
year = {2007},
url = {https://doi.org/10.1007/978-3-540-71316-6\_14},
doi = {10.1007/978-3-540-71316-6\_14},
timestamp = {Tue, 05 Jul 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/esop/NanevskiAMB07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icfp/NanevskiMB06,
author = {Aleksandar Nanevski and
Greg Morrisett and
Lars Birkedal},
editor = {John H. Reppy and
Julia Lawall},
title = {Polymorphism and separation in hoare type theory},
booktitle = {Proceedings of the 11th {ACM} {SIGPLAN} International Conference on
Functional Programming, {ICFP} 2006, Portland, Oregon, USA, September
16-21, 2006},
pages = {62--73},
publisher = {{ACM}},
year = {2006},
url = {https://doi.org/10.1145/1159803.1159812},
doi = {10.1145/1159803.1159812},
timestamp = {Mon, 17 Jan 2022 15:20:18 +0100},
biburl = {https://dblp.org/rec/conf/icfp/NanevskiMB06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfp/NanevskiP05,
author = {Aleksandar Nanevski and
Frank Pfenning},
title = {Staged computation with names and necessity},
journal = {J. Funct. Program.},
volume = {15},
number = {5},
pages = {893--939},
year = {2005},
url = {https://doi.org/10.1017/S095679680500568X},
doi = {10.1017/S095679680500568X},
timestamp = {Sat, 27 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jfp/NanevskiP05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/lisp/NanevskiBH03,
author = {Aleksandar Nanevski and
Guy E. Blelloch and
Robert Harper},
title = {Automatic Generation of Staged Geometric Predicates},
journal = {High. Order Symb. Comput.},
volume = {16},
number = {4},
pages = {379--400},
year = {2003},
url = {https://doi.org/10.1023/A:1025876920522},
doi = {10.1023/A:1025876920522},
timestamp = {Thu, 05 Mar 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/lisp/NanevskiBH03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icfp/NanevskiPP03,
author = {Aleksandar Nanevski and
Brigitte Pientka and
Frank Pfenning},
title = {A modal foundation for meta-variables},
booktitle = {Eighth {ACM} {SIGPLAN} International Conference on Functional Programming,
Workshop on Mechanized reasoning about languages with variable binding,
{MERLIN} 2003, Uppsala, Sweden, August 2003},
publisher = {{ACM}},
year = {2003},
url = {https://doi.org/10.1145/976571.976582},
doi = {10.1145/976571.976582},
timestamp = {Mon, 12 Jul 2021 15:34:15 +0200},
biburl = {https://dblp.org/rec/conf/icfp/NanevskiPP03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ppdp/Nanevski03,
author = {Aleksandar Nanevski},
title = {From dynamic binding to state via modal possibility},
booktitle = {Proceedings of the 5th International {ACM} {SIGPLAN} Conference on
Principles and Practice of Declarative Programming, 27-29 August 2003,
Uppsala, Sweden},
pages = {207--218},
publisher = {{ACM}},
year = {2003},
url = {https://doi.org/10.1145/888251.888271},
doi = {10.1145/888251.888271},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/ppdp/Nanevski03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icfp/Nanevski02,
author = {Aleksandar Nanevski},
editor = {Mitchell Wand and
Simon L. Peyton Jones},
title = {Meta-programming with names and necessity},
booktitle = {Proceedings of the Seventh {ACM} {SIGPLAN} International Conference
on Functional Programming {(ICFP} '02), Pittsburgh, Pennsylvania,
USA, October 4-6, 2002},
pages = {206--217},
publisher = {{ACM}},
year = {2002},
url = {https://doi.org/10.1145/581478.581498},
doi = {10.1145/581478.581498},
timestamp = {Wed, 07 Jul 2021 17:30:33 +0200},
biburl = {https://dblp.org/rec/conf/icfp/Nanevski02.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icfp/NanevskiBH01,
author = {Aleksandar Nanevski and
Guy E. Blelloch and
Robert Harper},
editor = {Benjamin C. Pierce},
title = {Automatic Generation of Staged Geometric Predicates},
booktitle = {Proceedings of the Sixth {ACM} {SIGPLAN} International Conference
on Functional Programming {(ICFP} '01), Firenze (Florence), Italy,
September 3-5, 2001},
pages = {217--228},
publisher = {{ACM}},
year = {2001},
url = {https://doi.org/10.1145/507635.507662},
doi = {10.1145/507635.507662},
timestamp = {Wed, 07 Jul 2021 17:30:33 +0200},
biburl = {https://dblp.org/rec/conf/icfp/NanevskiBH01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
a service of 
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.
last updated on 2024-04-25 02:15 CEST 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:
