Dependent Types and Multi-monadic Effects in F*Nikhil Swamy1 Cătălin Hriţcu2 Chantal Keller1,3 Aseem Rastogi4 Antoine Delignat-Lavaud2,5 Simon Forest2,5 Karthikeyan Bhargavan2 Cédric Fournet1,3 Pierre-Yves Strub6 Markulf Kohlweiss1 Jean-Karim Zinzindohoue2,5 Santiago Zanella-Béguelin1 1Microsoft Research 2Inria 3MSR-Inria 4UMD 5ENS Paris 6IMDEA Software Institute Symposium on Principles of Programming Languages, POPL 2016 Abstract We present a
