Suivre
Aleksandar Nanevski
Aleksandar Nanevski
IMDEA Software Institute
Adresse e-mail validée de imdea.org - Page d'accueil
Titre
Citée par
Citée par
Année
Contextual modal type theory
A Nanevski, F Pfenning, B Pientka
ACM Transactions on Computational Logic (TOCL) 9 (3), 1-49, 2008
3832008
Ynot: dependent types for imperative programs
A Nanevski, G Morrisett, A Shinnar, P Govereau, L Birkedal
Proceedings of the 13th ACM SIGPLAN international conference on Functional …, 2008
283*2008
Polymorphism and separation in Hoare type theory
A Nanevski, G Morrisett, L Birkedal
ACM SIGPLAN Notices 41 (9), 62-73, 2006
1862006
Hoare type theory, polymorphism and separation1
A Nanevski, G Morrisett, L Birkedal
Journal of Functional Programming 18 (5-6), 865-911, 2008
1792008
Mechanized verification of fine-grained concurrent programs
I Sergey, A Nanevski, A Banerjee
Proceedings of the 36th ACM SIGPLAN Conference on Programming Language …, 2015
1612015
Communicating state transition systems for fine-grained concurrent resources
A Nanevski, R Ley-Wild, I Sergey, GA Delbianco
Programming Languages and Systems: 23rd European Symposium on Programming …, 2014
1522014
Verification of information flow and access control policies with dependent types
A Nanevski, A Banerjee, D Garg
2011 IEEE Symposium on Security and Privacy, 165-179, 2011
1222011
Structuring the verification of heap-manipulating programs
A Nanevski, V Vafeiadis, J Berdine
Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2010
922010
Inferring invariants in separation logic for imperative list-processing programs
S Magill, A Nanevski, E Clarke, P Lee
SPACE 1 (1), 5-7, 2006
852006
Subjective auxiliary state for coarse-grained concurrency
R Ley-Wild, A Nanevski
Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2013
822013
Meta-programming with names and necessity
A Nanevski
ACM SIGPLAN Notices 37 (9), 206-217, 2002
792002
Abstract predicates and mutable ADTs in Hoare type theory
A Nanevski, A Ahmed, G Morrisett, L Birkedal
Programming Languages and Systems: 16th European Symposium on Programming …, 2007
772007
Specifying and verifying concurrent algorithms with histories and subjectivity
I Sergey, A Nanevski, A Banerjee
Programming Languages and Systems: 24th European Symposium on Programming …, 2015
732015
Effectively-propositional reasoning about reachability in linked data structures
S Itzhaky, A Banerjee, N Immerman, A Nanevski, M Sagiv
International Conference on Computer Aided Verification, 756-772, 2013
732013
Dependent type theory for verification of information flow and access control policies
A Nanevski, A Banerjee, D Garg
ACM Transactions on Programming Languages and Systems (TOPLAS) 35 (2), 1-41, 2013
732013
How to make ad hoc proof automation less ad hoc
G Gonthier, B Ziliani, A Nanevski, D Dreyer
ACM SIGPLAN Notices 46 (9), 163-175, 2011
682011
Mtac: a monad for typed tactic programming in Coq
B Ziliani, D Dreyer, NR Krishnaswami, A Nanevski, V Vafeiadis
ACM SIGPLAN Notices 48 (9), 87-100, 2013
572013
Staged computation with names and necessity
A Nanevski, F Pfenning
Journal of Functional Programming 15 (6), 893-939, 2005
552005
Mtac: A monad for typed tactic programming in Coq
B Ziliani, D Dreyer, NR Krishnaswami, A Nanevski, V Vafeiadis
Journal of functional programming 25, e12, 2015
502015
Modular reasoning about heap paths via effectively propositional formulas
S Itzhaky, A Banerjee, N Immerman, O Lahav, A Nanevski, M Sagiv
ACM SIGPLAN Notices 49 (1), 385-396, 2014
462014
Le système ne peut pas réaliser cette opération maintenant. Veuillez réessayer plus tard.
Articles 1–20