Erik Palmgren - Internalising modified realisability in constructive type theory

lmcs:2266 - Logical Methods in Computer Science, October 5, 2005, Volume 1, Issue 2 - https://doi.org/10.2168/LMCS-1(2:2)2005
Internalising modified realisability in constructive type theoryArticle

Authors: Erik Palmgren

    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.

    Comment: 7 pages

    https://doi.org/10.2168/LMCS-1(2:2)2005
    Source: arXiv.org:math/0505418
    Volume: Volume 1, Issue 2
    Published on: October 5, 2005
    Imported on: November 3, 2004
    Keywords: Mathematics - Logic, Computer Science - Logic in Computer Science, F.4.1
    Licence: arXiv.org - Assumed non-exclusive license to distribute

    Share and export

    Consultation statistics

    This page has been seen 2649 times.
    This article's PDF has been downloaded 334 times.