Nicolas Marti's Homepage
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