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...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2005-10-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/2266/pdf |
| _version_ | 1827323038344937472 |
|---|---|
| author | Erik Palmgren |
| author_facet | Erik Palmgren |
| author_sort | Erik Palmgren |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:38:29Z |
| format | Article |
| id | doaj.art-e6a50aaee58b4184bb8a8c84c6ebe0f1 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:38:29Z |
| publishDate | 2005-10-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-e6a50aaee58b4184bb8a8c84c6ebe0f12024-03-08T08:32:15ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742005-10-01Volume 1, Issue 210.2168/LMCS-1(2:2)20052266Internalising modified realisability in constructive type theoryErik PalmgrenA 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.https://lmcs.episciences.org/2266/pdfmathematics - logiccomputer science - logic in computer sciencef.4.1 |
| spellingShingle | Erik Palmgren Internalising modified realisability in constructive type theory Logical Methods in Computer Science mathematics - logic computer science - logic in computer science f.4.1 |
| title | Internalising modified realisability in constructive type theory |
| title_full | Internalising modified realisability in constructive type theory |
| title_fullStr | Internalising modified realisability in constructive type theory |
| title_full_unstemmed | Internalising modified realisability in constructive type theory |
| title_short | Internalising modified realisability in constructive type theory |
| title_sort | internalising modified realisability in constructive type theory |
| topic | mathematics - logic computer science - logic in computer science f.4.1 |
| url | https://lmcs.episciences.org/2266/pdf |
| work_keys_str_mv | AT erikpalmgren internalisingmodifiedrealisabilityinconstructivetypetheory |