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: Nanevski:Aleksandar
Contributed to:
2015
20152014
2014
2013
20132013
20132011
201120102008200820072006200320022001
2016
20172019Wrote 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.