45 Search Results for "Kobayashi, Naoki"

Volume

LIPIcs, Volume 195

6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference)

Editors: Naoki Kobayashi

Document
DOI: 10.4230/LIPIcs.CONCUR.2021.34
Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes

Authors: Patrick Baillot, Alexis Ghyselen, and Naoki Kobayashi

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
We address the problem of analysing the complexity of concurrent programs written in Pi-calculus. We are interested in parallel complexity, or span, understood as the execution time in a model with maximal parallelism. A type system for parallel complexity has been recently proposed by the first two authors but it is too imprecise for non-linear channels and cannot analyse some concurrent processes. Aiming for a more precise analysis, we design a type system which builds on the concepts of sized types and usages. The sized types allow us to parametrize the complexity by the size of inputs, and the usages allow us to achieve a kind of rely-guarantee reasoning on the timing each process communicates with its environment. We prove that our new type system soundly estimates the parallel complexity, and show through examples that it is often more precise than the previous type system of the first two authors.
Cite as

Patrick Baillot, Alexis Ghyselen, and Naoki Kobayashi. Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 34:1-34:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{baillot_et_al:LIPIcs.CONCUR.2021.34,
  author =	{Baillot, Patrick and Ghyselen, Alexis and Kobayashi, Naoki},
  title =	{{Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{34:1--34:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.34},
  URN =		{urn:nbn:de:0030-drops-144111},
  doi =		{10.4230/LIPIcs.CONCUR.2021.34},
  annote =	{Keywords: Type Systems, Pi-calculus, Process Calculi, Complexity Analysis, Usages, Sized Types}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.FSCD.2021
LIPIcs, Volume 195, FSCD 2021, Complete Volume

Authors: Naoki Kobayashi

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
LIPIcs, Volume 195, FSCD 2021, Complete Volume
Cite as

6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 1-634, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Proceedings{kobayashi:LIPIcs.FSCD.2021,
  title =	{{LIPIcs, Volume 195, FSCD 2021, Complete Volume}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{1--634},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021},
  URN =		{urn:nbn:de:0030-drops-142371},
  doi =		{10.4230/LIPIcs.FSCD.2021},
  annote =	{Keywords: LIPIcs, Volume 195, FSCD 2021, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.FSCD.2021.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Naoki Kobayashi

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 0:i-0:xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{kobayashi:LIPIcs.FSCD.2021.0,
  author =	{Kobayashi, Naoki},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{0:i--0:xvi},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.0},
  URN =		{urn:nbn:de:0030-drops-142382},
  doi =		{10.4230/LIPIcs.FSCD.2021.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2021.1
Duality in Action (Invited Talk)

Authors: Paul Downen and Zena M. Ariola

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
The duality between "true" and "false" is a hallmark feature of logic. We show how this duality can be put to use in the theory and practice of programming languages and their implementations, too. Starting from a foundation of constructive logic as dialogues, we illustrate how it describes a symmetric language for computation, and survey several applications of the dualities found therein.
Cite as

Paul Downen and Zena M. Ariola. Duality in Action (Invited Talk). In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 1:1-1:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{downen_et_al:LIPIcs.FSCD.2021.1,
  author =	{Downen, Paul and Ariola, Zena M.},
  title =	{{Duality in Action}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{1:1--1:32},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.1},
  URN =		{urn:nbn:de:0030-drops-142390},
  doi =		{10.4230/LIPIcs.FSCD.2021.1},
  annote =	{Keywords: Duality, Logic, Curry-Howard, Sequent Calculus, Rewriting, Compilation}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2021.2
Completion and Reduction Orders (Invited Talk)

Authors: Nao Hirokawa

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
We present three techniques for improving the Knuth-Bendix completion procedure and its variants: An order extension by semantic labeling, a new confluence criterion for terminating term rewrite systems, and inter-reduction for maximal completion.
Cite as

Nao Hirokawa. Completion and Reduction Orders (Invited Talk). In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 2:1-2:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{hirokawa:LIPIcs.FSCD.2021.2,
  author =	{Hirokawa, Nao},
  title =	{{Completion and Reduction Orders}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{2:1--2:9},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.2},
  URN =		{urn:nbn:de:0030-drops-142403},
  doi =		{10.4230/LIPIcs.FSCD.2021.2},
  annote =	{Keywords: term rewriting, completion, reduction order}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2021.3
Process-As-Formula Interpretation: A Substructural Multimodal View (Invited Talk)

Authors: Elaine Pimentel, Carlos Olarte, and Vivek Nigam

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
In this survey, we show how the processes-as-formulas interpretation, where computations and proof-search are strongly connected, can be used to specify different concurrent behaviors as logical theories. The proposed interpretation is parametric and modular, and it faithfully captures behaviors such as: Linear and spatial computations, epistemic state of agents, and preferences in concurrent systems. The key for this modularity is the incorporation of multimodalities in a resource aware logic, together with the ability of quantifying on such modalities. We achieve tight adequacy theorems by relying on a focusing discipline that allows for controlling the proof search process.
Cite as

Elaine Pimentel, Carlos Olarte, and Vivek Nigam. Process-As-Formula Interpretation: A Substructural Multimodal View (Invited Talk). In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{pimentel_et_al:LIPIcs.FSCD.2021.3,
  author =	{Pimentel, Elaine and Olarte, Carlos and Nigam, Vivek},
  title =	{{Process-As-Formula Interpretation: A Substructural Multimodal View}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{3:1--3:21},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.3},
  URN =		{urn:nbn:de:0030-drops-142414},
  doi =		{10.4230/LIPIcs.FSCD.2021.3},
  annote =	{Keywords: Linear logic, proof theory, process calculi}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2021.4
Some Formal Structures in Probability (Invited Talk)

Authors: Sam Staton

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
This invited talk will discuss how developments in the Formal Structures for Computation and Deduction can also suggest new directions for the foundations of probability theory. I plan to focus on two aspects: abstraction, and laziness. I plan to highlight two challenges: higher-order random functions, and stochastic memoization.
Cite as

Sam Staton. Some Formal Structures in Probability (Invited Talk). In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 4:1-4:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{staton:LIPIcs.FSCD.2021.4,
  author =	{Staton, Sam},
  title =	{{Some Formal Structures in Probability}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{4:1--4:4},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.4},
  URN =		{urn:nbn:de:0030-drops-142421},
  doi =		{10.4230/LIPIcs.FSCD.2021.4},
  annote =	{Keywords: Probabilistic programming}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.5
The Expressive Power of One Variable Used Once: The Chomsky Hierarchy and First-Order Monadic Constructor Rewriting

Authors: Jakob Grue Simonsen

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
We study the implicit computational complexity of constructor term rewriting systems where every function and constructor symbol is unary or nullary. Surprisingly, adding simple and natural constraints to rule formation yields classes of systems that accept exactly the four classes of languages in the Chomsky hierarchy.
Cite as

Jakob Grue Simonsen. The Expressive Power of One Variable Used Once: The Chomsky Hierarchy and First-Order Monadic Constructor Rewriting. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{simonsen:LIPIcs.FSCD.2021.5,
  author =	{Simonsen, Jakob Grue},
  title =	{{The Expressive Power of One Variable Used Once: The Chomsky Hierarchy and First-Order Monadic Constructor Rewriting}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{5:1--5:17},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.5},
  URN =		{urn:nbn:de:0030-drops-142439},
  doi =		{10.4230/LIPIcs.FSCD.2021.5},
  annote =	{Keywords: Constructor term rewriting, Chomsky Hierarchy, Implicit Complexity}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.6
Church’s Semigroup Is Sq-Universal

Authors: Rick Statman

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
We prove Church’s lambda calculus semigroup is sq-universal.
Cite as

Rick Statman. Church’s Semigroup Is Sq-Universal. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 6:1-6:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{statman:LIPIcs.FSCD.2021.6,
  author =	{Statman, Rick},
  title =	{{Church’s Semigroup Is Sq-Universal}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{6:1--6:6},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.6},
  URN =		{urn:nbn:de:0030-drops-142448},
  doi =		{10.4230/LIPIcs.FSCD.2021.6},
  annote =	{Keywords: lambda calculus, Church’s semigroup, sq-universal}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.7
Call-By-Value, Again!

Authors: Axel Kerinec, Giulio Manzonetto, and Simona Ronchi Della Rocca

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
The quest for a fully abstract model of the call-by-value λ-calculus remains crucial in programming language theory, and constitutes an ongoing line of research. While a model enjoying this property has not been found yet, this interesting problem acts as a powerful motivation for investigating classes of models, studying the associated theories and capturing operational properties semantically. We study a relational model presented as a relevant intersection type system, where intersection is in general non-idempotent, except for an idempotent element that is injected in the system. This model is adequate, equates many λ-terms that are indeed equivalent in the maximal observational theory, and satisfies an Approximation Theorem w.r.t. a system of approximants representing finite pieces of call-by-value Böhm trees. We show that these tools can be used for characterizing the most significant properties of the calculus - namely valuability, potential valuability and solvability - both semantically, through the notion of approximants, and logically, by means of the type assignment system. We mainly focus on the characterizations of solvability, as they constitute an original result. Finally, we prove the decidability of the inhabitation problem for our type system by exhibiting a non-deterministic algorithm, which is proven sound, correct and terminating.
Cite as

Axel Kerinec, Giulio Manzonetto, and Simona Ronchi Della Rocca. Call-By-Value, Again!. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{kerinec_et_al:LIPIcs.FSCD.2021.7,
  author =	{Kerinec, Axel and Manzonetto, Giulio and Ronchi Della Rocca, Simona},
  title =	{{Call-By-Value, Again!}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{7:1--7:18},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.7},
  URN =		{urn:nbn:de:0030-drops-142458},
  doi =		{10.4230/LIPIcs.FSCD.2021.7},
  annote =	{Keywords: \lambda-calculus, call-by-value, intersection types, solvability, inhabitation}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.8
Predicative Aspects of Order Theory in Univalent Foundations

Authors: Tom de Jong and Martín Hötzel Escardó

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
We investigate predicative aspects of order theory in constructive univalent foundations. By predicative and constructive, we respectively mean that we do not assume Voevodsky’s propositional resizing axioms or excluded middle. Our work complements existing work on predicative mathematics by exploring what cannot be done predicatively in univalent foundations. Our first main result is that nontrivial (directed or bounded) complete posets are necessarily large. That is, if such a nontrivial poset is small, then weak propositional resizing holds. It is possible to derive full propositional resizing if we strengthen nontriviality to positivity. The distinction between nontriviality and positivity is analogous to the distinction between nonemptiness and inhabitedness. We prove our results for a general class of posets, which includes directed complete posets, bounded complete posets and sup-lattices, using a technical notion of a δ_V-complete poset. We also show that nontrivial locally small δ_V-complete posets necessarily lack decidable equality. Specifically, we derive weak excluded middle from assuming a nontrivial locally small δ_V-complete poset with decidable equality. Moreover, if we assume positivity instead of nontriviality, then we can derive full excluded middle. Secondly, we show that each of Zorn’s lemma, Tarski’s greatest fixed point theorem and Pataraia’s lemma implies propositional resizing. Hence, these principles are inherently impredicative and a predicative development of order theory must therefore do without them. Finally, we clarify, in our predicative setting, the relation between the traditional definition of sup-lattice that requires suprema for all subsets and our definition that asks for suprema of all small families.
Cite as

Tom de Jong and Martín Hötzel Escardó. Predicative Aspects of Order Theory in Univalent Foundations. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{dejong_et_al:LIPIcs.FSCD.2021.8,
  author =	{de Jong, Tom and Escard\'{o}, Mart{\'\i}n H\"{o}tzel},
  title =	{{Predicative Aspects of Order Theory in Univalent Foundations}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{8:1--8:18},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.8},
  URN =		{urn:nbn:de:0030-drops-142461},
  doi =		{10.4230/LIPIcs.FSCD.2021.8},
  annote =	{Keywords: order theory, constructivity, predicativity, univalent foundations}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.9
A Strong Call-By-Need Calculus

Authors: Thibaut Balabonski, Antoine Lanco, and Guillaume Melquiond

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
We present a call-by-need λ-calculus that enables strong reduction (that is, reduction inside the body of abstractions) and guarantees that arguments are only evaluated if needed and at most once. This calculus uses explicit substitutions and subsumes the existing strong-call-by-need strategy, but allows for more reduction sequences, and often shorter ones, while preserving the neededness. The calculus is shown to be normalizing in a strong sense: Whenever a λ-term t admits a normal form n in the λ-calculus, then any reduction sequence from t in the calculus eventually reaches a representative of the normal form n. We also exhibit a restriction of this calculus that has the diamond property and that only performs reduction sequences of minimal length, which makes it systematically better than the existing strategy. We have used the Abella proof assistant to formalize part of this calculus, and discuss how this experiment affected its design.
Cite as

Thibaut Balabonski, Antoine Lanco, and Guillaume Melquiond. A Strong Call-By-Need Calculus. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 9:1-9:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{balabonski_et_al:LIPIcs.FSCD.2021.9,
  author =	{Balabonski, Thibaut and Lanco, Antoine and Melquiond, Guillaume},
  title =	{{A Strong Call-By-Need Calculus}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{9:1--9: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.9},
  URN =		{urn:nbn:de:0030-drops-142477},
  doi =		{10.4230/LIPIcs.FSCD.2021.9},
  annote =	{Keywords: strong reduction, call-by-need, evaluation strategy, normalization}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.10
A Bicategorical Model for Finite Nondeterminism

Authors: Zeinab Galal

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
Finiteness spaces were introduced by Ehrhard as a refinement of the relational model of linear logic. A finiteness space is a set equipped with a class of finitary subsets which can be thought of being subsets that behave like finite sets. A morphism between finiteness spaces is a relation that preserves the finitary structure. This model provided a semantics for finite non-determism and it gave a semantical motivation for differential linear logic and the syntactic notion of Taylor expansion. In this paper, we present a bicategorical extension of this construction where the relational model is replaced with the model of generalized species of structures introduced by Fiore et al. and the finiteness property now relies on finite presentability.
Cite as

Zeinab Galal. A Bicategorical Model for Finite Nondeterminism. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 10:1-10:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{galal:LIPIcs.FSCD.2021.10,
  author =	{Galal, Zeinab},
  title =	{{A Bicategorical Model for Finite Nondeterminism}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{10:1--10:17},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.10},
  URN =		{urn:nbn:de:0030-drops-142487},
  doi =		{10.4230/LIPIcs.FSCD.2021.10},
  annote =	{Keywords: Differential linear logic, Species of structures, Finiteness, Bicategorical semantics}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.11
Failure of Cut-Elimination in the Cyclic Proof System of Bunched Logic with Inductive Propositions

Authors: Kenji Saotome, Koji Nakazawa, and Daisuke Kimura

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
Cyclic proof systems are sequent-calculus style proof systems that allow circular structures representing induction, and they are considered suitable for automated inductive reasoning. However, Kimura et al. have shown that the cyclic proof system for the symbolic heap separation logic does not satisfy the cut-elimination property, one of the most fundamental properties of proof systems. This paper proves that the cyclic proof system for the bunched logic with only nullary inductive predicates does not satisfy the cut-elimination property. It is hard to adapt the existing proof technique chasing contradictory paths in cyclic proofs since the bunched logic contains the structural rules. This paper proposes a new proof technique called proof unrolling. This technique can be adapted to the symbolic heap separation logic, and it shows that the cut-elimination fails even if we restrict the inductive predicates to nullary ones.
Cite as

Kenji Saotome, Koji Nakazawa, and Daisuke Kimura. Failure of Cut-Elimination in the Cyclic Proof System of Bunched Logic with Inductive Propositions. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 11:1-11:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{saotome_et_al:LIPIcs.FSCD.2021.11,
  author =	{Saotome, Kenji and Nakazawa, Koji and Kimura, Daisuke},
  title =	{{Failure of Cut-Elimination in the Cyclic Proof System of Bunched Logic with Inductive Propositions}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{11:1--11:14},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.11},
  URN =		{urn:nbn:de:0030-drops-142494},
  doi =		{10.4230/LIPIcs.FSCD.2021.11},
  annote =	{Keywords: cyclic proofs, cut-elimination, bunched logic, separation logic, linear logic}
}
  • Refine by Author
  • 12 Kobayashi, Naoki
  • 5 Asada, Kazuyuki
  • 5 Tsukada, Takeshi
  • 2 Asai, Kenichi
  • 2 Das, Anupam
  • Show More...

  • Refine by Classification
  • 10 Theory of computation → Equational logic and rewriting
  • 6 Theory of computation → Proof theory
  • 6 Theory of computation → Type theory
  • 4 Theory of computation → Denotational semantics
  • 4 Theory of computation → Lambda calculus
  • Show More...

  • Refine by Keyword
  • 4 intersection types
  • 3 linear logic
  • 2 Higher-order model checking
  • 2 Kruskal's tree theorem
  • 2 confluence
  • Show More...

  • Refine by Type
  • 44 document
  • 1 volume

  • Refine by Publication Year
  • 37 2021
  • 3 2020
  • 2 2017
  • 1 2013
  • 1 2016
  • Show More...

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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact