Internalising modified realisability in constructive type theory
英文摘要：
A modified realisability interpretation of infinitary logic is formalised and proved sound in constructive type theory (CTT). The logic considered subsumes first order logic. The interpretation makes it possible to extract programs with simplified types and to incorporate and reason about them in CTT.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
