Change search
ReferencesLink to record
Permanent link

Direct link
Realizability in Coq
KTH, School of Engineering Sciences (SCI), Mathematics (Dept.), Mathematics (Div.).
2015 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesisAlternative title
Realiserbarhet i Coq (Swedish)
Abstract [en]

This thesis describes a Coq formalization of realizability interpretations of arithmetic. The realizability interpretations are based on partial combinatory algebras—to each partial combinatory algebra there is an associated realizability interpretation. I construct two partial combinatory algebras. One of these gives a realizability interpretation equivalent to Kleene’s original one, without involving the usual recursion-theoretic machinery.


Abstract [sv]

Den här uppsatsen beskriver en Coq-formalisering av realiserbarhetstolkningar av aritmetik. Realiserbarhetstolkningarna baseras på partiella kombinatoriska algebror—för varje partiell kombinatorisk algebra finns det en motsvarande realiserbarhetstolkning. Jag konstruerar två partiella kombinatoriska algebror. En av dessa ger en realiserbarhetstolkning som är ekvivalent med Kleenes ursprungliga tolkning, men dess konstruktion använder inte det sedvanliga rekursionsteoretiska maskineriet.

Place, publisher, year, edition, pages
TRITA-MAT-E, 2015:71
Keyword [en]
Coq, formalization, partial combinatory algebra, realizability
Keyword [sv]
Coq, formalisering, partiell kombinatorisk algebra, realiserbarhet
National Category
URN: urn:nbn:se:kth:diva-174109OAI: diva2:858615
Subject / course
Educational program
Master of Science - Mathematics
Available from: 2015-10-02 Created: 2015-09-30 Last updated: 2015-10-14Bibliographically approved

Open Access in DiVA

fulltext(543 kB)55 downloads
File information
File name FULLTEXT01.pdfFile size 543 kBChecksum SHA-512
Type fulltextMimetype application/pdf

By organisation
Mathematics (Div.)

Search outside of DiVA

GoogleGoogle Scholar
Total: 55 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 349 hits
ReferencesLink to record
Permanent link

Direct link