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 2855 times.
This article's PDF has been downloaded 379 times.