Aleks Nanevski

Aleks Nanevski is a Research Professor at the IMDEA Software Institute in Madrid, Spain. He holds a Ph.D. in Computer Science from Carnegie Mellon University (2004) and completed postdoctoral research at Harvard University and Microsoft Research. His research focuses on programming languages and formal verification, particularly integrating dependent type systems with imperative features like concurrency and pointers. He co-leads the Functional Concurrent Separation Logic (FCSL) project, advancing verification techniques for concurrent programs.

Education & Affiliations:

• Ph.D. in Computer Science, Carnegie Mellon University (2004)
• Postdoctoral Fellowships: Harvard University (USA), Microsoft Research (UK)
• Joined IMDEA Software Institute in 2009

Research Interests:

Nanevski designs languages and logics that unify programming with formal verification, leveraging type theory to ensure correctness in systems with imperative features. His work emphasizes concurrency, pointer arithmetic, and modular reasoning in concurrent separation logics. Recent efforts include declarative linearizability proofs and contextual modal types for algebraic effects.

Professional Activities:

• Program Chair: HOPE 2017, LOLA 2012
• PC Member: OOPSLA 2024, POPL 2023, and multiple top-tier conferences

Advising & Team:

• Current advisees: Jesús Domínguez, Joakim Öhman
• Former advisees include Ilya Sergey (Postdoc), Germán Delbianco (PhD), and Nikita Zyuzin

Labs/Teams:

Leads the FCSL project, developing tools for verifying fine-grained concurrent programs using dependent types and separation logic.