Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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
2015.
Series
TRITA-MAT-E, 2015:71
Keyword [en]
Coq, formalization, partial combinatory algebra, realizability
Keyword [sv]
Coq, formalisering, partiell kombinatorisk algebra, realiserbarhet
National Category
Mathematics
Identifiers
URN: urn:nbn:se:kth:diva-174109OAI: oai:DiVA.org:kth-174109DiVA: diva2:858615
External cooperation
Stockholms universitet
Subject / course
Mathematics
Educational program
Master of Science - Mathematics
Supervisors
Examiners
Available from: 2015-10-02 Created: 2015-09-30 Last updated: 2015-10-14Bibliographically approved

Open Access in DiVA

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

By organisation
Mathematics (Div.)
Mathematics

Search outside of DiVA

GoogleGoogle Scholar
Total: 119 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

urn-nbn

Altmetric score

urn-nbn
Total: 421 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf