License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2021.25
URN: urn:nbn:de:0030-drops-142631
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14263/
Matache, Cristina ;
Moss, Sean ;
Staton, Sam
Recursion and Sequentiality in Categories of Sheaves
Abstract
We present a fully abstract model of a call-by-value language with higher-order functions, recursion and natural numbers, as an exponential ideal in a topos. Our model is inspired by the fully abstract models of O'Hearn, Riecke and Sandholm, and Marz and Streicher. In contrast with semantics based on cpo’s, we treat recursion as just one feature in a model built by combining a choice of modular components.
BibTeX - Entry
@InProceedings{matache_et_al:LIPIcs.FSCD.2021.25,
author = {Matache, Cristina and Moss, Sean and Staton, Sam},
title = {{Recursion and Sequentiality in Categories of Sheaves}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {25:1--25:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-191-7},
ISSN = {1868-8969},
year = {2021},
volume = {195},
editor = {Kobayashi, Naoki},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/14263},
URN = {urn:nbn:de:0030-drops-142631},
doi = {10.4230/LIPIcs.FSCD.2021.25},
annote = {Keywords: Denotational semantics, Full abstraction, Recursion, Sheaf toposes, CPOs}
}
|
Keywords: |
|
Denotational semantics, Full abstraction, Recursion, Sheaf toposes, CPOs |
|
Collection: |
|
6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021) |
|
Issue Date: |
|
2021 |
|
Date of publication: |
|
06.07.2021 |
