I am a PhD student at the university of Paris XI in the LRI laboratory. I work in the Démons team under supervision of Christine Paulin-Mohring. My thesis subject is An environment for programming with dependent types. It consists in conceiving methods to ease definition and reasonning on bug-free, mechanicaly proved programs.