Aleksandar Nanevski

Author Info

Name	Affiliation	Papers
ALEKSANDAR NANEVSKI	IMDEA Software, Facultad de Informática (UPM), Campus Montegancedo, 28660 Boadilla del Monte, Madrid, Spain	34
Collaborators	Citations	PageRank
41	583	27.01
Referers	Referees	References
765	735	791

Search Limit

100765

Publications (34 rows)

Collaborators (41 rows)

Referers (100 rows)

Referees (100 rows)

Title	Citations	PageRank	Year
Contextual modal types for algebraic effects and handlers	0	0.34	2021
On Algebraic Abstractions for Concurrent Separation Logics	0	0.34	2021
Proving Highly-Concurrent Traversals Correct	0	0.34	2020
Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations.	1	0.35	2019
Concurrent Data Structures Linked in Time (Artifact).	0	0.34	2017
Concurrent Data Structures Linked in Time.	1	0.34	2017
Operational Aspects of C/C++ Concurrency.	2	0.36	2016
Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects	3	0.38	2015
Mechanized verification of fine-grained concurrent programs	28	0.80	2015
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity	6	0.41	2014
Communicating State Transition Systems for Fine-Grained Concurrent Resources.	32	0.95	2014
Modular reasoning about heap paths via effectively propositional formulas	6	0.45	2014
Effectively-Propositional reasoning about reachability in linked data structures	25	0.78	2013
How to make ad hoc proof automation less ad hoc	26	1.29	2013
Mtac: a monad for typed tactic programming in Coq	14	0.77	2013
Denotation of contextual modal type theory (CMTT): Syntax and meta-programming.	1	0.38	2013
Subjective auxiliary state for coarse-grained concurrency	23	0.92	2013
Dependent types for enforcement of information flow and erasure policies in heterogeneous data structures	4	0.42	2013
Hoare-style reasoning with (algebraic) continuations	2	0.40	2013
Dependent Type Theory for Verification of Information Flow and Access Control Policies	21	0.60	2013
Denotation of syntax and metaprogramming in contextual modal type theory (CMTT)	0	0.34	2012
Partiality, state and dependent types	4	0.42	2011
Verification of Information Flow and Access Control Policies with Dependent Types	44	1.09	2011
Towards type-theoretic semantics for transactional concurrency	5	0.42	2009
Contextual modal type theory	79	2.57	2008
Ynot: dependent types for imperative programs	68	2.20	2008
A realizability model for impredicative Hoare type theory	15	0.89	2008
Hoare type theory, polymorphism and separation1	31	1.05	2008
Abstract predicates and mutable adts in hoare type theory	30	1.25	2007
Polymorphism and separation in hoare type theory	64	2.43	2006
Staged computation with names and necessity	24	0.90	2005
Automatic Generation of Staged Geometric Predicates	8	1.24	2003
From dynamic binding to state via modal possibility	11	0.76	2003
A modal foundation for meta-variables	5	0.48	2003