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.

The whole coq development is available in a single .tgz file with a makefile (using Coq 8.1)