Internalising modified realisability in constructive type theory
Logic
2017-01-11 v3 Logic in Computer Science
Abstract
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.
Keywords
Cite
@article{arxiv.math/0505418,
title = {Internalising modified realisability in constructive type theory},
author = {Erik Palmgren},
journal= {arXiv preprint arXiv:math/0505418},
year = {2017}
}
Comments
7 pages