6 Search Results for "Hoshino, Naohiko"


Document
On the Lattice of Program Metrics

Authors: Ugo Dal Lago, Naohiko Hoshino, and Paolo Pistone

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)


Abstract
In this paper we are concerned with understanding the nature of program metrics for calculi with higher-order types, seen as natural generalizations of program equivalences. Some of the metrics we are interested in are well-known, such as those based on the interpretation of terms in metric spaces and those obtained by generalizing observational equivalence. We also introduce a new one, called the interactive metric, built by applying the well-known Int-Construction to the category of metric complete partial orders. Our aim is then to understand how these metrics relate to each other, i.e., whether and in which cases one such metric refines another, in analogy with corresponding well-studied problems about program equivalences. The results we obtain are twofold. We first show that the metrics of semantic origin, i.e., the denotational and interactive ones, lie in between the observational and equational metrics and that in some cases, these inclusions are strict. Then, we give a result about the relationship between the denotational and interactive metrics, revealing that the former is less discriminating than the latter. All our results are given for a linear lambda-calculus, and some of them can be generalized to calculi with graded comonads, in the style of Fuzz.

Cite as

Ugo Dal Lago, Naohiko Hoshino, and Paolo Pistone. On the Lattice of Program Metrics. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 20:1-20:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{dallago_et_al:LIPIcs.FSCD.2023.20,
  author =	{Dal Lago, Ugo and Hoshino, Naohiko and Pistone, Paolo},
  title =	{{On the Lattice of Program Metrics}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{20:1--20:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.20},
  URN =		{urn:nbn:de:0030-drops-180049},
  doi =		{10.4230/LIPIcs.FSCD.2023.20},
  annote =	{Keywords: Metrics, Lambda Calculus, Linear Types}
}
Document
Planar Realizability via Left and Right Applications

Authors: Haruka Tomita

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)


Abstract
We introduce a class of applicative structures called bi-BDI-algebras. Bi-BDI-algebras are generalizations of partial combinatory algebras and BCI-algebras, and feature two sorts of applications (left and right applications). Applying the categorical realizability construction to bi-BDI-algebras, we obtain monoidal bi-closed categories of assemblies (as well as of modest sets). We further investigate two kinds of comonadic applicative morphisms on bi-BDI-algebras as non-symmetric analogues of linear combinatory algebras, which induce models of exponential and exchange modalities on non-symmetric linear logics.

Cite as

Haruka Tomita. Planar Realizability via Left and Right Applications. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 35:1-35:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{tomita:LIPIcs.CSL.2022.35,
  author =	{Tomita, Haruka},
  title =	{{Planar Realizability via Left and Right Applications}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{35:1--35:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.35},
  URN =		{urn:nbn:de:0030-drops-157558},
  doi =		{10.4230/LIPIcs.CSL.2022.35},
  annote =	{Keywords: Realizability, combinatory algebra, monoidal bi-closed category, exponential modality, exchange modality}
}
Document
Realizability Without Symmetry

Authors: Haruka Tomita

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)


Abstract
In categorical realizability, it is common to construct categories of assemblies and modest sets from applicative structures. In this paper, we introduce several classes of applicative structures and apply the categorical realizability construction to them. Then we obtain closed multicategories, closed categories and skew closed categories, which are more general categorical structures than Cartesian closed categories and symmetric monoidal closed categories. Moreover, we give the necessary and sufficient conditions for obtaining closed multicategories and closed categories of assemblies.

Cite as

Haruka Tomita. Realizability Without Symmetry. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 38:1-38:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{tomita:LIPIcs.CSL.2021.38,
  author =	{Tomita, Haruka},
  title =	{{Realizability Without Symmetry}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{38:1--38:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.38},
  URN =		{urn:nbn:de:0030-drops-134729},
  doi =		{10.4230/LIPIcs.CSL.2021.38},
  annote =	{Keywords: Realizability, combinatory algebra, closed multicategory, closed category, skew closed category}
}
Document
The Axiom of Choice in Cartesian Bicategories

Authors: Filippo Bonchi, Jens Seeber, and Paweł Sobociński

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)


Abstract
We argue that cartesian bicategories, often used as a general categorical algebra of relations, are also a natural setting for the study of the axiom of choice (AC). In this setting, AC manifests itself as an inequation asserting that every total relation contains a map. The generality of cartesian bicategories allows us to separate this formulation from other set-theoretically equivalent properties, for instance that epimorphisms split. Moreover, via a classification result, we show that cartesian bicategories satisfying choice tend to be those that arise from bicategories of spans.

Cite as

