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...
| Hlavní autor: | |
|---|---|
| Médium: | Článek |
| Jazyk: | English |
| Vydáno: |
Logical Methods in Computer Science e.V.
2005-10-01
|
| Edice: | Logical Methods in Computer Science |
| Témata: | |
| On-line přístup: | https://lmcs.episciences.org/2266/pdf |
| Shrnutí: | 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. |
|---|---|
| ISSN: | 1860-5974 |