BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Canada
1 × France
1 × Hungary
1 × Japan
1 × Portugal
1 × Russia
1 × Serbia
1 × Sweden
1 × United Kingdom
2 × Italy
2 × Spain
5 × USA
Collaborated with:
G.A.Delbianco I.Sergey A.Banerjee L.Birkedal G.Morrisett R.Ley-Wild Anindya Banerjee 0001 V.Vafeiadis B.Ziliani D.Dreyer S.Itzhaky N.Immerman M.Sagiv G.Stewart K.Svendsen J.Berdine G.E.Blelloch R.Harper G.Gonthier R.L.Petersen A.Ahmed Ignacio Fábregas N.R.Krishnaswami A.Shinnar P.Govereau O.Lahav
Talks about:
concurr (7) type (7) program (6) hoar (5) structur (4) state (4) theori (3) reason (3) depend (3) grain (3)

Person: Aleksandar Nanevski

DBLP DBLP: Nanevski:Aleksandar

Contributed to:

ESOP 20152015
PLDI 20152015
ESOP 20142014
POPL 20142014
CAV 20132013
ICFP 20132013
POPL 20132013
PPDP 20132013
ICFP 20112011
TLCA 20112011
POPL 20102010
ESOP 20082008
ICFP 20082008
ESOP 20072007
ICFP 20062006
PPDP 20032003
ICFP 20022002
ICFP 20012001
OOPSLA 20162016
ECOOP 20172017
OOPSLA 20192019

Wrote 22 papers:

ESOP-2015-SergeyNB #algorithm #concurrent #specification #verification
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity (IS, AN, AB), pp. 333–358.
PLDI-2015-SergeyNB #concurrent #fine-grained #source code #verification
Mechanized verification of fine-grained concurrent programs (IS, AN, AB), pp. 77–87.
ESOP-2014-NanevskiLSD #communication #concurrent #fine-grained
Communicating State Transition Systems for Fine-Grained Concurrent Resources (AN, RLW, IS, GAD), pp. 290–310.
POPL-2014-ItzhakyBILNS #composition #effectiveness #reasoning
Modular reasoning about heap paths via effectively propositional formulas (SI, AB, NI, OL, AN, MS), pp. 385–396.
CAV-2013-ItzhakyBINS #data type #effectiveness #linked data #open data #reachability #reasoning
Effectively-Propositional Reasoning about Reachability in Linked Data Structures (SI, AB, NI, AN, MS), pp. 756–772.
ICFP-2013-DelbiancoN #algebra #continuation #hoare #reasoning
Hoare-style reasoning with (algebraic) continuations (GAD, AN), pp. 363–376.
ICFP-2013-ZilianiDKNV #coq #monad #named #programming
Mtac: a monad for typed tactic programming in Coq (BZ, DD, NRK, AN, VV), pp. 87–100.
POPL-2013-Ley-WildN #concurrent
Subjective auxiliary state for coarse-grained concurrency (RLW, AN), pp. 561–574.
PPDP-2013-StewartBN #data flow #data type #dependent type #policy #semistructured data
Dependent types for enforcement of information flow and erasure policies in heterogeneous data structures (GS, AB, AN), pp. 145–156.
ICFP-2011-GonthierZND #ad hoc #automation #how #proving
How to make ad hoc proof automation less ad hoc (GG, BZ, AN, DD), pp. 163–175.
TLCA-2011-SvendsenBN #dependent type
Partiality, State and Dependent Types (KS, LB, AN), pp. 198–212.
POPL-2010-NanevskiVB #source code #verification
Structuring the verification of heap-manipulating programs (AN, VV, JB), pp. 261–274.
ESOP-2008-PetersenBNM #hoare #type system
A Realizability Model for Impredicative Hoare Type Theory (RLP, LB, AN, GM), pp. 337–352.
ICFP-2008-NanevskiMSGB #dependent type #imperative #named #source code
Ynot: dependent types for imperative programs (AN, GM, AS, PG, LB), pp. 229–240.
ESOP-2007-NanevskiAMB #data type #hoare #type system
Abstract Predicates and Mutable ADTs in Hoare Type Theory (AN, AA, GM, LB), pp. 189–204.
ICFP-2006-NanevskiMB #hoare #morphism #polymorphism #type system
Polymorphism and separation in hoare type theory (AN, GM, LB), pp. 62–73.
PPDP-2003-Nanevski
From dynamic binding to state via modal possibility (AN), pp. 207–218.
ICFP-2002-Nanevski #metaprogramming
Meta-programming with names and necessity (AN), pp. 206–217.
ICFP-2001-NanevskiBH #automation #generative #geometry #staged
Automatic Generation of Staged Geometric Predicates (AN, GEB, RH), pp. 217–228.
OOPSLA-2016-SergeyNBD #concurrent #correctness #hoare #specification
Hoare-style specifications as correctness conditions for non-linearizable concurrent objects (IS, AN, AB0, GAD), pp. 92–110.
ECOOP-2017-DelbiancoSNB #concurrent #data type
Concurrent Data Structures Linked in Time (GAD, IS, AN, AB0), p. 30.
OOPSLA-2019-Nanevski0DF #concurrent #logic #morphism #simulation #source code #specification
Specifying concurrent programs in separation logic: morphisms and simulations (AN, AB0, GAD, IF), p. 30.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.