Internalising modified realisability in constructive type theory

摘要

A modified realisability interpretation of infinitary logicis formalised and proved sound in constructive typetheory (CTT). The logic considered subsumes first order logic. The interpretation makes it possible to extract programs with simplifiedtypes and to incorporate and reason about them in CTT.