Volume
LIPIcs, Volume 195
6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Formal Structures for Computation and Deduction (FSCD)
Publication Details
- published at: 2021-07-06
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-191-7
- DBLP: db/conf/rta/fscd2021
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 195, FSCD 2021, Complete Volume
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.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
Front Matter, Table of Contents, Preface, Conference Organization
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.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
Duality in Action (Invited Talk)
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.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
Completion and Reduction Orders (Invited Talk)
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.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
Process-As-Formula Interpretation: A Substructural Multimodal View (Invited Talk)
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.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
Some Formal Structures in Probability (Invited Talk)
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.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
The Expressive Power of One Variable Used Once: The Chomsky Hierarchy and First-Order Monadic Constructor Rewriting
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.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
Church’s Semigroup Is Sq-Universal
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.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
Call-By-Value, Again!
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.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
Predicative Aspects of Order Theory in Univalent Foundations
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.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
A Strong Call-By-Need Calculus
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.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
A Bicategorical Model for Finite Nondeterminism
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.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
Failure of Cut-Elimination in the Cyclic Proof System of Bunched Logic with Inductive Propositions
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.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}
}
Document
A Functional Abstraction of Typed Invocation Contexts
Abstract
In their paper "A Functional Abstraction of Typed Contexts", Danvy and Filinski show how to derive a type system of the shift and reset operators from a CPS translation. In this paper, we show how this method scales to Felleisen’s control and prompt operators. Compared to shift and reset, control and prompt exhibit a more dynamic behavior, in that they can manipulate a trail of contexts surrounding the invocation of captured continuations. Our key observation is that, by adopting a functional representation of trails in the CPS translation, we can derive a type system that allows fine-grain reasoning of programs involving manipulation of invocation contexts.
Cite as
Youyou Cong, Chiaki Ishio, Kaho Honda, and Kenichi Asai. A Functional Abstraction of Typed Invocation Contexts. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{cong_et_al:LIPIcs.FSCD.2021.12,
author = {Cong, Youyou and Ishio, Chiaki and Honda, Kaho and Asai, Kenichi},
title = {{A Functional Abstraction of Typed Invocation Contexts}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {12:1--12: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.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.12},
URN = {urn:nbn:de:0030-drops-142507},
doi = {10.4230/LIPIcs.FSCD.2021.12},
annote = {Keywords: delimited continuations, control operators, control and prompt, CPS translation, type system}
}
Document
Beth Semantics and Labelled Deduction for Intuitionistic Sentential Calculus with Identity
Abstract
In this paper we consider the intuitionistic sentential calculus with Suszko’s identity (ISCI). After recalling the basic concepts of the logic and its associated Hilbert proof system, we introduce a new sound and complete class of models for ISCI which can be viewed as algebraic counterparts (and extensions) of sheaf-theoretic topological models of intuitionistic logic. We use this new class of models, called Beth semantics for ISCI, to derive a first labelled sequent calculus and show its adequacy w.r.t. the standard Hilbert axiomatization of ISCI. This labelled proof system, like all other current proof systems for ISCI that we know of, does not enjoy the subformula property, which is problematic for achieving termination. We therefore introduce a second labelled sequent calculus in which the standard rules for identity are replaced with new special rules and show that this second calculus admits cut-elimination. Finally, using a key regularity property of the forcing relation in Beth models, we show that the eigenvariable condition can be dropped, thus leading to the termination and decidability results.
Cite as
Didier Galmiche, Marta Gawek, and Daniel Méry. Beth Semantics and Labelled Deduction for Intuitionistic Sentential Calculus with Identity. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 13:1-13:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{galmiche_et_al:LIPIcs.FSCD.2021.13,
author = {Galmiche, Didier and Gawek, Marta and M\'{e}ry, Daniel},
title = {{Beth Semantics and Labelled Deduction for Intuitionistic Sentential Calculus with Identity}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {13:1--13: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.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.13},
URN = {urn:nbn:de:0030-drops-142516},
doi = {10.4230/LIPIcs.FSCD.2021.13},
annote = {Keywords: Algebraic Semantics, Beth Models, Labelled Deduction, Intuitionistic Logic}
}
Document
New Minimal Linear Inferences in Boolean Logic Independent of Switch and Medial
Abstract
A linear inference is a valid inequality of Boolean algebra in which each variable occurs at most once on each side. Equivalently, it is a linear rewrite rule on Boolean terms that constitutes a valid implication. Linear inferences have played a significant role in structural proof theory, in particular in models of substructural logics and in normalisation arguments for deep inference proof systems.
Systems of linear logic and, later, deep inference are founded upon two particular linear inferences, switch : x ∧ (y ∨ z) → (x ∧ y) ∨ z, and medial : (w ∧ x) ∨ (y ∧ z) → (w ∨ y) ∧ (x ∨ z). It is well-known that these two are not enough to derive all linear inferences (even modulo all valid linear equations), but beyond this little more is known about the structure of linear inferences in general. In particular despite recurring attention in the literature, the smallest linear inference not derivable under switch and medial ("switch-medial-independent") was not previously known.
In this work we leverage recently developed graphical representations of linear formulae to build an implementation that is capable of more efficiently searching for switch-medial-independent inferences. We use it to find two "minimal" 8-variable independent inferences and also prove that no smaller ones exist; in contrast, a previous approach based directly on formulae reached computational limits already at 7 variables. One of these new inferences derives some previously found independent linear inferences. The other exhibits structure seemingly beyond the scope of previous approaches we are aware of; in particular, its existence contradicts a conjecture of Das and Strassburger.
Cite as
Anupam Das and Alex A. Rice. New Minimal Linear Inferences in Boolean Logic Independent of Switch and Medial. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{das_et_al:LIPIcs.FSCD.2021.14,
author = {Das, Anupam and Rice, Alex A.},
title = {{New Minimal Linear Inferences in Boolean Logic Independent of Switch and Medial}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {14:1--14:19},
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/entities/document/10.4230/LIPIcs.FSCD.2021.14},
URN = {urn:nbn:de:0030-drops-142525},
doi = {10.4230/LIPIcs.FSCD.2021.14},
annote = {Keywords: rewriting, linear inference, proof theory, linear logic, implementation}
}
Document
A Modular Associative Commutative (AC) Congruence Closure Algorithm
Abstract
Algorithms for computing congruence closure of ground equations over uninterpreted symbols and interpreted symbols satisfying associativity and commutativity (AC) properties are proposed. The algorithms are based on a framework for computing the congruence closure by abstracting nonflat terms by constants as proposed first in Kapur’s congruence closure algorithm (RTA97). The framework is general, flexible, and has been extended also to develop congruence closure algorithms for the cases when associative-commutative function symbols can have additional properties including idempotency, nilpotency and/or have identities, as well as their various combinations. The algorithms are modular; their correctness and termination proofs are simple, exploiting modularity. Unlike earlier algorithms, the proposed algorithms neither rely on complex AC compatible well-founded orderings on nonvariable terms nor need to use the associative-commutative unification and extension rules in completion for generating canonical rewrite systems for congruence closures. They are particularly suited for integrating into Satisfiability modulo Theories (SMT) solvers.
Cite as
Deepak Kapur. A Modular Associative Commutative (AC) Congruence Closure Algorithm. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 15:1-15:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{kapur:LIPIcs.FSCD.2021.15,
author = {Kapur, Deepak},
title = {{A Modular Associative Commutative (AC) Congruence Closure Algorithm}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {15:1--15: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.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.15},
URN = {urn:nbn:de:0030-drops-142530},
doi = {10.4230/LIPIcs.FSCD.2021.15},
annote = {Keywords: Congruence Closure, Associative and Commutative, Word Problems, Finitely Presented Algebras, Equational Theories}
}
Document
Derivation of a Virtual Machine For Four Variants of Delimited-Control Operators
Abstract
This paper derives an abstract machine and a virtual machine for the λ-calculus with four variants of delimited-control operators: shift/reset, control/prompt, shift₀/reset₀, and control₀/prompt₀. Starting from Shan’s definitional interpreter for the four operators, we successively apply various meaning-preserving transformations. Both trails of invocation contexts (needed for control and control₀) and metacontinuations (needed for shift₀ and control₀) are defunctionalized and eventually represented as a list of stack frames. The resulting virtual machine clearly models not only how the control operators and captured continuations behave but also when and which portion of stack frames is copied to the heap.
Cite as
Maika Fujii and Kenichi Asai. Derivation of a Virtual Machine For Four Variants of Delimited-Control Operators. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 16:1-16:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{fujii_et_al:LIPIcs.FSCD.2021.16,
author = {Fujii, Maika and Asai, Kenichi},
title = {{Derivation of a Virtual Machine For Four Variants of Delimited-Control Operators}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {16:1--16:19},
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/entities/document/10.4230/LIPIcs.FSCD.2021.16},
URN = {urn:nbn:de:0030-drops-142547},
doi = {10.4230/LIPIcs.FSCD.2021.16},
annote = {Keywords: delimited-control operators, functional derivation, CPS transformation, defunctionalization, abstract machine, virtual machine}
}
Document
Positional Injectivity for Innocent Strategies
Abstract
In asynchronous games, Melliès proved that innocent strategies are positional: their behaviour only depends on the position, not the temporal order used to reach it. This insightful result shaped our understanding of the link between dynamic (i.e. game) and static (i.e. relational) semantics.
In this paper, we investigate the positionality of innocent strategies in the traditional setting of Hyland-Ong-Nickau-Coquand pointer games. We show that though innocent strategies are not positional, total finite innocent strategies still enjoy a key consequence of positionality, namely positional injectivity: they are entirely determined by their positions. Unfortunately, this does not hold in general: we show a counter-example if finiteness and totality are lifted. For finite partial strategies we leave the problem open; we show however the partial result that two strategies with the same positions must have the same P-views of maximal length.
Cite as
Lison Blondeau-Patissier and Pierre Clairambault. Positional Injectivity for Innocent Strategies. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 17:1-17:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{blondeaupatissier_et_al:LIPIcs.FSCD.2021.17,
author = {Blondeau-Patissier, Lison and Clairambault, Pierre},
title = {{Positional Injectivity for Innocent Strategies}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {17:1--17: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/entities/document/10.4230/LIPIcs.FSCD.2021.17},
URN = {urn:nbn:de:0030-drops-142555},
doi = {10.4230/LIPIcs.FSCD.2021.17},
annote = {Keywords: Game Semantics, Innocence, Relational Semantics, Positionality}
}
Document
Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq
Abstract
We present an alternate undecidability proof for entailment in (intuitionistic) multiplicative sub-exponential linear logic (MSELL). We contribute the result and its mechanised proof to the Coq library of synthetic undecidability. The result crucially relies on the undecidability of the halting problem for two counters Minsky machines, which we also hand out to the library. As a seed of undecidability, we start from FRACTRAN halting which we (many-one) reduce to Minsky machines termination by implementing Euclidean division using two counters only. We then give an alternate presentation of those two counters machines as sequent rules, where computation is performed by proof-search, and halting reduced to provability. We use this system called non-deterministic two counters Minsky machines to describe and compare both the legacy reduction to linear logic, and the more recent reduction to MSELL. In contrast with that former MSELL undecidability proof, our correctness argument for the reduction uses trivial phase semantics in place of a focused calculus.
Cite as
Dominique Larchey-Wendling. Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{larcheywendling:LIPIcs.FSCD.2021.18,
author = {Larchey-Wendling, Dominique},
title = {{Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {18:1--18:20},
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/entities/document/10.4230/LIPIcs.FSCD.2021.18},
URN = {urn:nbn:de:0030-drops-142568},
doi = {10.4230/LIPIcs.FSCD.2021.18},
annote = {Keywords: Undecidability, computability theory, many-one reduction, Minsky machines, Fractran, sub-exponential linear logic, Coq}
}
Document
An RPO-Based Ordering Modulo Permutation Equations and Its Applications to Rewrite Systems
Abstract
Rewriting modulo equations has been researched for several decades but due to the lack of suitable orderings, there are some limitations to rewriting modulo permutation equations. Given a finite set of permutation equations E, we present a new RPO-based ordering modulo E using (permutation) group actions and their associated orbits. It is an E-compatible reduction ordering on terms with the subterm property and is E-total on ground terms. We also present a completion and ground completion method for rewriting modulo a finite set of permutation equations E using our ordering modulo E. We show that our ground completion modulo E always admits a finite ground convergent (modulo E) rewrite system, which allows us to obtain the decidability of the word problem of ground theories modulo E.
Cite as
Dohan Kim and Christopher Lynch. An RPO-Based Ordering Modulo Permutation Equations and Its Applications to Rewrite Systems. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{kim_et_al:LIPIcs.FSCD.2021.19,
author = {Kim, Dohan and Lynch, Christopher},
title = {{An RPO-Based Ordering Modulo Permutation Equations and Its Applications to Rewrite Systems}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {19:1--19: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.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.19},
URN = {urn:nbn:de:0030-drops-142572},
doi = {10.4230/LIPIcs.FSCD.2021.19},
annote = {Keywords: Recursive Path Ordering, Permutation Equation, Permutation Group, Rewrite System, Completion, Ground Completion}
}
Document
Some Axioms for Mathematics
Abstract
The λΠ-calculus modulo theory is a logical framework in which many logical systems can be expressed as theories. We present such a theory, the theory {U}, where proofs of several logical systems can be expressed. Moreover, we identify a sub-theory of {U} corresponding to each of these systems, and prove that, when a proof in {U} uses only symbols of a sub-theory, then it is a proof in that sub-theory.
Cite as
Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, and François Thiré. Some Axioms for Mathematics. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{blanqui_et_al:LIPIcs.FSCD.2021.20,
author = {Blanqui, Fr\'{e}d\'{e}ric and Dowek, Gilles and Grienenberger, \'{E}milie and Hondet, Gabriel and Thir\'{e}, Fran\c{c}ois},
title = {{Some Axioms for Mathematics}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {20:1--20:19},
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/entities/document/10.4230/LIPIcs.FSCD.2021.20},
URN = {urn:nbn:de:0030-drops-142581},
doi = {10.4230/LIPIcs.FSCD.2021.20},
annote = {Keywords: logical framework, axiomatic theory, dependent types, rewriting, interoperabilty}
}
Document
Non-Deterministic Functions as Non-Deterministic Processes
Abstract
We study encodings of the λ-calculus into the π-calculus in the unexplored case of calculi with non-determinism and failures. On the sequential side, we consider λ^↯_⊕, a new non-deterministic calculus in which intersection types control resources (terms); on the concurrent side, we consider 𝗌π, a π-calculus in which non-determinism and failure rest upon a Curry-Howard correspondence between linear logic and session types. We present a typed encoding of λ^↯_⊕ into 𝗌π and establish its correctness. Our encoding precisely explains the interplay of non-deterministic and fail-prone evaluation in λ^↯_⊕ via typed processes in 𝗌π. In particular, it shows how failures in sequential evaluation (absence/excess of resources) can be neatly codified as interaction protocols.
Cite as
Joseph W. N. Paulus, Daniele Nantes-Sobrinho, and Jorge A. Pérez. Non-Deterministic Functions as Non-Deterministic Processes. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 21:1-21:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{paulus_et_al:LIPIcs.FSCD.2021.21,
author = {Paulus, Joseph W. N. and Nantes-Sobrinho, Daniele and P\'{e}rez, Jorge A.},
title = {{Non-Deterministic Functions as Non-Deterministic Processes}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {21:1--21: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/entities/document/10.4230/LIPIcs.FSCD.2021.21},
URN = {urn:nbn:de:0030-drops-142598},
doi = {10.4230/LIPIcs.FSCD.2021.21},
annote = {Keywords: Resource calculi, \pi-calculus, intersection types, session types, linear logic}
}
Document
Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor
Abstract
The finite powerset functor is a construct frequently employed for the specification of nondeterministic transition systems as coalgebras. The final coalgebra of the finite powerset functor, whose elements characterize the dynamical behavior of transition systems, is a well-understood object which enjoys many equivalent presentations in set-theoretic foundations based on classical logic.
In this paper, we discuss various constructions of the final coalgebra of the finite powerset functor in constructive type theory, and we formalize our results in the Cubical Agda proof assistant. Using setoids, the final coalgebra of the finite powerset functor can be defined from the final coalgebra of the list functor. Using types instead of setoids, as it is common in homotopy type theory, one can specify the finite powerset datatype as a higher inductive type and define its final coalgebra as a coinductive type. Another construction is obtained by quotienting the final coalgebra of the list functor, but the proof of finality requires the assumption of the axiom of choice. We conclude the paper with an analysis of a classical construction by James Worrell, and show that its adaptation to our constructive setting requires the presence of classical axioms such as countable choice and the lesser limited principle of omniscience.
Cite as
Niccolò Veltri. Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{veltri:LIPIcs.FSCD.2021.22,
author = {Veltri, Niccol\`{o}},
title = {{Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {22:1--22: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.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.22},
URN = {urn:nbn:de:0030-drops-142601},
doi = {10.4230/LIPIcs.FSCD.2021.22},
annote = {Keywords: type theory, finite powerset, final coalgebra, Cubical Agda}
}
Document
Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Programs
Abstract
We investigate program equivalence for linear higher-order (sequential) languages endowed with primitives for computational effects. More specifically, we study operationally-based notions of program equivalence for a linear λ-calculus with explicit copying and algebraic effects à la Plotkin and Power. Such a calculus makes explicit the interaction between copying and linearity, which are intensional aspects of computation, with effects, which are, instead, extensional. We review some of the notions of equivalences for linear calculi proposed in the literature and show their limitations when applied to effectful calculi where copying is a first-class citizen. We then introduce resource transition systems, namely transition systems whose states are built over tuples of programs representing the available resources, as an operational semantics accounting for both intensional and extensional interactive behaviours of programs. Our main result is a sound and complete characterization of contextual equivalence as trace equivalence defined on top of resource transition systems.
Cite as
Ugo Dal Lago and Francesco Gavazzo. Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Programs. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 23:1-23:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{dallago_et_al:LIPIcs.FSCD.2021.23,
author = {Dal Lago, Ugo and Gavazzo, Francesco},
title = {{Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Programs}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {23:1--23:19},
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/entities/document/10.4230/LIPIcs.FSCD.2021.23},
URN = {urn:nbn:de:0030-drops-142618},
doi = {10.4230/LIPIcs.FSCD.2021.23},
annote = {Keywords: algebraic effects, linearity, program equivalence, full abstraction}
}
Document
Z; Syntax-Free Developments
Abstract
We present the Z-property and instantiate it to various rewrite systems: associativity, positive braids, self-distributivity, the lambda-calculus, lambda-calculi with explicit substitutions, orthogonal TRSs, .... The Z-property is proven equivalent to Takahashi’s angle property by means of a syntax-free notion of development. We show that several classical consequences of having developments such as confluence, normalisation, and recurrence, can be regained in a syntax-free way, and investigate how the notion corresponds to the classical syntactic notion of development in term rewriting.
Cite as
Vincent van Oostrom. Z; Syntax-Free Developments. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 24:1-24:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{vanoostrom:LIPIcs.FSCD.2021.24,
author = {van Oostrom, Vincent},
title = {{Z; Syntax-Free Developments}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {24:1--24: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/entities/document/10.4230/LIPIcs.FSCD.2021.24},
URN = {urn:nbn:de:0030-drops-142620},
doi = {10.4230/LIPIcs.FSCD.2021.24},
annote = {Keywords: rewrite system, confluence, normalisation, recurrence}
}
Document
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.
Cite as
Cristina Matache, Sean Moss, and Sam Staton. Recursion and Sequentiality in Categories of Sheaves. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 25:1-25:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@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/entities/document/10.4230/LIPIcs.FSCD.2021.25},
URN = {urn:nbn:de:0030-drops-142631},
doi = {10.4230/LIPIcs.FSCD.2021.25},
annote = {Keywords: Denotational semantics, Full abstraction, Recursion, Sheaf toposes, CPOs}
}
Document
Polymorphic Automorphisms and the Picard Group
Abstract
We investigate the concept of definable, or inner, automorphism in the logical setting of partial Horn theories. The central technical result extends a syntactical characterization of the group of such automorphisms (called the covariant isotropy group) associated with an algebraic theory to the wider class of quasi-equational theories. We apply this characterization to prove that the isotropy group of a strict monoidal category is precisely its Picard group of invertible objects. Furthermore, we obtain an explicit description of the covariant isotropy group of a presheaf category.
Cite as
Pieter Hofstra, Jason Parker, and Philip J. Scott. Polymorphic Automorphisms and the Picard Group. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 26:1-26:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{hofstra_et_al:LIPIcs.FSCD.2021.26,
author = {Hofstra, Pieter and Parker, Jason and Scott, Philip J.},
title = {{Polymorphic Automorphisms and the Picard Group}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {26:1--26: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.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.26},
URN = {urn:nbn:de:0030-drops-142646},
doi = {10.4230/LIPIcs.FSCD.2021.26},
annote = {Keywords: Partial Horn Theories, Monoidal Categories, Definable Automorphisms, Polymorphism, Indeterminates, Normal Forms}
}
Document
What’s Decidable About (Atomic) Polymorphism?
Abstract
Due to the undecidability of most type-related properties of System F like type inhabitation or type checking, restricted polymorphic systems have been widely investigated (the most well-known being ML-polymorphism). In this paper we investigate System Fat, or atomic System F, a very weak predicative fragment of System F whose typable terms coincide with the simply typable ones. We show that the type-checking problem for Fat is decidable and we propose an algorithm which sheds some new light on the source of undecidability in full System F. Moreover, we investigate free theorems and contextual equivalence in this fragment, and we show that the latter, unlike in the simply typed lambda-calculus, is undecidable.
Cite as
Paolo Pistone and Luca Tranchini. What’s Decidable About (Atomic) Polymorphism?. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 27:1-27:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{pistone_et_al:LIPIcs.FSCD.2021.27,
author = {Pistone, Paolo and Tranchini, Luca},
title = {{What’s Decidable About (Atomic) Polymorphism?}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {27:1--27:23},
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/entities/document/10.4230/LIPIcs.FSCD.2021.27},
URN = {urn:nbn:de:0030-drops-142652},
doi = {10.4230/LIPIcs.FSCD.2021.27},
annote = {Keywords: Atomic System F, Predicative Polymorphism, ML-Polymorphism, Type-Checking, Contextual Equivalence, Free Theorems}
}
Document
Coalgebra Encoding for Efficient Minimization
Abstract
Recently, we have developed an efficient generic partition refinement algorithm, which computes behavioural equivalence on a state-based system given as an encoded coalgebra, and implemented it in the tool CoPaR. Here we extend this to a fully fledged minimization algorithm and tool by integrating two new aspects: (1) the computation of the transition structure on the minimized state set, and (2) the computation of the reachable part of the given system. In our generic coalgebraic setting these two aspects turn out to be surprisingly non-trivial requiring us to extend the previous theory. In particular, we identify a sufficient condition on encodings of coalgebras, and we show how to augment the existing interface, which encapsulates computations that are specific for the coalgebraic type functor, to make the above extensions possible. Both extensions have linear run time.
Cite as
Hans-Peter Deifel, Stefan Milius, and Thorsten Wißmann. Coalgebra Encoding for Efficient Minimization. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{deifel_et_al:LIPIcs.FSCD.2021.28,
author = {Deifel, Hans-Peter and Milius, Stefan and Wi{\ss}mann, Thorsten},
title = {{Coalgebra Encoding for Efficient Minimization}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {28:1--28:19},
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/entities/document/10.4230/LIPIcs.FSCD.2021.28},
URN = {urn:nbn:de:0030-drops-142664},
doi = {10.4230/LIPIcs.FSCD.2021.28},
annote = {Keywords: Coalgebra, Partition refinement, Transition systems, Minimization}
}
Document
On the Logical Strength of Confluence and Normalisation for Cyclic Proofs
Abstract
In this work we address the logical strength of confluence and normalisation for non-wellfounded typing derivations, in the tradition of "cyclic proof theory". We present a circular version CT of Gödel's system T, with the aim of comparing the relative expressivity of the theories CT and T. We approach this problem by formalising rewriting-theoretic results such as confluence and normalisation for the underlying "coterm" rewriting system of CT within fragments of second-order arithmetic.
We establish confluence of CT within the theory RCA₀, a conservative extension of primitive recursive arithmetic and IΣ1. This allows us to recast type structures of hereditarily recursive operations as "coterm" models of T. We show that these also form models of CT, by formalising a totality argument for circular typing derivations within suitable fragments of second-order arithmetic. Relying on well-known proof mining results, we thus obtain an interpretation of CT into T; in fact, more precisely, we interpret level-n-CT into level-(n+1)-T, an optimum result in terms of abstraction complexity.
A direct consequence of these model-theoretic results is weak normalisation for CT. As further results, we also show strong normalisation for CT and continuity of functionals computed by its type 2 coterms.
Cite as
Anupam Das. On the Logical Strength of Confluence and Normalisation for Cyclic Proofs. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 29:1-29:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{das:LIPIcs.FSCD.2021.29,
author = {Das, Anupam},
title = {{On the Logical Strength of Confluence and Normalisation for Cyclic Proofs}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {29:1--29:23},
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/entities/document/10.4230/LIPIcs.FSCD.2021.29},
URN = {urn:nbn:de:0030-drops-142678},
doi = {10.4230/LIPIcs.FSCD.2021.29},
annote = {Keywords: confluence, normalisation, system T, circular proofs, reverse mathematics, type structures}
}
Document
Abstract Clones for Abstract Syntax
Abstract
We give a formal treatment of simple type theories, such as the simply-typed λ-calculus, using the framework of abstract clones. Abstract clones traditionally describe first-order structures, but by equipping them with additional algebraic structure, one can further axiomatize second-order, variable-binding operators. This provides a syntax-independent representation of simple type theories. We describe multisorted second-order presentations, such as the presentation of the simply-typed λ-calculus, and their clone-theoretic algebras; free algebras on clones abstractly describe the syntax of simple type theories quotiented by equations such as β- and η-equality. We give a construction of free algebras and derive a corresponding induction principle, which facilitates syntax-independent proofs of properties such as adequacy and normalization for simple type theories. Working only with clones avoids some of the complexities inherent in presheaf-based frameworks for abstract syntax.
Cite as
Nathanael Arkor and Dylan McDermott. Abstract Clones for Abstract Syntax. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{arkor_et_al:LIPIcs.FSCD.2021.30,
author = {Arkor, Nathanael and McDermott, Dylan},
title = {{Abstract Clones for Abstract Syntax}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {30:1--30:19},
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/entities/document/10.4230/LIPIcs.FSCD.2021.30},
URN = {urn:nbn:de:0030-drops-142686},
doi = {10.4230/LIPIcs.FSCD.2021.30},
annote = {Keywords: simple type theories, abstract clones, second-order abstract syntax, substitution, variable binding, presentations, free algebras, induction, logical relations}
}
Document
Tuple Interpretations for Higher-Order Complexity
Abstract
We develop a class of algebraic interpretations for many-sorted and higher-order term rewriting systems that takes type information into account. Specifically, base-type terms are mapped to tuples of natural numbers and higher-order terms to functions between those tuples. Tuples may carry information relevant to the type; for instance, a term of type nat may be associated to a pair ⟨ cost, size ⟩ representing its evaluation cost and size. This class of interpretations results in a more fine-grained notion of complexity than runtime or derivational complexity, which makes it particularly useful to obtain complexity bounds for higher-order rewriting systems.
We show that rewriting systems compatible with tuple interpretations admit finite bounds on derivation height. Furthermore, we demonstrate how to mechanically construct tuple interpretations and how to orient β and η reductions within our technique. Finally, we relate our method to runtime complexity and prove that specific interpretation shapes imply certain runtime complexity bounds.
Cite as
Cynthia Kop and Deivid Vale. Tuple Interpretations for Higher-Order Complexity. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 31:1-31:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{kop_et_al:LIPIcs.FSCD.2021.31,
author = {Kop, Cynthia and Vale, Deivid},
title = {{Tuple Interpretations for Higher-Order Complexity}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {31:1--31: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/entities/document/10.4230/LIPIcs.FSCD.2021.31},
URN = {urn:nbn:de:0030-drops-142692},
doi = {10.4230/LIPIcs.FSCD.2021.31},
annote = {Keywords: Complexity, higher-order term rewriting, many-sorted term rewriting, polynomial interpretations, weakly monotonic algebras}
}
Document
Output Without Delay: A π-Calculus Compatible with Categorical Semantics
Abstract
The quest for logical or categorical foundations of the π-calculus (not limited to session-typed variants) remains an important challenge. A categorical type theory correspondence for a variant of the i/o-typed π-calculus was recently revealed by Sakayori and Tsukada, but, at the same time, they exposed that this categorical semantics contradicts with most of the behavioural equivalences. This paper diagnoses the nature of this problem and attempts to fill the gap between categorical and operational semantics. We first identify the source of the problem to be the mismatch between the operational and categorical interpretation of a process called the forwarder. From the operational viewpoint, a forwarder may add an arbitrary delay when forwarding a message, whereas, from the categorical viewpoint, a forwarder must not add any delay when forwarding a message. Led by this observation, we introduce a calculus that can express forwarders that do not introduce delay. More specifically, the calculus we introduce is a variant of the π-calculus with a new operational semantics in which output actions are forced to happen as soon as they get unguarded. We show that this calculus (i) is compatible with the categorical semantics and (ii) can encode the standard π-calculus.
Cite as
Ken Sakayori and Takeshi Tsukada. Output Without Delay: A π-Calculus Compatible with Categorical Semantics. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 32:1-32:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{sakayori_et_al:LIPIcs.FSCD.2021.32,
author = {Sakayori, Ken and Tsukada, Takeshi},
title = {{Output Without Delay: A \pi-Calculus Compatible with Categorical Semantics}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {32:1--32: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/entities/document/10.4230/LIPIcs.FSCD.2021.32},
URN = {urn:nbn:de:0030-drops-142705},
doi = {10.4230/LIPIcs.FSCD.2021.32},
annote = {Keywords: \pi-calculus, categorical semantics, linear approximation}
}