Realizability toposes from specifications

Jonas Frey

doi:10.4230/LIPIcs.TLCA.2015.196

Realizability toposes from specifications

Jonas Frey

Datalogisk Institut

3 Citationer (Scopus)

Abstract

We investigate a framework of Krivine realizability with I/O effects, and present a method of associating realizability models to specifications on the I/O behavior of processes, by using adequate interpretations of the central concepts of pole and proof-like term. This method does in particular allow to associate realizability models to computable functions. Following recent work of Streicher and others we show how these models give rise to triposes and toposes.

Originalsprog	Engelsk
Tidsskrift	Leibniz International Proceedings in Informatics
Vol/bind	38
Sider (fra-til)	196-210
Antal sider	15
ISSN	1868-8969
DOI	https://doi.org/10.4230/LIPIcs.TLCA.2015.196
Status	Udgivet - 1 jul. 2015
Begivenhed	International Conference on Typed Lambda Calculi and Applications - , Tyskland Varighed: 1 okt. 2015 → … Konferencens nummer: 13

Konference

Konference	International Conference on Typed Lambda Calculi and Applications
Nummer	13
Land/Område	Tyskland
Periode	01/10/2015 → …

Adgang til dokumentet

10.4230/LIPIcs.TLCA.2015.196

http://drops.dagstuhl.de/opus/volltexte/2015/5164

Citationsformater

@inproceedings{ee45b84509814cbf97635bf8d556cc4a,

title = "Realizability toposes from specifications",

abstract = "We investigate a framework of Krivine realizability with I/O effects, and present a method of associating realizability models to specifications on the I/O behavior of processes, by using adequate interpretations of the central concepts of pole and proof-like term. This method does in particular allow to associate realizability models to computable functions. Following recent work of Streicher and others we show how these models give rise to triposes and toposes.",

author = "Jonas Frey",

year = "2015",

month = jul,

day = "1",

doi = "10.4230/LIPIcs.TLCA.2015.196",

language = "English",

volume = "38",

pages = "196--210",

journal = "Leibniz International Proceedings in Informatics, LIPIcs",

issn = "1868-8969",

publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH",

note = "International Conference on Typed Lambda Calculi and Applications ; Conference date: 01-10-2015",

}

TY - GEN

T1 - Realizability toposes from specifications

AU - Frey, Jonas

N1 - Conference code: 13

PY - 2015/7/1

Y1 - 2015/7/1

N2 - We investigate a framework of Krivine realizability with I/O effects, and present a method of associating realizability models to specifications on the I/O behavior of processes, by using adequate interpretations of the central concepts of pole and proof-like term. This method does in particular allow to associate realizability models to computable functions. Following recent work of Streicher and others we show how these models give rise to triposes and toposes.

AB - We investigate a framework of Krivine realizability with I/O effects, and present a method of associating realizability models to specifications on the I/O behavior of processes, by using adequate interpretations of the central concepts of pole and proof-like term. This method does in particular allow to associate realizability models to computable functions. Following recent work of Streicher and others we show how these models give rise to triposes and toposes.

U2 - 10.4230/LIPIcs.TLCA.2015.196

DO - 10.4230/LIPIcs.TLCA.2015.196

M3 - Conference article

SN - 1868-8969

VL - 38

SP - 196

EP - 210

JO - Leibniz International Proceedings in Informatics, LIPIcs

JF - Leibniz International Proceedings in Informatics, LIPIcs

T2 - International Conference on Typed Lambda Calculi and Applications

Y2 - 1 October 2015

ER -

Realizability toposes from specifications

Abstract

Konference

Adgang til dokumentet

Fingeraftryk

Citationsformater