Write a Blog >>
ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
Aleksandar Nanevski

Registered user since Sat 12 Sep 2015

Name:Aleksandar Nanevski

My research is in the design and implementation of programming languages and logics for software verification. More specifically, I am interested in applying programming methodology to facilitate the construction of formal proofs in mathematics in general, and of program correctness in particular. My recent focus has been on designing methods for integrating programming with pointers, concurrency, and other important imperative features, into dependent type systems such as that of the proof assistant Coq. The goal of the integration is to leverage the proving power of Coq to obtain effective and scalable ways for reasoning about security and correctness of imperative programs.

I am also interested in all other aspects of formal mathematics and programming language theory and applications related to compilation, optimization, semantics, interactive theorem proving, program extraction, automated deduction, decision procedures, program analysis and model checking.

Affiliation:IMDEA Software Institute


Show activities from other conferences

ICFP 2016-profile
View general profile