M. började som sannolikhetsteoretiker i Kolmogorovs skola och är bl.a. känd för arbeten om begreppet slumpföljd. Han övergick därefter till logik och matematisk grundvalsforskning. M:s viktigaste arbeten inom dessa områden gäller utvecklandet av en intuitionistisk typteori (Intuitionistic Type Theory, 1984), som visat sig ytterst fruktbar även inom datalogi