Semantic foundations and inference of non-null annotations

You can find here the Coq sources of the development of the article Semantic foundations and inference of non-null annotations.