Nicolas Marti's Homepage



:D



I was a PhD student in the Yonezawa laboratory of the the University of Tokyo

My research focused on verification of programs.
More precisely I was interested in verification of operating systemes kernel.
I was working with Reynald Affeldt on a verification framework using separation logic using the Coq proof assistant (Implementation home page).

Here is a list of my publication

Here is my CV

My final Ph.D. thesis draft


Research software:

A certified verifier for separation logic (wedemo) (sources)

A kernel for typechecking a high-order typed lambda calculus (named Kernel), with a proof assistant (Poussin) and a computer algebra system (Minima) build on top (webdemo) (sources)


Obsolete work:
A little proof assistant

A little proof assistant/computer algebra system

my mail is
   
nicolas at yl dot is dot s dot u-tokyo dot ac dot jp