4 Search Results for "Kelly, Robert"

Document
DOI: 10.4230/LIPIcs.FSCD.2024.19
Semantics for a Turing-Complete Reversible Programming Language with Inductive Types

Authors: Kostia Chardonnet, Louis Lemonnier, and Benoît Valiron

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
This paper is concerned with the expressivity and denotational semantics of a functional higher-order reversible programming language based on Theseus. In this language, pattern-matching is used to ensure the reversibility of functions. We show how one can encode any Reversible Turing Machine in said language. We then build a sound and adequate categorical semantics based on join inverse categories, with additional structures to capture pattern-matching and to interpret inductive types and recursion. We then derive a notion of completeness in the sense that any computable, partial, first-order injective function is the image of a term in the language.
Cite as

Kostia Chardonnet, Louis Lemonnier, and Benoît Valiron. Semantics for a Turing-Complete Reversible Programming Language with Inductive Types. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{chardonnet_et_al:LIPIcs.FSCD.2024.19,
  author =	{Chardonnet, Kostia and Lemonnier, Louis and Valiron, Beno\^{i}t},
  title =	{{Semantics for a Turing-Complete Reversible Programming Language with Inductive Types}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{19:1--19:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.19},
  URN =		{urn:nbn:de:0030-drops-203487},
  doi =		{10.4230/LIPIcs.FSCD.2024.19},
  annote =	{Keywords: Reversible programming, functional programming, Computability, Denotational Semantics}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.14
Two-Dimensional Kripke Semantics I: Presheaves

Authors: G. A. Kavvos

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
The study of modal logic has witnessed tremendous development following the introduction of Kripke semantics. However, recent developments in programming languages and type theory have led to a second way of studying modalities, namely through their categorical semantics. We show how the two correspond.
Cite as

G. A. Kavvos. Two-Dimensional Kripke Semantics I: Presheaves. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 14:1-14:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{kavvos:LIPIcs.FSCD.2024.14,
  author =	{Kavvos, G. A.},
  title =	{{Two-Dimensional Kripke Semantics I: Presheaves}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{14:1--14:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.14},
  URN =		{urn:nbn:de:0030-drops-203438},
  doi =		{10.4230/LIPIcs.FSCD.2024.14},
  annote =	{Keywords: modal logic, categorical semantics, Kripke semantics, duality, open maps}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2018.10
Concurrent Robin Hood Hashing

Authors: Robert Kelly, Barak A. Pearlmutter, and Phil Maguire

Published in: LIPIcs, Volume 125, 22nd International Conference on Principles of Distributed Systems (OPODIS 2018)

Abstract
In this paper we examine the issues involved in adding concurrency to the Robin Hood hash table algorithm. We present a non-blocking obstruction-free K-CAS Robin Hood algorithm which requires only a single word compare-and-swap primitive, thus making it highly portable. The implementation maintains the attractive properties of the original Robin Hood structure, such as a low expected probe length, capability to operate effectively under a high load factor and good cache locality, all of which are essential for high performance on modern computer architectures. We compare our data-structures to various other lock-free and concurrent algorithms, as well as a simple hardware transactional variant, and show that our implementation performs better across a number of contexts.
Cite as

Robert Kelly, Barak A. Pearlmutter, and Phil Maguire. Concurrent Robin Hood Hashing. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kelly_et_al:LIPIcs.OPODIS.2018.10,
  author =	{Kelly, Robert and Pearlmutter, Barak A. and Maguire, Phil},
  title =	{{Concurrent Robin Hood Hashing}},
  booktitle =	{22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
  pages =	{10:1--10:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-098-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{125},
  editor =	{Cao, Jiannong and Ellen, Faith and Rodrigues, Luis and Ferreira, Bernardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2018.10},
  URN =		{urn:nbn:de:0030-drops-100701},
  doi =		{10.4230/LIPIcs.OPODIS.2018.10},
  annote =	{Keywords: concurrency, Robin Hood Hashing, data-structures, hash tables, non-blocking}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.GISCIENCE.2018.58
Dynamically-Spaced Geo-Grid Segmentation for Weighted Point Sampling on a Polygon Map Layer (Short Paper)

Authors: Kelly Sims, Gautam Thakur, Kevin Sparks, Marie Urban, Amy Rose, and Robert Stewart

Published in: LIPIcs, Volume 114, 10th International Conference on Geographic Information Science (GIScience 2018)

Abstract
Geo-grid algorithms divide a large polygon area into several smaller polygons, which are important for studying or executing a set of operations on underlying topological features of a map. The current geo-grid algorithms divide a large polygon in to a set of smaller but equal size polygons only (e.g. is ArcMaps Fishnet). The time to create a geo-grid is typically proportional to number of smaller polygons created. This raises two problems - (i) They cannot skip unwanted areas (such as water bodies, given about 71% percent of the Earth's surface is water-covered); (ii) They are incognizant to any underlying feature set that requires more deliberation. In this work, we propose a novel dynamically spaced geo-grid segmentation algorithm that overcomes these challenges and provides a computationally optimal output for borderline cases of an uneven polygon. Our method uses an underlying topological feature of population distributions, from the LandScan Global 2016 dataset, for creating grids as a function of these weighted features. We benchmark our results against available algorithms and found our approach improves geo-grid creation. Later on, we demonstrate the proposed approach is more effective in harvesting Points of Interest data from a crowd-sourced platform.
Cite as

Kelly Sims, Gautam Thakur, Kevin Sparks, Marie Urban, Amy Rose, and Robert Stewart. Dynamically-Spaced Geo-Grid Segmentation for Weighted Point Sampling on a Polygon Map Layer (Short Paper). In 10th International Conference on Geographic Information Science (GIScience 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 114, pp. 58:1-58:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{sims_et_al:LIPIcs.GISCIENCE.2018.58,
  author =	{Sims, Kelly and Thakur, Gautam and Sparks, Kevin and Urban, Marie and Rose, Amy and Stewart, Robert},
  title =	{{Dynamically-Spaced Geo-Grid Segmentation for Weighted Point Sampling on a Polygon Map Layer}},
  booktitle =	{10th International Conference on Geographic Information Science (GIScience 2018)},
  pages =	{58:1--58:7},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-083-5},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{114},
  editor =	{Winter, Stephan and Griffin, Amy and Sester, Monika},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.GISCIENCE.2018.58},
  URN =		{urn:nbn:de:0030-drops-93860},
  doi =		{10.4230/LIPIcs.GISCIENCE.2018.58},
  annote =	{Keywords: geofence, geo-grid, quadtree, points of interest (POI), volunteered geographic information (VGI)}
}
  • Refine by Author
  • 1 Chardonnet, Kostia
  • 1 Kavvos, G. A.
  • 1 Kelly, Robert
  • 1 Lemonnier, Louis
  • 1 Maguire, Phil
  • Show More...

  • Refine by Classification
  • 1 Computing methodologies → Concurrent algorithms
  • 1 Theory of computation → Categorical semantics
  • 1 Theory of computation → Divide and conquer
  • 1 Theory of computation → Modal and temporal logics
  • 1 Theory of computation → Program semantics

  • Refine by Keyword
  • 1 Computability
  • 1 Denotational Semantics
  • 1 Kripke semantics
  • 1 Reversible programming
  • 1 Robin Hood Hashing
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2024
  • 1 2018
  • 1 2019

© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact