Palmgren, Erik - Internalising modified realisability in constructive type theory

lmcs:2266 - Logical Methods in Computer Science, October 5, 2005, Volume 1, Issue 2
Internalising modified realisability in constructive type theory

Authors: Palmgren, Erik

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.


Source : oai:arXiv.org:math/0505418
DOI : 10.2168/LMCS-1(2:2)2005
Volume: Volume 1, Issue 2
Published on: October 5, 2005
Submitted on: November 3, 2004
Keywords: Mathematics - Logic,Computer Science - Logic in Computer Science,F.4.1


Share

Consultation statistics

This page has been seen 40 times.
This article's PDF has been downloaded 23 times.