Volume
LIPIcs, Volume 228
7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Formal Structures for Computation and Deduction (FSCD)
Event
FSCD 2022, August 2-5, 2022, Haifa, IsraelEditor
Publication Details
- published at: 2022-06-28
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-233-4
- DBLP: db/conf/rta/fscd2022
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 228, FSCD 2022, Complete Volume
Abstract
LIPIcs, Volume 228, FSCD 2022, Complete Volume
Cite as
7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 1-652, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Proceedings{felty:LIPIcs.FSCD.2022,
title = {{LIPIcs, Volume 228, FSCD 2022, Complete Volume}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {1--652},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022},
URN = {urn:nbn:de:0030-drops-162803},
doi = {10.4230/LIPIcs.FSCD.2022},
annote = {Keywords: LIPIcs, Volume 228, FSCD 2022, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{felty:LIPIcs.FSCD.2022.0,
author = {Felty, Amy P.},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {0:i--0:xviii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.0},
URN = {urn:nbn:de:0030-drops-162814},
doi = {10.4230/LIPIcs.FSCD.2022.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Cutting a Proof into Bite-Sized Chunks: Incrementally proving termination in higher-order term rewriting (Invited Talk)
Abstract
This paper discusses a number of methods to prove termination of higher-order term rewriting systems, with a particular focus on large systems. In first-order term rewriting, the dependency pair framework can be used to split up a large termination problem into multiple (much) smaller components that can be solved individually. This is important because a large problem may take exponentially longer to solve in one go than solving each of its components.
Unfortunately, while there are higher-order versions of several of these methods, they often fail to simplify a problem enough. Here, we will explore some of these techniques and their limitations, and discuss what else can be done to incrementally build a termination proof for higher-order systems.
Cite as
Cynthia Kop. Cutting a Proof into Bite-Sized Chunks: Incrementally proving termination in higher-order term rewriting (Invited Talk). In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 1:1-1:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{kop:LIPIcs.FSCD.2022.1,
author = {Kop, Cynthia},
title = {{Cutting a Proof into Bite-Sized Chunks: Incrementally proving termination in higher-order term rewriting}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {1:1--1:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.1},
URN = {urn:nbn:de:0030-drops-162827},
doi = {10.4230/LIPIcs.FSCD.2022.1},
annote = {Keywords: Termination, Modularity, Higher-order term rewriting, Dependency Pairs, Algebra Interpretations}
}
Document
Invited Talk
A Methodology for Designing Proof Search Calculi for Non-Classical Logics (Invited Talk)
Abstract
In this talk I present a methodology for designing proof search calculi for a wide range of non-classical logics, such as modal and tense logics, bi-intuitionistic (linear) logics and grammar logics. Most of these logics cannot be easily formalised in the traditional Gentzen-style sequent calculus; various structural extensions to sequent calculus seem to be required. One of the more expressive extensions of sequent calculus is Belnap’s display calculus, which allows one to formalise a very wide range of logics and which provides a generic cut-elimination method for logics formalised in the calculus. The generality of display calculus derives partly from the pervasive use of structural rules to capture properties of the underlying semantics of the logic of interest, such as various frame conditions in normal modal logics, that are not easily captured by introduction rules alone. Unlike traditional sequent calculi, the subformula property in display calculi does not typically give an immediate bound on the search space (assuming contraction is absent) in proof search, as new structures may be created and their creation may not be driven by any introduction rules for logical connectives. This line of work started out as an attempt to "tame" display calculus, to make it more proof search friendly, by eliminating or restricting the use of structural rules. Two key ideas that make this possible are the adoption of deep inference, allowing inference rules to be applied inside a nested structure, and the use of propagation rules in place of structural rules. A brief survey of the applications of this methodology to a wide range of logics is presented, along with some directions for future work.
Cite as
Alwen Tiu. A Methodology for Designing Proof Search Calculi for Non-Classical Logics (Invited Talk). In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 2:1-2:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{tiu:LIPIcs.FSCD.2022.2,
author = {Tiu, Alwen},
title = {{A Methodology for Designing Proof Search Calculi for Non-Classical Logics}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {2:1--2:4},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.2},
URN = {urn:nbn:de:0030-drops-162834},
doi = {10.4230/LIPIcs.FSCD.2022.2},
annote = {Keywords: Proof theory, Sequent calculus, Display calculus, Nested sequent calculus, Deep inference}
}
Document
A Fibrational Tale of Operational Logical Relations
Abstract
Logical relations built on top of an operational semantics are one of the most successful proof methods in programming language semantics. In recent years, more and more expressive notions of operationally-based logical relations have been designed and applied to specific families of languages. However, a unifying abstract framework for operationally-based logical relations is still missing. We show how fibrations can provide a uniform treatment of operational logical relations, using as reference example a λ-calculus with generic effects endowed with a novel, abstract operational semantics defined on a large class of categories. Moreover, this abstract perspective allows us to give a solid mathematical ground also to differential logical relations - a recently introduced notion of higher-order distance between programs - both pure and effectful, bringing them back to a common picture with traditional ones.
Cite as
Francesco Dagnino and Francesco Gavazzo. A Fibrational Tale of Operational Logical Relations. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{dagnino_et_al:LIPIcs.FSCD.2022.3,
author = {Dagnino, Francesco and Gavazzo, Francesco},
title = {{A Fibrational Tale of Operational Logical Relations}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {3:1--3:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.3},
URN = {urn:nbn:de:0030-drops-162840},
doi = {10.4230/LIPIcs.FSCD.2022.3},
annote = {Keywords: logical relations, operational semantics, fibrations, generic effects, program distance}
}
Document
On Quantitative Algebraic Higher-Order Theories
Abstract
We explore the possibility of extending Mardare et al.’s quantitative algebras to the structures which naturally emerge from Combinatory Logic and the λ-calculus. First of all, we show that the framework is indeed applicable to those structures, and give soundness and completeness results. Then, we prove some negative results clearly delineating to which extent categories of metric spaces can be models of such theories. We conclude by giving several examples of non-trivial higher-order quantitative algebras.
Cite as
Ugo Dal Lago, Furio Honsell, Marina Lenisa, and Paolo Pistone. On Quantitative Algebraic Higher-Order Theories. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 4:1-4:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{dallago_et_al:LIPIcs.FSCD.2022.4,
author = {Dal Lago, Ugo and Honsell, Furio and Lenisa, Marina and Pistone, Paolo},
title = {{On Quantitative Algebraic Higher-Order Theories}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {4:1--4:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.4},
URN = {urn:nbn:de:0030-drops-162851},
doi = {10.4230/LIPIcs.FSCD.2022.4},
annote = {Keywords: Quantitative Algebras, Lambda Calculus, Combinatory Logic, Metric Spaces}
}
Document
Sheaf Semantics of Termination-Insensitive Noninterference
Abstract
We propose a new sheaf semantics for secure information flow over a space of abstract behaviors, based on synthetic domain theory: security classes are open/closed partitions, types are sheaves, and redaction of sensitive information corresponds to restricting a sheaf to a closed subspace. Our security-aware computational model satisfies termination-insensitive noninterference automatically, and therefore constitutes an intrinsic alternative to state of the art extrinsic/relational models of noninterference. Our semantics is the latest application of Sterling and Harper’s recent re-interpretation of phase distinctions and noninterference in programming languages in terms of Artin gluing and topos-theoretic open/closed modalities. Prior applications include parametricity for ML modules, the proof of normalization for cubical type theory by Sterling and Angiuli, and the cost-aware logical framework of Niu et al. In this paper we employ the phase distinction perspective twice: first to reconstruct the syntax and semantics of secure information flow as a lattice of phase distinctions between "higher" and "lower" security, and second to verify the computational adequacy of our sheaf semantics with respect to a version of Abadi et al.’s dependency core calculus to which we have added a construct for declassifying termination channels.
Cite as
Jonathan Sterling and Robert Harper. Sheaf Semantics of Termination-Insensitive Noninterference. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{sterling_et_al:LIPIcs.FSCD.2022.5,
author = {Sterling, Jonathan and Harper, Robert},
title = {{Sheaf Semantics of Termination-Insensitive Noninterference}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {5:1--5:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.5},
URN = {urn:nbn:de:0030-drops-162869},
doi = {10.4230/LIPIcs.FSCD.2022.5},
annote = {Keywords: information flow, noninterference, denotational semantics, phase distinction, Artin gluing, modal type theory, topos theory, synthetic domain theory, synthetic Tait computability}
}
Document
Combined Hierarchical Matching: the Regular Case
Abstract
Matching algorithms are often central sub-routines in many areas of automated reasoning. They are used in areas such as functional programming, rule-based programming, automated theorem proving, and the symbolic analysis of security protocols. Matching is related to unification but provides a somewhat simplified problem. Thus, in some cases, we can obtain a matching algorithm even if the unification problem is undecidable. In this paper we consider a hierarchical approach to constructing matching algorithms. The hierarchical method has been successful for developing unification algorithms for theories defined over a constructor sub-theory. We show how the approach can be extended to matching problems which allows for the development, in a modular way, of hierarchical matching algorithms. Here we focus on regular theories, where both sides of each equational axiom have the same set of variables. We show that the combination of two hierarchical matching algorithms leads to a hierarchical matching algorithm for the union of regular theories sharing only a common constructor sub-theory.
Cite as
Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen. Combined Hierarchical Matching: the Regular Case. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 6:1-6:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{erbatur_et_al:LIPIcs.FSCD.2022.6,
author = {Erbatur, Serdar and Marshall, Andrew M. and Ringeissen, Christophe},
title = {{Combined Hierarchical Matching: the Regular Case}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {6:1--6:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.6},
URN = {urn:nbn:de:0030-drops-162879},
doi = {10.4230/LIPIcs.FSCD.2022.6},
annote = {Keywords: Matching, combination problem, equational theories}
}
Document
Nominal Anti-Unification with Atom-Variables
Abstract
Anti-unification is the task of generalizing a set of expressions in the most specific way. It was extended to the nominal framework by Baumgarter, Kutsia, Levy and Villaret, who defined an algorithm solving the nominal anti-unification problem, which runs in polynomial time. Unfortunately, when an infinite set of atoms are allowed in generalizations, a minimal complete set of solutions in nominal anti-unification does not exist, in general. In this paper, we present a more general approach to nominal anti-unification that uses atom-variables instead of explicit atoms, and two variants of freshness constraints: NL_A-constraints (with atom-variables), and Eqr-constraints based on Equivalence relations on atom-variables. The idea of atom-variables is that different atom-variables may be instantiated with identical or different atoms. Albeit simple, this freedom in the formulation increases its application potential: we provide an algorithm that is finitary for the NL_A-freshness constraints, and for Eqr-freshness constraints it computes a unique least general generalization. There is a price to pay in the general case: checking freshness constraints and other related logical questions will require exponential time. The setting of Baumgartner et al. is improved by the atom-only case, which runs in polynomial time and computes a unique least general generalization.
Cite as
Manfred Schmidt-Schauß and Daniele Nantes-Sobrinho. Nominal Anti-Unification with Atom-Variables. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 7:1-7:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{schmidtschau_et_al:LIPIcs.FSCD.2022.7,
author = {Schmidt-Schau{\ss}, Manfred and Nantes-Sobrinho, Daniele},
title = {{Nominal Anti-Unification with Atom-Variables}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {7:1--7:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.7},
URN = {urn:nbn:de:0030-drops-162885},
doi = {10.4230/LIPIcs.FSCD.2022.7},
annote = {Keywords: Generalization, anti-unification, nominal algorithms, higher-order deduction}
}
Document
A Certified Algorithm for AC-Unification
Abstract
Implementing unification modulo Associativity and Commutativity (AC) axioms is crucial in rewrite-based programming and theorem provers. We modify Stickel’s seminal AC-unification algorithm to avoid mutual recursion and formalise it in the PVS proof assistant. More precisely, we prove the adjusted algorithm’s termination, soundness, and completeness. To do this, we adapted Fages' termination proof, providing a unique elaborated measure that guarantees termination of the modified AC-unification algorithm. This development (to the best of our knowledge) provides the first fully formalised AC-unification algorithm.
Cite as
Mauricio Ayala-Rincón, Maribel Fernández, Gabriel Ferreira Silva, and Daniele Nantes Sobrinho. A Certified Algorithm for AC-Unification. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 8:1-8:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{ayalarincon_et_al:LIPIcs.FSCD.2022.8,
author = {Ayala-Rinc\'{o}n, Mauricio and Fern\'{a}ndez, Maribel and Silva, Gabriel Ferreira and Sobrinho, Daniele Nantes},
title = {{A Certified Algorithm for AC-Unification}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {8:1--8:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.8},
URN = {urn:nbn:de:0030-drops-162894},
doi = {10.4230/LIPIcs.FSCD.2022.8},
annote = {Keywords: AC-Unification, PVS, Certified Algorithms, Formal Methods, Interactive Theorem Proving}
}
Document
An Analysis of Tennenbaum’s Theorem in Constructive Type Theory
Abstract
Tennenbaum’s theorem states that the only countable model of Peano arithmetic (PA) with computable arithmetical operations is the standard model of natural numbers. In this paper, we use constructive type theory as a framework to revisit and generalize this result.
The chosen framework allows for a synthetic approach to computability theory, by exploiting the fact that, externally, all functions definable in constructive type theory can be shown computable. We internalize this fact by assuming a version of Church’s thesis expressing that any function on natural numbers is representable by a formula in PA. This assumption allows for a conveniently abstract setup to carry out rigorous computability arguments and feasible mechanization.
Concretely, we constructivize several classical proofs and present one inherently constructive rendering of Tennenbaum’s theorem, all following arguments from the literature. Concerning the classical proofs in particular, the constructive setting allows us to highlight differences in their assumptions and conclusions which are not visible classically. All versions are accompanied by a unified mechanization in the Coq proof assistant.
Cite as
Marc Hermes and Dominik Kirst. An Analysis of Tennenbaum’s Theorem in Constructive Type Theory. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{hermes_et_al:LIPIcs.FSCD.2022.9,
author = {Hermes, Marc and Kirst, Dominik},
title = {{An Analysis of Tennenbaum’s Theorem in Constructive Type Theory}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {9:1--9:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.9},
URN = {urn:nbn:de:0030-drops-162909},
doi = {10.4230/LIPIcs.FSCD.2022.9},
annote = {Keywords: first-order logic, Peano arithmetic, Tennenbaum’s theorem, constructive type theory, Church’s thesis, synthetic computability, Coq}
}
Document
Constructing Unprejudiced Extensional Type Theories with Choices via Modalities
Abstract
Time-progressing expressions, i.e., expressions that compute to different values over time such as Brouwerian choice sequences or reference cells, are a common feature in many frameworks. For type theories to support such elements, they usually employ sheaf models. In this paper, we provide a general framework in the form of an extensional type theory incorporating various time-progressing elements along with a general possible-worlds forcing interpretation parameterized by modalities. The modalities can, in turn, be instantiated with topological spaces of bars, leading to a general sheaf model. This parameterized construction allows us to capture a distinction between theories that are "agnostic", i.e., compatible with classical reasoning in the sense that classical axioms can be validated, and those that are "intuitionistic", i.e., incompatible with classical reasoning in the sense that classical axioms can be proven false. This distinction is made via properties of the modalities selected to model the theory and consequently via the space of bars instantiating the modalities. We further identify a class of time-progressing elements that allows deriving "intuitionistic" theories that include not only choice sequences but also simpler operators, namely reference cells.
Cite as
Liron Cohen and Vincent Rahli. Constructing Unprejudiced Extensional Type Theories with Choices via Modalities. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 10:1-10:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{cohen_et_al:LIPIcs.FSCD.2022.10,
author = {Cohen, Liron and Rahli, Vincent},
title = {{Constructing Unprejudiced Extensional Type Theories with Choices via Modalities}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {10:1--10:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.10},
URN = {urn:nbn:de:0030-drops-162917},
doi = {10.4230/LIPIcs.FSCD.2022.10},
annote = {Keywords: Intuitionism, Extensional Type Theory, Constructive Type Theory, Realizability, Choice sequences, References, Classical Logic, Theorem proving, Agda}
}
Document
Division by Two, in Homotopy Type Theory
Abstract
Natural numbers are isomorphism classes of finite sets and one can look for operations on sets which, after quotienting, allow recovering traditional arithmetic operations. Moreover, from a constructivist perspective, it is interesting to study whether those operations can be performed without resorting to the axiom of choice (the use of classical logic is usually necessary). Following the work of Bernstein, Sierpiński, Doyle and Conway, we study here "division by two" (or, rather, regularity of multiplication by two). We provide here a full formalization of this operation on sets, using the cubical variant of Agda, which is an implementation of the homotopy type theory setting, thus revealing some interesting points in the proof. As a novel contribution, we also show that this construction extends to general types, as opposed to sets.
Cite as
Samuel Mimram and Émile Oleon. Division by Two, in Homotopy Type Theory. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 11:1-11:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{mimram_et_al:LIPIcs.FSCD.2022.11,
author = {Mimram, Samuel and Oleon, \'{E}mile},
title = {{Division by Two, in Homotopy Type Theory}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {11:1--11:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.11},
URN = {urn:nbn:de:0030-drops-162920},
doi = {10.4230/LIPIcs.FSCD.2022.11},
annote = {Keywords: division, axiom of choice, set theory, homotopy type theory, Agda}
}
Document
Type-Based Termination for Futures
Abstract
In sequential functional languages, sized types enable termination checking of programs with complex patterns of recursion in the presence of mixed inductive-coinductive types. In this paper, we adapt sized types and their metatheory to the concurrent setting. We extend the semi-axiomatic sequent calculus, a subsuming paradigm for futures-based functional concurrency, and its underlying operational semantics with recursion and arithmetic refinements. The latter enables a new and highly general sized type scheme we call sized type refinements. As a widely applicable technical device, we type recursive programs with infinitely deep typing derivations that unfold all recursive calls. Then, we observe that certain such derivations can be made infinitely wide but finitely deep. The resulting trees serve as the induction target of our strong normalization result, which we develop via a novel logical relations argument.
Cite as
Siva Somayyajula and Frank Pfenning. Type-Based Termination for Futures. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 12:1-12:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{somayyajula_et_al:LIPIcs.FSCD.2022.12,
author = {Somayyajula, Siva and Pfenning, Frank},
title = {{Type-Based Termination for Futures}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {12:1--12:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.12},
URN = {urn:nbn:de:0030-drops-162931},
doi = {10.4230/LIPIcs.FSCD.2022.12},
annote = {Keywords: type-based termination, sized types, futures, concurrency, infinite proofs}
}
Document
Addition and Differentiation of ZX-Diagrams
Abstract
The ZX-calculus is a powerful framework for reasoning in quantum computing. It provides in particular a compact representation of matrices of interests. A peculiar property of the ZX-calculus is the absence of a formal sum allowing the linear combinations of arbitrary ZX-diagrams. The universality of the formalism guarantees however that for any two ZX-diagrams, the sum of their interpretations can be represented by a ZX-diagram. We introduce a general, inductive definition of the addition of ZX-diagrams, relying on the construction of controlled diagrams. Based on this addition technique, we provide an inductive differentiation of ZX-diagrams.
Indeed, given a ZX-diagram with variables in the description of its angles, one can differentiate the diagram according to one of these variables. Differentiation is ubiquitous in quantum mechanics and quantum computing (e.g. for solving optimization problems). Technically, differentiation of ZX-diagrams is strongly related to summation as witnessed by the product rules.
We also introduce an alternative, non inductive, differentiation technique rather based on the isolation of the variables. Finally, we apply our results to deduce a diagram for an Ising Hamiltonian.
Cite as
Emmanuel Jeandel, Simon Perdrix, and Margarita Veshchezerova. Addition and Differentiation of ZX-Diagrams. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 13:1-13:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{jeandel_et_al:LIPIcs.FSCD.2022.13,
author = {Jeandel, Emmanuel and Perdrix, Simon and Veshchezerova, Margarita},
title = {{Addition and Differentiation of ZX-Diagrams}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {13:1--13:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.13},
URN = {urn:nbn:de:0030-drops-162946},
doi = {10.4230/LIPIcs.FSCD.2022.13},
annote = {Keywords: ZX calculus, Addition of ZX diagrams, Diagrammatic differentiation}
}
Document
Restricting Tree Grammars with Term Rewriting
Abstract
We investigate the problem of enumerating all terms generated by a tree-grammar which are also in normal form with respect to a set of directed equations (rewriting relation). To this end we show that deciding emptiness and finiteness of the resulting set is EXPTIME-complete. The emptiness result is inspired by a prior result by Comon and Jacquemard on ground reducibility. The finiteness result is based on modification of pumping arguments used by Comon and Jacquemard. We highlight practical applications and limitations. We provide and evaluate a prototype implementation. Limitations are somewhat surprising in that, while deciding emptiness and finiteness is EXPTIME-complete for linear and nonlinear rewrite relations, the linear case is practically feasible while the nonlinear case is infeasible, even for a trivially small example. The algorithms provided for the linear case also improve on prior practical results by Kallat et al.
Cite as
Jan Bessai, Lukasz Czajka, Felix Laarmann, and Jakob Rehof. Restricting Tree Grammars with Term Rewriting. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{bessai_et_al:LIPIcs.FSCD.2022.14,
author = {Bessai, Jan and Czajka, Lukasz and Laarmann, Felix and Rehof, Jakob},
title = {{Restricting Tree Grammars with Term Rewriting}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {14:1--14:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.14},
URN = {urn:nbn:de:0030-drops-162953},
doi = {10.4230/LIPIcs.FSCD.2022.14},
annote = {Keywords: tree automata, tree grammar, term rewriting, normalization, emptiness, finiteness}
}
Document
On Lookaheads in Regular Expressions with Backreferences
Abstract
Many modern regular expression engines employ various extensions to give more expressive support for real-world usages. Among the major extensions employed by many of the modern regular expression engines are backreferences and lookaheads. A question of interest about these extended regular expressions is their expressive power. Previous works have shown that (i) the extension by lookaheads does not enhance the expressive power, i.e., the expressive power of regular expressions with lookaheads is still regular, and that (ii) the extension by backreferences enhances the expressive power, i.e., the expressive power of regular expressions with backreferences (abbreviated as rewb) is no longer regular. This raises the following natural question: Does the extension of regular expressions with backreferences by lookaheads enhance the expressive power of regular expressions with backreferences? This paper answers the question positively by proving that adding either positive lookaheads or negative lookaheads increases the expressive power of rewb (the former abbreviated as rewbl_p and the latter as rewbl_n). A consequence of our result is that neither the class of finite state automata nor that of memory automata (MFA) of Schmid [Markus L. Schmid, 2016] (which corresponds to regular expressions with backreferenes but without lookaheads) corresponds to rewbl_p or rewbl_n. To fill the void, as a first step toward building such automata, we propose a new class of automata called memory automata with positive lookaheads (PLMFA) that corresponds to rewbl_p. The key idea of PLMFA is to extend MFA with a new kind of memories, called positive-lookahead memory, that is used to simulate the backtracking behavior of positive lookaheads. Interestingly, our positive-lookahead memories are almost perfectly symmetric to the capturing-group memories of MFA. Therefore, our PLMFA can be seen as a natural extension of MFA that can be obtained independently of its original intended purpose of simulating rewbl_p.
Cite as
Nariyoshi Chida and Tachio Terauchi. On Lookaheads in Regular Expressions with Backreferences. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{chida_et_al:LIPIcs.FSCD.2022.15,
author = {Chida, Nariyoshi and Terauchi, Tachio},
title = {{On Lookaheads in Regular Expressions with Backreferences}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {15:1--15:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.15},
URN = {urn:nbn:de:0030-drops-162965},
doi = {10.4230/LIPIcs.FSCD.2022.15},
annote = {Keywords: Regular expressions, Lookaheads, Backreferences, Memory automata}
}
Document
Certified Decision Procedures for Two-Counter Machines
Abstract
Two-counter machines, pioneered by Minsky in the 1960s, constitute a particularly simple, universal model of computation. Universality of reversible two-counter machines (having a right-unique step relation) has been shown by Morita in the 1990s. Therefore, the halting problem for reversible two-counter machines is undecidable. Surprisingly, this statement is specific to certain instruction sets of the underlying machine model.
In the present work we consider two-counter machines (CM2) with instructions inc_c (increment counter c, go to next instruction), dec_c q (if counter c is zero, then go to next instruction, otherwise decrement counter c and go to instruction q). While the halting problem for CM2 is undecidable, we give a decision procedure for the halting problem for reversible CM2, contrasting Morita’s result.
We supplement our result with decision procedures for uniform boundedness (is there a uniform bound on the number of reachable configurations?) and uniform mortality (is there a uniform bound on the number of steps in any run?) for CM2.
Termination and correctness of each presented decision procedure is certified using the Coq proof assistant. In fact, both the implementation and certification is carried out simultaneously using the tactic language of the Coq proof assistant. Building upon existing infrastructure, the mechanized decision procedures are contributed to the Coq library of undecidability proofs.
Cite as
Andrej Dudenhefner. Certified Decision Procedures for Two-Counter Machines. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{dudenhefner:LIPIcs.FSCD.2022.16,
author = {Dudenhefner, Andrej},
title = {{Certified Decision Procedures for Two-Counter Machines}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {16:1--16:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.16},
URN = {urn:nbn:de:0030-drops-162978},
doi = {10.4230/LIPIcs.FSCD.2022.16},
annote = {Keywords: constructive mathematics, computability theory, decidability, counter automata, mechanization, Coq}
}
Document
Strategies for Asymptotic Normalization
Abstract
We present an abstract technique to study normalizing strategies when termination is asymptotic, that is, it appears as a limit. Asymptotic termination occurs in several settings, such as effectful, and in particular probabilistic computation - where the limits are distributions over the possible outputs - or infinitary lambda-calculi - where the limits are infinitary terms such as Böhm trees.
As a concrete application, we obtain a result which is of independent interest: a normalization theorem for Call-by-Value (and - in a uniform way - for Call-by-Name) probabilistic lambda-calculus.
Cite as
Claudia Faggian and Giulio Guerrieri. Strategies for Asymptotic Normalization. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 17:1-17:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{faggian_et_al:LIPIcs.FSCD.2022.17,
author = {Faggian, Claudia and Guerrieri, Giulio},
title = {{Strategies for Asymptotic Normalization}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {17:1--17:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.17},
URN = {urn:nbn:de:0030-drops-162987},
doi = {10.4230/LIPIcs.FSCD.2022.17},
annote = {Keywords: rewriting, strategies, normalization, lambda calculus, probabilistic rewriting}
}
Document
Solvability for Generalized Applications
Abstract
Solvability is a key notion in the theory of call-by-name lambda-calculus, used in particular to identify meaningful terms. However, adapting this notion to other call-by-name calculi, or extending it to different models of computation - such as call-by-value - , is not straightforward. In this paper, we study solvability for call-by-name and call-by-value lambda-calculi with generalized applications, both variants inspired from von Plato’s natural deduction with generalized elimination rules. We develop an operational as well as a logical theory of solvability for each of them. The operational characterization relies on a notion of solvable reduction for generalized applications, and the logical characterization is given in terms of typability in an appropriate non-idempotent intersection type system. Finally, we show that solvability in generalized applications and solvability in the lambda-calculus are equivalent notions.
Cite as
Delia Kesner and Loïc Peyrot. Solvability for Generalized Applications. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 18:1-18:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{kesner_et_al:LIPIcs.FSCD.2022.18,
author = {Kesner, Delia and Peyrot, Lo\"{i}c},
title = {{Solvability for Generalized Applications}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {18:1--18:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.18},
URN = {urn:nbn:de:0030-drops-162994},
doi = {10.4230/LIPIcs.FSCD.2022.18},
annote = {Keywords: Lambda-calculus, Generalized applications, Solvability, CBN/CBV, Quantitative types}
}
Document
Normalization Without Syntax
Abstract
We present normalization for intuitionistic combinatorial proofs (ICPs) and relate it to the simply-typed lambda-calculus. We prove confluence and strong normalization. Combinatorial proofs, or "proofs without syntax", form a graphical semantics of proof in various logics that is canonical yet complexity-aware: they are a polynomial-sized representation of sequent proofs that factors out exactly the non-duplicating permutations. Our approach to normalization aligns with these characteristics: it is canonical (free of permutations) and generic (readily applied to other logics). Our reduction mechanism is a canonical representation of reduction in sequent calculus with closed cuts (no abstraction is allowed below a cut), and relates to closed reduction in lambda-calculus and supercombinators. While we will use ICPs concretely, the notion of reduction is completely abstract, and can be specialized to give a reduction mechanism for any representation of typed normal forms.
Cite as
Willem B. Heijltjes, Dominic J. D. Hughes, and Lutz Straßburger. Normalization Without Syntax. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{heijltjes_et_al:LIPIcs.FSCD.2022.19,
author = {Heijltjes, Willem B. and Hughes, Dominic J. D. and Stra{\ss}burger, Lutz},
title = {{Normalization Without Syntax}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {19:1--19:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.19},
URN = {urn:nbn:de:0030-drops-163004},
doi = {10.4230/LIPIcs.FSCD.2022.19},
annote = {Keywords: combinatorial proofs, intuitionistic logic, lambda-calculus, Curry-Howard, proof nets}
}
Document
Decision Problems for Linear Logic with Least and Greatest Fixed Points
Abstract
Linear logic is an important logic for modelling resources and decomposing computational interpretations of proofs. Decision problems for fragments of linear logic exhibiting "infinitary" behaviour (such as exponentials) are notoriously complicated. In this work, we address the decision problems for variations of linear logic with fixed points (μMALL), in particular, recent systems based on "circular" and "non-wellfounded" reasoning. In this paper, we show that μMALL is undecidable.
More explicitly, we show that the general non-wellfounded system is Π⁰₁-hard via a reduction to the non-halting of Minsky machines, and thus is strictly stronger than its circular counterpart (which is in Σ⁰₁). Moreover, we show that the restriction of these systems to theorems with only the least fixed points is already Σ⁰₁-complete via a reduction to the reachability problem of alternating vector addition systems with states. This implies that both the circular system and the finitary system (with explicit (co)induction) are Σ⁰₁-complete.
Cite as
Anupam Das, Abhishek De, and Alexis Saurin. Decision Problems for Linear Logic with Least and Greatest Fixed Points. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 20:1-20:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{das_et_al:LIPIcs.FSCD.2022.20,
author = {Das, Anupam and De, Abhishek and Saurin, Alexis},
title = {{Decision Problems for Linear Logic with Least and Greatest Fixed Points}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {20:1--20:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.20},
URN = {urn:nbn:de:0030-drops-163019},
doi = {10.4230/LIPIcs.FSCD.2022.20},
annote = {Keywords: Linear logic, fixed points, decidability, vector addition systems}
}
Document
Linear Lambda-Calculus is Linear
Abstract
We prove a linearity theorem for an extension of linear logic with addition and multiplication by a scalar: the proofs of some propositions in this logic are linear in the algebraic sense. This work is part of a wider research program that aims at defining a logic whose proof language is a quantum programming language.
Cite as
Alejandro Díaz-Caro and Gilles Dowek. Linear Lambda-Calculus is Linear. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{diazcaro_et_al:LIPIcs.FSCD.2022.21,
author = {D{\'\i}az-Caro, Alejandro and Dowek, Gilles},
title = {{Linear Lambda-Calculus is Linear}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {21:1--21:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.21},
URN = {urn:nbn:de:0030-drops-163024},
doi = {10.4230/LIPIcs.FSCD.2022.21},
annote = {Keywords: Proof theory, Lambda calculus, Linear logic, Quantum computing}
}
Document
A Graphical Proof Theory of Logical Time
Abstract
Logical time is a partial order over events in distributed systems, constraining which events precede others. Special interest has been given to series-parallel orders since they correspond to formulas constructed via the two operations for "series" and "parallel" composition. For this reason, series-parallel orders have received attention from proof theory, leading to pomset logic, the logic BV, and their extensions. However, logical time does not always form a series-parallel order; indeed, ubiquitous structures in distributed systems are beyond current proof theoretic methods. In this paper, we explore how this restriction can be lifted. We design new logics that work directly on graphs instead of formulas, we develop their proof theory, and we show that our logics are conservative extensions of the logic BV.
Cite as
Matteo Acclavio, Ross Horne, Sjouke Mauw, and Lutz Straßburger. A Graphical Proof Theory of Logical Time. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 22:1-22:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{acclavio_et_al:LIPIcs.FSCD.2022.22,
author = {Acclavio, Matteo and Horne, Ross and Mauw, Sjouke and Stra{\ss}burger, Lutz},
title = {{A Graphical Proof Theory of Logical Time}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {22:1--22:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.22},
URN = {urn:nbn:de:0030-drops-163037},
doi = {10.4230/LIPIcs.FSCD.2022.22},
annote = {Keywords: proof theory, causality, deep inference}
}
Document
A Stratified Approach to Löb Induction
Abstract
Guarded type theory extends type theory with a handful of modalities and constants to encode productive recursion. While these theories have seen widespread use, the metatheory of guarded type theories, particularly guarded dependent type theories remains underdeveloped. We show that integrating Löb induction is the key obstruction to unifying guarded recursion and dependence in a well-behaved type theory and prove a no-go theorem sharply bounding such type theories.
Based on these results, we introduce GuTT: a stratified guarded type theory. GuTT is properly two type theories, sGuTT and dGuTT. The former contains only propositional rules governing Löb induction but enjoys decidable type-checking while the latter extends the former with definitional equalities. Accordingly, dGuTT does not have decidable type-checking. We prove, however, a novel guarded canonicity theorem for dGuTT, showing that programs in dGuTT can be run. These two type theories work in concert, with users writing programs in sGuTT and running them in dGuTT.
Cite as
Daniel Gratzer and Lars Birkedal. A Stratified Approach to Löb Induction. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 23:1-23:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{gratzer_et_al:LIPIcs.FSCD.2022.23,
author = {Gratzer, Daniel and Birkedal, Lars},
title = {{A Stratified Approach to L\"{o}b Induction}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {23:1--23:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.23},
URN = {urn:nbn:de:0030-drops-163048},
doi = {10.4230/LIPIcs.FSCD.2022.23},
annote = {Keywords: Dependent type theory, guarded recursion, modal type theory, canonicity, categorical gluing}
}
Document
Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity
Abstract
The encoding of proof systems and type theories in logical frameworks is key to allow the translation of proofs from one system to the other. The λΠ-calculus modulo rewriting is a powerful logical framework in which various systems have already been encoded, including type systems with an infinite hierarchy of type universes equipped with a unary successor operator and a binary max operator: Matita, Coq, Agda and Lean. However, to decide the word problem in this max-successor algebra, all the encodings proposed so far use rewriting with matching modulo associativity and commutativity (AC), which is of high complexity and difficult to integrate in usual algorithms for b-reduction and type-checking. In this paper, we show that we do not need matching modulo AC by enforcing terms to be in some special canonical form wrt associativity and commutativity, and by using rewriting rules taking advantage of this canonical form. This work has been implemented in the proof assistant Lambdapi.
Cite as
Frédéric Blanqui. Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 24:1-24:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{blanqui:LIPIcs.FSCD.2022.24,
author = {Blanqui, Fr\'{e}d\'{e}ric},
title = {{Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {24:1--24:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.24},
URN = {urn:nbn:de:0030-drops-163059},
doi = {10.4230/LIPIcs.FSCD.2022.24},
annote = {Keywords: logical framework, type theory, type universes, rewriting}
}
Document
Adequate and Computational Encodings in the Logical Framework Dedukti
Abstract
Dedukti is a very expressive logical framework which unlike most frameworks, such as the Edinburgh Logical Framework (LF), allows for the representation of computation alongside deduction. However, unlike LF encodings, Dedukti encodings proposed until now do not feature an adequacy theorem - i.e., a bijection between terms in the encoded system and in its encoding. Moreover, many of them also do not have a conservativity result, which compromises the ability of Dedukti to check proofs written in such encodings. We propose a different approach for Dedukti encodings which do not only allow for simpler conservativity proofs, but which also restore the adequacy of encodings. More precisely, we propose in this work adequate (and thus conservative) encodings for Functional Pure Type Systems. However, in contrast with LF encodings, ours is computational - that is, represents computation directly as computation. Therefore, our work is the first to present and prove correct an approach allowing for encodings that are both adequate and computational in Dedukti.
Cite as
Thiago Felicissimo. Adequate and Computational Encodings in the Logical Framework Dedukti. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 25:1-25:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{felicissimo:LIPIcs.FSCD.2022.25,
author = {Felicissimo, Thiago},
title = {{Adequate and Computational Encodings in the Logical Framework Dedukti}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {25:1--25:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.25},
URN = {urn:nbn:de:0030-drops-163064},
doi = {10.4230/LIPIcs.FSCD.2022.25},
annote = {Keywords: Type Theory, Logical Frameworks, Rewriting, Dedukti, Pure Type Systems}
}
Document
mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity
Abstract
Implicit Computational Complexity (ICC) drives better understanding of complexity classes, but it also guides the development of resources-aware languages and static source code analyzers. Among the methods developed, the mwp-flow analysis [Jones and Lars Kristiansen, 2009] certifies polynomial bounds on the size of the values manipulated by an imperative program. This result is obtained by bounding the transitions between states instead of focusing on states in isolation, as most static analyzers do, and is not concerned with termination or tight bounds on values. Those differences, along with its built-in compositionality, make the mwp-flow analysis a good target for determining how ICC-inspired techniques diverge compared with more traditional static analysis methods. This paper’s contributions are three-fold: we fine-tune the internal machinery of the original analysis to make it tractable in practice; we extend the analysis to function calls and leverage its machinery to compute the result of the analysis efficiently; and we implement the resulting analysis as a lightweight tool to automatically perform data-size analysis of C programs. This documented effort prepares and enables the development of certified complexity analysis, by transforming a costly analysis into a tractable program, that furthermore decorrelates the problem of deciding if a bound exist with the problem of computing it.
Cite as
Clément Aubert, Thomas Rubiano, Neea Rusch, and Thomas Seiller. mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 26:1-26:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{aubert_et_al:LIPIcs.FSCD.2022.26,
author = {Aubert, Cl\'{e}ment and Rubiano, Thomas and Rusch, Neea and Seiller, Thomas},
title = {{mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {26:1--26:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.26},
URN = {urn:nbn:de:0030-drops-163071},
doi = {10.4230/LIPIcs.FSCD.2022.26},
annote = {Keywords: Static Program Analysis, Implicit Computational Complexity, Automatic Complexity Analysis, Program Verification}
}
Document
Polynomial Termination Over ℕ Is Undecidable
Abstract
In this paper we prove via a reduction from Hilbert’s 10th problem that the problem whether the termination of a given rewrite system can be shown by a polynomial interpretation in the natural numbers is undecidable, even for rewrite systems that are incrementally polynomially terminating. We also prove that incremental polynomial termination is an undecidable property of terminating rewrite systems.
Cite as
Fabian Mitterwallner and Aart Middeldorp. Polynomial Termination Over ℕ Is Undecidable. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{mitterwallner_et_al:LIPIcs.FSCD.2022.27,
author = {Mitterwallner, Fabian and Middeldorp, Aart},
title = {{Polynomial Termination Over \mathbb{N} Is Undecidable}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {27:1--27:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.27},
URN = {urn:nbn:de:0030-drops-163081},
doi = {10.4230/LIPIcs.FSCD.2022.27},
annote = {Keywords: Term Rewriting, Polynomial Termination, Undecidability}
}
Document
Compositional Confluence Criteria
Abstract
We show how confluence criteria based on decreasing diagrams are generalized to ones composable with other criteria. For demonstration of the method, the confluence criteria of orthogonality, rule labeling, and critical pair systems for term rewriting are recast into composable forms. In addition to them, we prove that Toyama’s parallel closedness result based on parallel critical pairs subsumes his almost parallel closedness theorem.
Cite as
Kiraku Shintani and Nao Hirokawa. Compositional Confluence Criteria. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{shintani_et_al:LIPIcs.FSCD.2022.28,
author = {Shintani, Kiraku and Hirokawa, Nao},
title = {{Compositional Confluence Criteria}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {28:1--28:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.28},
URN = {urn:nbn:de:0030-drops-163095},
doi = {10.4230/LIPIcs.FSCD.2022.28},
annote = {Keywords: term rewriting, confluence, decreasing diagrams}
}
Document
Rewriting for Monoidal Closed Categories
Abstract
This paper develops a formal string diagram language for monoidal closed categories. Previous work has shown that string diagrams for freely generated symmetric monoidal categories can be viewed as hypergraphs with interfaces, and the axioms of these categories can be realized by rewriting systems. This work proposes hierarchical hypergraphs as a suitable formalization of string diagrams for monoidal closed categories. We then show double pushout rewriting captures the axioms of these closed categories.
Cite as
Mario Alvarez-Picallo, Dan Ghica, David Sprunger, and Fabio Zanasi. Rewriting for Monoidal Closed Categories. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{alvarezpicallo_et_al:LIPIcs.FSCD.2022.29,
author = {Alvarez-Picallo, Mario and Ghica, Dan and Sprunger, David and Zanasi, Fabio},
title = {{Rewriting for Monoidal Closed Categories}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {29:1--29:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.29},
URN = {urn:nbn:de:0030-drops-163108},
doi = {10.4230/LIPIcs.FSCD.2022.29},
annote = {Keywords: string diagrams, rewriting, hierarchical hypergraph, monoidal closed category}
}
Document
Stateful Structural Operational Semantics
Abstract
Compositionality of denotational semantics is an important concern in programming semantics. Mathematical operational semantics in the sense of Turi and Plotkin guarantees compositionality, but seen from the point of view of stateful computation it applies only to very fine-grained equivalences that essentially assume unrestricted interference by the environment between any two statements. We introduce the more restrictive stateful SOS rule format for stateful languages. We show that compositionality of two more coarse-grained semantics, respectively given by assuming read-only interference or no interference between steps, remains an undecidable property even for stateful SOS. However, further restricting the rule format in a manner inspired by the cool GSOS formats of Bloom and van Glabbeek, we obtain the streamlined and cool stateful SOS formats, which respectively guarantee compositionality of the two more abstract equivalences.
Cite as
Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat. Stateful Structural Operational Semantics. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{goncharov_et_al:LIPIcs.FSCD.2022.30,
author = {Goncharov, Sergey and Milius, Stefan and Schr\"{o}der, Lutz and Tsampas, Stelios and Urbat, Henning},
title = {{Stateful Structural Operational Semantics}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {30:1--30:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.30},
URN = {urn:nbn:de:0030-drops-163111},
doi = {10.4230/LIPIcs.FSCD.2022.30},
annote = {Keywords: Structural Operational Semantics, Rule Formats, Distributive Laws}
}
Document
A Combinatorial Approach to Higher-Order Structure for Polynomial Functors
Abstract
Polynomial functors are categorical structures used in a variety of applications across theoretical computer science; for instance, in database theory, denotational semantics, functional programming, and type theory. A well-known problem is that the bicategory of finitary polynomial functors between categories of indexed sets is not cartesian closed, despite its success and influence on denotational models and linear logic.
This paper introduces a formal bridge between the model of finitary polynomial functors and the combinatorial theory of generalised species of structures. Our approach consists in viewing finitary polynomial functors as free analytic functors, which correspond to free generalised species. In order to systematically consider finitary polynomial functors from this combinatorial perspective, we study a model of groupoids with additional logical structure; this is used to constrain the generalised species between them. The result is a new cartesian closed bicategory that embeds finitary polynomial functors.
Cite as
Marcelo Fiore, Zeinab Galal, and Hugo Paquet. A Combinatorial Approach to Higher-Order Structure for Polynomial Functors. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{fiore_et_al:LIPIcs.FSCD.2022.31,
author = {Fiore, Marcelo and Galal, Zeinab and Paquet, Hugo},
title = {{A Combinatorial Approach to Higher-Order Structure for Polynomial Functors}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {31:1--31:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.31},
URN = {urn:nbn:de:0030-drops-163129},
doi = {10.4230/LIPIcs.FSCD.2022.31},
annote = {Keywords: Bicategorical models, denotational semantics, stable domain theory, linear logic, polynomial functors, species of structures, groupoids}
}
Document
Galois Connecting Call-by-Value and Call-by-Name
Abstract
We establish a general framework for reasoning about the relationship between call-by-value and call-by-name.
In languages with side-effects, call-by-value and call-by-name executions of programs often have different, but related, observable behaviours. For example, if a program might diverge but otherwise has no side-effects, then whenever it terminates under call-by-value, it terminates with the same result under call-by-name. We propose a technique for stating and proving these properties. The key ingredient is Levy’s call-by-push-value calculus, which we use as a framework for reasoning about evaluation orders. We construct maps between the call-by-value and call-by-name interpretations of types. We then identify properties of side-effects that imply these maps form a Galois connection. These properties hold for some side-effects (such as divergence), but not others (such as mutable state). This gives rise to a general reasoning principle that relates call-by-value and call-by-name. We apply the reasoning principle to example side-effects including divergence and nondeterminism.
Cite as
Dylan McDermott and Alan Mycroft. Galois Connecting Call-by-Value and Call-by-Name. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 32:1-32:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{mcdermott_et_al:LIPIcs.FSCD.2022.32,
author = {McDermott, Dylan and Mycroft, Alan},
title = {{Galois Connecting Call-by-Value and Call-by-Name}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {32:1--32:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.32},
URN = {urn:nbn:de:0030-drops-163138},
doi = {10.4230/LIPIcs.FSCD.2022.32},
annote = {Keywords: computational effect, evaluation order, call-by-push-value, categorical semantics}
}