License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TLCA.2015.196
URN: urn:nbn:de:0030-drops-51645
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5164/
Go to the corresponding LIPIcs Volume Portal

Frey, Jonas

Realizability Toposes from Specifications

pdf-format:
19.pdf (0.5 MB)

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 ad- equate 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.

BibTeX - Entry

@InProceedings{frey:LIPIcs:2015:5164,
  author =	{Jonas Frey},
  title =	{{Realizability Toposes from Specifications}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{196--210},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Thorsten Altenkirch},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5164},
  URN =		{urn:nbn:de:0030-drops-51645},
  doi =		{10.4230/LIPIcs.TLCA.2015.196},
  annote =	{Keywords: Krivine machine, classical realizability, realizability topos, bisimulation}
}

Keywords: Krivine machine, classical realizability, realizability topos, bisimulation
Collection: 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)
Issue Date: 2015
Date of publication: 15.06.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI