Challenges Extensibility and openness not designed for certain specific interoperations But can we just use MLFs, e.g.Coq? Expressiveness type safety,concurrency properties,partial correctness,.. A general and uniform model of control flow Allow functions certified in different systems to call each other the key for modularity:separate verification proof reuse Principled interoperation with clear meta-property properties of the whole system composed of modules Not readily supported in Coq!Challenges ◼ Extensibility and openness ◼ not designed for certain specific interoperations But can we just use MLFs, e.g. Coq? ◼ Expressiveness ◼ type safety, concurrency properties, partial correctness, … ◼ A general and uniform model of control flow ◼ Allow functions certified in different systems to call each other ◼ the key for modularity: separate verification & proof reuse ◼ Principled interoperation with clear meta-property ◼ properties of the whole system composed of modules Not readily supported in Coq!