This is meant to be the homepage of seplog, an implementation of separation logic in Coq. For the time being, you will find more information here.