Internalising modified realisability in constructive type theory

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 CT...

Full description

Bibliographic Details
Main Author: Erik Palmgren
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2005-10-01
Series:Logical Methods in Computer Science
Subjects:
mathematics - logic
computer science - logic in computer science
f.4.1
Online Access:https://lmcs.episciences.org/2266/pdf

Similar Items

Similar Items