Filippo Bonchi, Jens Seeber, and Paweł Sobociński. The Axiom of Choice in Cartesian Bicategories. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CALCO.2019.15,
  author =	{Bonchi, Filippo and Seeber, Jens and Soboci\'{n}ski, Pawe{\l}},
  title =	{{The Axiom of Choice in Cartesian Bicategories}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{15:1--15:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.15},
  URN =		{urn:nbn:de:0030-drops-114439},
  doi =		{10.4230/LIPIcs.CALCO.2019.15},
  annote =	{Keywords: Cartesian bicategories, Axiom of choice, string diagrams}
}
Document
On the Expressivity of Linear Recursion Schemes

Authors: Pierre Clairambault and Andrzej S. Murawski

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)


Abstract
We investigate the expressive power of higher-order recursion schemes (HORS) restricted to linear types. Two formalisms are considered: multiplicative additive HORS (MAHORS), which feature both linear function types and products, and multiplicative HORS (MHORS), based on linear function types only. For MAHORS, we establish an equi-expressivity result with a variant of tree-stack automata. Consequently, we can show that MAHORS are strictly more expressive than first-order HORS, that they are incomparable with second-order HORS, and that the associated branch languages lie at the third level of the collapsible pushdown hierarchy. In the multiplicative case, we show that MHORS are equivalent to a special kind of pushdown automata. It follows that any MHORS can be translated to an equivalent first-order MHORS in polynomial time. Further, we show that MHORS generate regular trees and can be translated to equivalent order-0 HORS in exponential time. Consequently, MHORS turn out to have the same expressive power as 0-HORS but they can be exponentially more concise. Our results are obtained through a combination of techniques from game semantics, the geometry of interaction and automata theory.

Cite as

Pierre Clairambault and Andrzej S. Murawski. On the Expressivity of Linear Recursion Schemes. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 50:1-50:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{clairambault_et_al:LIPIcs.MFCS.2019.50,
  author =	{Clairambault, Pierre and Murawski, Andrzej S.},
  title =	{{On the Expressivity of Linear Recursion Schemes}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{50:1--50:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.50},
  URN =		{urn:nbn:de:0030-drops-109945},
  doi =		{10.4230/LIPIcs.MFCS.2019.50},
  annote =	{Keywords: higher-order recursion schemes, linear logic, game semantics, geometry of interaction}
}
Document
Coalgebras and Higher-Order Computation: a GoI Approach

Authors: Ichiro Hasuo

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)


Abstract
Girard's geometry of interaction (GoI) can be seen---in one practical aspect of it---as a compositional compilation method from functional programs to sequential machines. There tokens move around and express interactions between (parts of) programs. Intrigued by the combination of abstract structures and concrete dynamics in GoI, our line of work has aimed at exploiting, in GoI, results from the theory of coalgebra---a categorical abstraction of state-based transition systems that has found its use principally in concurrency theory. Such reinforced connection between higher-order computation and state-based dynamics is made possible thanks to an elegant categorical axiomatization of GoI by Abramsky, Haghverdi and Scott, where traced monoidal categories are identified to be the essential structure behind. In the talk I shall lay out these basic ideas, together with some of our results on: GoI semantics for a quantum programming language; and our ``memoryful'' extension of GoI with algebraic effects. The talk is based on my joint work with my colleague Naohiko Hoshino (RIMS, Kyoto Univer- sity) and my (former) students Koko Muroya (University of Birmingham) and Toshiki Kataoka (University of Tokyo), to whom I owe special thanks.

Cite as

Ichiro Hasuo. Coalgebras and Higher-Order Computation: a GoI Approach. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 2:1-2:2, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{hasuo:LIPIcs.FSCD.2016.2,
  author =	{Hasuo, Ichiro},
  title =	{{Coalgebras and Higher-Order Computation: a GoI Approach}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{2:1--2:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.2},
  URN =		{urn:nbn:de:0030-drops-59698},
  doi =		{10.4230/LIPIcs.FSCD.2016.2},
  annote =	{Keywords: functional programming, geometry of interaction, categorical semantics, coalgebra}
}
  • Refine by Author
  • 2 Tomita, Haruka
  • 1 Bonchi, Filippo
  • 1 Clairambault, Pierre
  • 1 Dal Lago, Ugo
  • 1 Hasuo, Ichiro
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Categorical semantics
  • 2 Theory of computation → Program semantics
  • 1 Theory of computation → Logic

  • Refine by Keyword
  • 2 Realizability
  • 2 combinatory algebra
  • 2 geometry of interaction
  • 1 Axiom of choice
  • 1 Cartesian bicategories
  • Show More...

  • Refine by Type
  • 6 document

  • Refine by Publication Year
  • 2 2019
  • 1 2016
  • 1 2021
  • 1 2022
  • 1 2023

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail