Volume
LIPIcs, Volume 260
8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Formal Structures for Computation and Deduction (FSCD)
Event
FSCD 2023, July 3-6, 2023, Rome, ItalyEditors
Publication Details
- published at: 2023-06-28
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-277-8
- DBLP: db/conf/rta/fscd2023
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 260, FSCD 2023, Complete Volume
Abstract
LIPIcs, Volume 260, FSCD 2023, Complete Volume
Cite as
8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 1-658, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Proceedings{gaboardi_et_al:LIPIcs.FSCD.2023,
title = {{LIPIcs, Volume 260, FSCD 2023, Complete Volume}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {1--658},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023},
URN = {urn:nbn:de:0030-drops-179830},
doi = {10.4230/LIPIcs.FSCD.2023},
annote = {Keywords: LIPIcs, Volume 260, FSCD 2023, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{gaboardi_et_al:LIPIcs.FSCD.2023.0,
author = {Gaboardi, Marco and van Raamsdonk, Femke},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {0:i--0:xviii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.0},
URN = {urn:nbn:de:0030-drops-179849},
doi = {10.4230/LIPIcs.FSCD.2023.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Nominal Techniques for Software Specification and Verification (Invited Talk)
Abstract
In this talk we discuss the nominal approach to the specification of languages with binders and some applications to programming languages and verification.
Cite as
Maribel Fernández. Nominal Techniques for Software Specification and Verification (Invited Talk). In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 1:1-1:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{fernandez:LIPIcs.FSCD.2023.1,
author = {Fern\'{a}ndez, Maribel},
title = {{Nominal Techniques for Software Specification and Verification}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {1:1--1:4},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.1},
URN = {urn:nbn:de:0030-drops-179855},
doi = {10.4230/LIPIcs.FSCD.2023.1},
annote = {Keywords: Binding operator, Nominal Logic, Nominal Rewriting, Unification, Equational Theories, Type Systems}
}
Document
Invited Talk
How Can We Make Trustworthy AI? (Invited Talk)
Abstract
Not too long ago most headlines talked about our fear of AI. Today, AI is ubiquitous, and the conversation has moved on from whether we should use AI to how we can trust the AI systems that we use in our daily lives. In this talk I look at some key technical ingredients that help us build confidence and trust in using intelligent technology. I argue that intuitiveness, interaction, explainability and inclusion of human domain knowledge are essential in building this trust. I present some of the techniques and methods we are building for making AI systems that think and interact with humans in more intuitive and personalised ways, enabling humans to better understand the solutions produced by machines, and enabling machines to incorporate human domain knowledge in their reasoning and learning processes.
Cite as
Mateja Jamnik. How Can We Make Trustworthy AI? (Invited Talk). In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{jamnik:LIPIcs.FSCD.2023.2,
author = {Jamnik, Mateja},
title = {{How Can We Make Trustworthy AI?}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {2:1--2:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.2},
URN = {urn:nbn:de:0030-drops-179869},
doi = {10.4230/LIPIcs.FSCD.2023.2},
annote = {Keywords: AI, human-centric computing, knowledge representation, reasoning, machine learning}
}
Document
Invited Talk
A Lambda Calculus Satellite (Invited Talk)
Abstract
We shortly summarize the contents of the book "A Lambda Calculus Satellite", presented at the 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023).
Cite as
Giulio Manzonetto. A Lambda Calculus Satellite (Invited Talk). In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 3:1-3:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{manzonetto:LIPIcs.FSCD.2023.3,
author = {Manzonetto, Giulio},
title = {{A Lambda Calculus Satellite}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {3:1--3:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.3},
URN = {urn:nbn:de:0030-drops-179878},
doi = {10.4230/LIPIcs.FSCD.2023.3},
annote = {Keywords: \lambda-calculus, rewriting, denotational models, equational theories}
}
Document
Invited Talk
Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition (Invited Talk)
Abstract
Automated termination analysis is a central topic in the research of term rewriting. In this talk, I will first review the theoretical foundation of termination of term rewriting, leading to the recently established tuple interpretation method. Then I will present an Isabelle/HOL formalization of the theory. Although the formalization is based on the existing library IsaFoR (Isabelle Formalization of Rewriting), the present work takes another approach of representing relations (predicates rather than sets) so that the notation is more human friendly. Then I will present a unified implementation of the termination analysis techniques via SMT encoding, leading to the termination prover NaTT. Many tools have been developed for termination analysis and have been competing annually in termCOMP (Termination Competition) for two decades. At the end of the talk, I will share my experience in organizing termCOMP in the last five years.
Cite as
Akihisa Yamada. Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition (Invited Talk). In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 4:1-4:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{yamada:LIPIcs.FSCD.2023.4,
author = {Yamada, Akihisa},
title = {{Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {4:1--4:5},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.4},
URN = {urn:nbn:de:0030-drops-179882},
doi = {10.4230/LIPIcs.FSCD.2023.4},
annote = {Keywords: Term rewriting, Termination, Isabelle/HOL, Competition}
}
Document
Homotopy Type Theory as Internal Languages of Diagrams of ∞-Logoses
Abstract
We show that certain diagrams of ∞-logoses are reconstructed in internal languages of their oplax limits via lex, accessible modalities, which enables us to use plain homotopy type theory to reason about not only a single ∞-logos but also a diagram of ∞-logoses. This also provides a higher dimensional version of Sterling’s synthetic Tait computability - a type theory for higher dimensional logical relations.
Cite as
Taichi Uemura. Homotopy Type Theory as Internal Languages of Diagrams of ∞-Logoses. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{uemura:LIPIcs.FSCD.2023.5,
author = {Uemura, Taichi},
title = {{Homotopy Type Theory as Internal Languages of Diagrams of ∞-Logoses}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {5:1--5:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.5},
URN = {urn:nbn:de:0030-drops-179897},
doi = {10.4230/LIPIcs.FSCD.2023.5},
annote = {Keywords: Homotopy type theory, ∞-logos, ∞-topos, oplax limit, Artin gluing, modality, synthetic Tait computability, logical relation}
}
Document
The Formal Theory of Monads, Univalently
Abstract
We develop the formal theory of monads, as established by Street, in univalent foundations. This allows us to formally reason about various kinds of monads on the right level of abstraction. In particular, we define the bicategory of monads internal to a bicategory, and prove that it is univalent. We also define Eilenberg-Moore objects, and we show that both Eilenberg-Moore categories and Kleisli categories give rise to Eilenberg-Moore objects. Finally, we relate monads and adjunctions in arbitrary bicategories. Our work is formalized in Coq using the https://github.com/UniMath/UniMath library.
Cite as
Niels van der Weide. The Formal Theory of Monads, Univalently. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{vanderweide:LIPIcs.FSCD.2023.6,
author = {van der Weide, Niels},
title = {{The Formal Theory of Monads, Univalently}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {6:1--6:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.6},
URN = {urn:nbn:de:0030-drops-179904},
doi = {10.4230/LIPIcs.FSCD.2023.6},
annote = {Keywords: bicategory theory, univalent foundations, formalization, monads, Coq}
}
Document
Automata-Based Verification of Relational Properties of Functions over Algebraic Data Structures
Abstract
This paper is concerned with automatically proving properties about the input-output relation of functional programs operating over algebraic data types. Recent results show how to approximate the image of a functional program using a regular tree language. Though expressive, those techniques cannot prove properties relating the input and the output of a function, e.g., proving that the output of a function reversing a list has the same length as the input list. In this paper, we built upon those results and define a procedure to compute or over-approximate such a relation. Instead of representing the image of a function by a regular set of terms, we represent (an approximation of) the input-output relation by a regular set of tuples of terms. Regular languages of tuples of terms are recognized using a tree automaton recognizing convolutions of terms, where a convolution transforms a tuple of terms into a term built on tuples of symbols. Both the program and the properties are transformed into predicates and Constrained Horn clauses (CHCs). Then, using an Implication Counter Example procedure (ICE), we infer a model of the clauses, associating to each predicate a regular relation. In this ICE procedure, checking if a given model satisfies the clauses is undecidable in general. We overcome undecidability by proposing an incomplete but sound inference procedure for such relational regular properties. Though the procedure is incomplete, its implementation performs well on 120 examples. It efficiently proves non-trivial relational properties or finds counter-examples.
Cite as
Théo Losekoot, Thomas Genet, and Thomas Jensen. Automata-Based Verification of Relational Properties of Functions over Algebraic Data Structures. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 7:1-7:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{losekoot_et_al:LIPIcs.FSCD.2023.7,
author = {Losekoot, Th\'{e}o and Genet, Thomas and Jensen, Thomas},
title = {{Automata-Based Verification of Relational Properties of Functions over Algebraic Data Structures}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {7:1--7:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.7},
URN = {urn:nbn:de:0030-drops-179915},
doi = {10.4230/LIPIcs.FSCD.2023.7},
annote = {Keywords: Formal verification, Tree automata, Constrained Horn Clauses, Model inference, Relational properties, Algebraic datatypes}
}
Document
The Sum-Product Algorithm For Quantitative Multiplicative Linear Logic
Abstract
We consider an extension of multiplicative linear logic which encompasses bayesian networks and expresses samples sharing and marginalisation with the polarised rules of contraction and weakening. We introduce the necessary formalism to import exact inference algorithms from bayesian networks, giving the sum-product algorithm as an example of calculating the weighted relational semantics of a multiplicative proof-net improving runtime performance by storing intermediate results.
Cite as
Thomas Ehrhard, Claudia Faggian, and Michele Pagani. The Sum-Product Algorithm For Quantitative Multiplicative Linear Logic. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{ehrhard_et_al:LIPIcs.FSCD.2023.8,
author = {Ehrhard, Thomas and Faggian, Claudia and Pagani, Michele},
title = {{The Sum-Product Algorithm For Quantitative Multiplicative Linear Logic}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {8:1--8:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.8},
URN = {urn:nbn:de:0030-drops-179926},
doi = {10.4230/LIPIcs.FSCD.2023.8},
annote = {Keywords: Linear Logic, Proof-Nets, Denotational Semantics, Probabilistic Programming}
}
Document
Generalized Newman’s Lemma for Discrete and Continuous Systems
Abstract
We propose a generalization of Newman’s lemma which gives a criterion of confluence for a wide class of not-necessarily-terminating abstract rewriting systems. We show that ordinary Newman’s lemma for terminating systems can be considered as a corollary of this criterion. We describe a formalization of the proposed generalized Newman’s lemma in Isabelle proof assistant using HOL logic.
Cite as
Ievgen Ivanov. Generalized Newman’s Lemma for Discrete and Continuous Systems. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{ivanov:LIPIcs.FSCD.2023.9,
author = {Ivanov, Ievgen},
title = {{Generalized Newman’s Lemma for Discrete and Continuous Systems}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {9:1--9:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.9},
URN = {urn:nbn:de:0030-drops-179936},
doi = {10.4230/LIPIcs.FSCD.2023.9},
annote = {Keywords: abstract rewriting system, confluence, discrete-continuous systems, proof assistant, formal proof}
}
Document
E-Unification for Second-Order Abstract Syntax
Abstract
Higher-order unification (HOU) concerns unification of (extensions of) λ-calculus and can be seen as an instance of equational unification (E-unification) modulo βη-equivalence of λ-terms. We study equational unification of terms in languages with arbitrary variable binding constructions modulo arbitrary second-order equational theories. Abstract syntax with general variable binding and parametrised metavariables allows us to work with arbitrary binders without committing to λ-calculus or use inconvenient and error-prone term encodings, leading to a more flexible framework. In this paper, we introduce E-unification for second-order abstract syntax and describe a unification procedure for such problems, merging ideas from both full HOU and general E-unification. We prove that the procedure is sound and complete.
Cite as
Nikolai Kudasov. E-Unification for Second-Order Abstract Syntax. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 10:1-10:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{kudasov:LIPIcs.FSCD.2023.10,
author = {Kudasov, Nikolai},
title = {{E-Unification for Second-Order Abstract Syntax}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {10:1--10:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.10},
URN = {urn:nbn:de:0030-drops-179944},
doi = {10.4230/LIPIcs.FSCD.2023.10},
annote = {Keywords: E-unification, higher-order unification, second-order abstract syntax}
}
Document
Two Decreasing Measures for Simply Typed λ-Terms
Abstract
This paper defines two decreasing measures for terms of the simply typed λ-calculus, called the 𝒲-measure and the 𝒯^{𝐦}-measure. A decreasing measure is a function that maps each typable λ-term to an element of a well-founded ordering, in such a way that contracting any β-redex decreases the value of the function, entailing strong normalization. Both measures are defined constructively, relying on an auxiliary calculus, a non-erasing variant of the λ-calculus. In this system, dubbed the λ^{𝐦}-calculus, each β-step creates a "wrapper" containing a copy of the argument that cannot be erased and cannot interact with the context in any other way. Both measures rely crucially on the observation, known to Turing and Prawitz, that contracting a redex cannot create redexes of higher degree, where the degree of a redex is defined as the height of the type of its λ-abstraction. The 𝒲-measure maps each λ-term to a natural number, and it is obtained by evaluating the term in the λ^{𝐦}-calculus and counting the number of remaining wrappers. The 𝒯^{𝐦}-measure maps each λ-term to a structure of nested multisets, where the nesting depth is proportional to the maximum redex degree.
Cite as
Pablo Barenbaum and Cristian Sottile. Two Decreasing Measures for Simply Typed λ-Terms. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{barenbaum_et_al:LIPIcs.FSCD.2023.11,
author = {Barenbaum, Pablo and Sottile, Cristian},
title = {{Two Decreasing Measures for Simply Typed \lambda-Terms}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {11:1--11:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.11},
URN = {urn:nbn:de:0030-drops-179956},
doi = {10.4230/LIPIcs.FSCD.2023.11},
annote = {Keywords: Lambda Calculus, Rewriting, Termination, Strong Normalization, Simple Types}
}
Document
Hydra Battles and AC Termination
Abstract
We present a new encoding of the Battle of Hercules and Hydra as a rewrite system with AC symbols. Unlike earlier term rewriting encodings, it faithfully models any strategy of Hercules to beat Hydra. To prove the termination of our encoding, we employ type introduction in connection with many-sorted semantic labeling for AC rewriting and AC-RPO.
Cite as
Nao Hirokawa and Aart Middeldorp. Hydra Battles and AC Termination. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{hirokawa_et_al:LIPIcs.FSCD.2023.12,
author = {Hirokawa, Nao and Middeldorp, Aart},
title = {{Hydra Battles and AC Termination}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {12:1--12:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.12},
URN = {urn:nbn:de:0030-drops-179965},
doi = {10.4230/LIPIcs.FSCD.2023.12},
annote = {Keywords: battle of Hercules and Hydra, term rewriting, termination}
}
Document
Strategies as Resource Terms, and Their Categorical Semantics
Abstract
As shown by Tsukada and Ong, simply-typed, normal and η-long resource terms correspond to plays in Hyland-Ong games, quotiented by Melliès' homotopy equivalence. Though inspiring, their proof is indirect, relying on the injectivity of the relational model {w.r.t.} both sides of the correspondence - in particular, the dynamics of the resource calculus is taken into account only via the compatibility of the relational model with the composition of normal terms defined by normalization.
In the present paper, we revisit and extend these results. Our first contribution is to restate the correspondence by considering causal structures we call augmentations, which are canonical representatives of Hyland-Ong plays up to homotopy. This allows us to give a direct and explicit account of the connection with normal resource terms. As a second contribution, we extend this account to the reduction of resource terms: building on a notion of strategies as weighted sums of augmentations, we provide a denotational model of the resource calculus, invariant under reduction. A key step - and our third contribution - is a categorical model we call a resource category, which is to the resource calculus what differential categories are to the differential λ-calculus.
Cite as
Lison Blondeau-Patissier, Pierre Clairambault, and Lionel Vaux Auclair. Strategies as Resource Terms, and Their Categorical Semantics. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 13:1-13:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{blondeaupatissier_et_al:LIPIcs.FSCD.2023.13,
author = {Blondeau-Patissier, Lison and Clairambault, Pierre and Vaux Auclair, Lionel},
title = {{Strategies as Resource Terms, and Their Categorical Semantics}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {13:1--13:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.13},
URN = {urn:nbn:de:0030-drops-179976},
doi = {10.4230/LIPIcs.FSCD.2023.13},
annote = {Keywords: Resource calculus, Game semantics, Categorical semantics}
}
Document
Rewriting Modulo Traced Comonoid Structure
Abstract
In this paper we adapt previous work on rewriting string diagrams using hypergraphs to the case where the underlying category has a traced comonoid structure, in which wires can be forked and the outputs of a morphism can be connected to its input. Such a structure is particularly interesting because any traced Cartesian (dataflow) category has an underlying traced comonoid structure. We show that certain subclasses of hypergraphs are fully complete for traced comonoid categories: that is to say, every term in such a category has a unique corresponding hypergraph up to isomorphism, and from every hypergraph with the desired properties, a unique term in the category can be retrieved up to the axioms of traced comonoid categories. We also show how the framework of double pushout rewriting (DPO) can be adapted for traced comonoid categories by characterising the valid pushout complements for rewriting in our setting. We conclude by presenting a case study in the form of recent work on an equational theory for sequential circuits: circuits built from primitive logic gates with delay and feedback. The graph rewriting framework allows for the definition of an operational semantics for sequential circuits.
Cite as
Dan R. Ghica and George Kaye. Rewriting Modulo Traced Comonoid Structure. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 14:1-14:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{ghica_et_al:LIPIcs.FSCD.2023.14,
author = {Ghica, Dan R. and Kaye, George},
title = {{Rewriting Modulo Traced Comonoid Structure}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {14:1--14:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.14},
URN = {urn:nbn:de:0030-drops-179983},
doi = {10.4230/LIPIcs.FSCD.2023.14},
annote = {Keywords: symmetric traced monoidal categories, string diagrams, graph rewriting, comonoid structure, double pushout rewriting}
}
Document
Cost-Size Semantics for Call-By-Value Higher-Order Rewriting
Abstract
Higher-order rewriting is a framework in which higher-order programs can be described by transformation rules on expressions. A computation occurs by transforming an expression into another using such rules. This step-by-step computation model induced by rewriting naturally gives rise to a notion of complexity as the number of steps needed to reduce expressions to a normal form, i.e., an expression that cannot be reduced further. The study of complexity analysis focuses on the development of automatable techniques to provide bounds to this number. In this paper, we consider a form of higher-order rewriting with a call-by-value evaluation strategy, so as to model call-by-value programs. We provide a cost-size semantics: a class of algebraic interpretations to map terms to tuples which bound both the reduction cost and the size of normal forms.
Cite as
Cynthia Kop and Deivid Vale. Cost-Size Semantics for Call-By-Value Higher-Order Rewriting. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 15:1-15:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{kop_et_al:LIPIcs.FSCD.2023.15,
author = {Kop, Cynthia and Vale, Deivid},
title = {{Cost-Size Semantics for Call-By-Value Higher-Order Rewriting}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {15:1--15:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.15},
URN = {urn:nbn:de:0030-drops-179993},
doi = {10.4230/LIPIcs.FSCD.2023.15},
annote = {Keywords: Call-by-Value Evaluation, Complexity Theory, Higher-Order Rewriting}
}
Document
Categorical Coherence from Term Rewriting Systems
Abstract
The celebrated Squier theorem allows to prove coherence properties of algebraic structures, such as MacLane’s coherence theorem for monoidal categories, based on rewriting techniques. We are interested here in extending the theory and associated tools simultaneously in two directions. Firstly, we want to take in account situations where coherence is partial, in the sense that it only applies for a subset of structural morphisms (for instance, in the case of the coherence theorem for symmetric monoidal categories, we do not want to strictify the symmetry). Secondly, we are interested in structures where variables can be duplicated or erased. We develop theorems and rewriting techniques in order to achieve this, first in the setting of abstract rewriting systems, and then extend them to term rewriting systems, suitably generalized in order to take coherence in account. As an illustration of our results, we explain how to recover the coherence theorems for monoidal and symmetric monoidal categories.
Cite as
Samuel Mimram. Categorical Coherence from Term Rewriting Systems. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{mimram:LIPIcs.FSCD.2023.16,
author = {Mimram, Samuel},
title = {{Categorical Coherence from Term Rewriting Systems}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {16:1--16:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.16},
URN = {urn:nbn:de:0030-drops-180009},
doi = {10.4230/LIPIcs.FSCD.2023.16},
annote = {Keywords: coherence, rewriting system, Lawvere theory}
}
Document
Convolution Products on Double Categories and Categorification of Rule Algebras
Abstract
Motivated by compositional categorical rewriting theory, we introduce a convolution product over presheaves of double categories which generalizes the usual Day tensor product of presheaves of monoidal categories. One interesting aspect of the construction is that this convolution product is in general only oplax associative. For that reason, we identify several classes of double categories for which the convolution product is not just oplax associative, but fully associative. This includes in particular framed bicategories on the one hand, and double categories of compositional rewriting theories on the other. For the latter, we establish a formula which justifies the view that the convolution product categorifies the rule algebra product.
Cite as
Nicolas Behr, Paul-André Melliès, and Noam Zeilberger. Convolution Products on Double Categories and Categorification of Rule Algebras. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 17:1-17:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{behr_et_al:LIPIcs.FSCD.2023.17,
author = {Behr, Nicolas and Melli\`{e}s, Paul-Andr\'{e} and Zeilberger, Noam},
title = {{Convolution Products on Double Categories and Categorification of Rule Algebras}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {17:1--17:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.17},
URN = {urn:nbn:de:0030-drops-180017},
doi = {10.4230/LIPIcs.FSCD.2023.17},
annote = {Keywords: Categorical rewriting, double pushout, sesqui-pushout, double categories, convolution product, presheaf categories, framed bicategories, opfibrations, rule algebra}
}
Document
For the Metatheory of Type Theory, Internal Sconing Is Enough
Abstract
Metatheorems about type theories are often proven by interpreting the syntax into models constructed using categorical gluing. We propose to use only sconing (gluing along a global section functor) instead of general gluing. The sconing is performed internally to a presheaf category, and we recover the original glued model by externalization.
Our method relies on constructions involving two notions of models: first-order models (with explicit contexts) and higher-order models (without explicit contexts). Sconing turns a displayed higher-order model into a displayed first-order model.
Using these, we derive specialized induction principles for the syntax of type theory. The input of such an induction principle is a boilerplate-free description of its motives and methods, not mentioning contexts. The output is a section with computation rules specified in the same internal language. We illustrate our framework by proofs of canonicity and normalization for type theory.
Cite as
Rafaël Bocquet, Ambrus Kaposi, and Christian Sattler. For the Metatheory of Type Theory, Internal Sconing Is Enough. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 18:1-18:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{bocquet_et_al:LIPIcs.FSCD.2023.18,
author = {Bocquet, Rafa\"{e}l and Kaposi, Ambrus and Sattler, Christian},
title = {{For the Metatheory of Type Theory, Internal Sconing Is Enough}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {18:1--18:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.18},
URN = {urn:nbn:de:0030-drops-180029},
doi = {10.4230/LIPIcs.FSCD.2023.18},
annote = {Keywords: type theory, presheaves, canonicity, normalization, sconing, gluing}
}
Document
The Logical Essence of Compiling with Continuations
Abstract
The essence of compiling with continuations is that conversion to continuation-passing style (CPS) is equivalent to a source language transformation converting to administrative normal form (ANF). Taking as source language Moggi’s computational lambda-calculus (λ{𝖢}), we define an alternative to the CPS-translation with target in the sequent calculus LJQ, named value-filling style (VFS) translation, and making use of the ability of the sequent calculus to represent contexts formally. The VFS-translation requires no type translation: indeed, double negations are introduced only when encoding the VFS target language in the CPS target language. This optional encoding, when composed with the VFS-translation reconstructs the original CPS-translation. Going back to direct style, the "essence" of the VFS-translation is that it reveals a new sublanguage of ANF, the value-enclosed style (VES), next to another one, the continuation-enclosing style (CES): such an alternative is due to a dilemma in the syntax of λ{𝖢}, concerning how to expand the application constructor. In the typed scenario, VES and CES correspond to an alternative between two proof systems for call-by-value, LJQ and natural deduction with generalized applications, confirming proof theory as a foundation for intermediate representations.
Cite as
José Espírito Santo and Filipa Mendes. The Logical Essence of Compiling with Continuations. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 19:1-19:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{espiritosanto_et_al:LIPIcs.FSCD.2023.19,
author = {Esp{\'\i}rito Santo, Jos\'{e} and Mendes, Filipa},
title = {{The Logical Essence of Compiling with Continuations}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {19:1--19:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.19},
URN = {urn:nbn:de:0030-drops-180036},
doi = {10.4230/LIPIcs.FSCD.2023.19},
annote = {Keywords: Continuation-passing style, Sequent calculus, Generalized applications, Administrative normal form}
}
Document
On the Lattice of Program Metrics
Abstract
In this paper we are concerned with understanding the nature of program metrics for calculi with higher-order types, seen as natural generalizations of program equivalences. Some of the metrics we are interested in are well-known, such as those based on the interpretation of terms in metric spaces and those obtained by generalizing observational equivalence. We also introduce a new one, called the interactive metric, built by applying the well-known Int-Construction to the category of metric complete partial orders. Our aim is then to understand how these metrics relate to each other, i.e., whether and in which cases one such metric refines another, in analogy with corresponding well-studied problems about program equivalences. The results we obtain are twofold. We first show that the metrics of semantic origin, i.e., the denotational and interactive ones, lie in between the observational and equational metrics and that in some cases, these inclusions are strict. Then, we give a result about the relationship between the denotational and interactive metrics, revealing that the former is less discriminating than the latter. All our results are given for a linear lambda-calculus, and some of them can be generalized to calculi with graded comonads, in the style of Fuzz.
Cite as
Ugo Dal Lago, Naohiko Hoshino, and Paolo Pistone. On the Lattice of Program Metrics. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{dallago_et_al:LIPIcs.FSCD.2023.20,
author = {Dal Lago, Ugo and Hoshino, Naohiko and Pistone, Paolo},
title = {{On the Lattice of Program Metrics}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {20:1--20:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.20},
URN = {urn:nbn:de:0030-drops-180049},
doi = {10.4230/LIPIcs.FSCD.2023.20},
annote = {Keywords: Metrics, Lambda Calculus, Linear Types}
}
Document
Unifying Graded Linear Logic and Differential Operators
Abstract
Linear Logic refines Classical Logic by taking into account the resources used during the proof and program computation. In the past decades, it has been extended to various frameworks. The most famous are indexed linear logics which can describe the resource management or the complexity analysis of a program. From another perspective, Differential Linear Logic is an extension which allows the linearization of proofs. In this article, we merge these two directions by first defining a differential version of Graded linear logic: this is made by indexing exponential connectives with a monoid of differential operators. We prove that it is equivalent to a graded version of previously defined extension of finitary differential linear logic. We give a denotational model of our logic, based on distribution theory and linear partial differential operators with constant coefficients.
Cite as
Flavien Breuvart, Marie Kerjean, and Simon Mirwasser. Unifying Graded Linear Logic and Differential Operators. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 21:1-21:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{breuvart_et_al:LIPIcs.FSCD.2023.21,
author = {Breuvart, Flavien and Kerjean, Marie and Mirwasser, Simon},
title = {{Unifying Graded Linear Logic and Differential Operators}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {21:1--21:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.21},
URN = {urn:nbn:de:0030-drops-180052},
doi = {10.4230/LIPIcs.FSCD.2023.21},
annote = {Keywords: Linear Logic, Denotational Semantics, Functional Analysis, Graded Logic}
}
Document
α-Avoidance
Abstract
When substitutions and bindings interact, there is a risk of undesired side effects if the substitution is applied naïvely. The λ-calculus captures this phenomenon concretely, as β-reduction may require the renaming of bound variables to avoid variable capture. In this paper we introduce α-paths as an estimation for α-avoidance, roughly expressing that α-conversions are not required to prevent variable capture. These paths provide a novel method to analyse and predict the potential need for α in different calculi. In particular, we show how α-path characterises α-avoidance for several sub-calculi of the λ-calculus like (i) developments, (ii) affine/linear λ-calculi, (iii) the weak λ-calculus, (iv) μ-unfolding and (iv) finally the safe λ-calculus. Furthermore, we study the unavoidability of α-conversions in untyped and simply-typed λ-calculi and prove undecidability of the need of α-conversions for (leftmost-outermost reductions) in the untyped λ-calculus. To ease the work with α-paths, we have implemented the method and the tool is publicly available.
Cite as
Samuel Frontull, Georg Moser, and Vincent van Oostrom. α-Avoidance. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 22:1-22:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{frontull_et_al:LIPIcs.FSCD.2023.22,
author = {Frontull, Samuel and Moser, Georg and van Oostrom, Vincent},
title = {{\alpha-Avoidance}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {22:1--22:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.22},
URN = {urn:nbn:de:0030-drops-180068},
doi = {10.4230/LIPIcs.FSCD.2023.22},
annote = {Keywords: \lambda-calculus, variable capture, \alpha-conversion, developments, safe \lambda-calculus, undecidability}
}
Document
Partial Model Checking and Partial Model Synthesis in LTL Using a Tableau-Based Approach
Abstract
In the process of designing a computer system S and checking whether an abstract model ℳ of S verifies a given specification property η, one might have only a partial knowledge of the model, either because ℳ has not yet been completely defined (constructed) by the designer, or because it is not completely observable by the verifier. This leads to new verification problems, subsuming satisfiability and model checking as special cases. We state and discuss these problems in the case of LTL specifications, and develop a uniform tableau-based approach for their solutions.
Cite as
Serenella Cerrito, Valentin Goranko, and Sophie Paillocher. Partial Model Checking and Partial Model Synthesis in LTL Using a Tableau-Based Approach. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 23:1-23:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{cerrito_et_al:LIPIcs.FSCD.2023.23,
author = {Cerrito, Serenella and Goranko, Valentin and Paillocher, Sophie},
title = {{Partial Model Checking and Partial Model Synthesis in LTL Using a Tableau-Based Approach}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {23:1--23:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.23},
URN = {urn:nbn:de:0030-drops-180075},
doi = {10.4230/LIPIcs.FSCD.2023.23},
annote = {Keywords: Linear temporal logic LTL, partial transition systems, partial model checking, partial model synthesis, tableaux}
}
Document
Combinatory Logic and Lambda Calculus Are Equal, Algebraically
Abstract
It is well-known that extensional lambda calculus is equivalent to extensional combinatory logic. In this paper we describe a formalisation of this fact in Cubical Agda. The distinguishing features of our formalisation are the following: (i) Both languages are defined as generalised algebraic theories, the syntaxes are intrinsically typed and quotiented by conversion; we never mention preterms or break the quotients in our construction. (ii) Typing is a parameter, thus the un(i)typed and simply typed variants are special cases of the same proof. (iii) We define syntaxes as quotient inductive-inductive types (QIITs) in Cubical Agda; we prove the equivalence and (via univalence) the equality of these QIITs; we do not rely on any axioms, the conversion functions all compute and can be experimented with.
Cite as
Thorsten Altenkirch, Ambrus Kaposi, Artjoms Šinkarovs, and Tamás Végh. Combinatory Logic and Lambda Calculus Are Equal, Algebraically. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{altenkirch_et_al:LIPIcs.FSCD.2023.24,
author = {Altenkirch, Thorsten and Kaposi, Ambrus and \v{S}inkarovs, Artjoms and V\'{e}gh, Tam\'{a}s},
title = {{Combinatory Logic and Lambda Calculus Are Equal, Algebraically}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {24:1--24:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.24},
URN = {urn:nbn:de:0030-drops-180086},
doi = {10.4230/LIPIcs.FSCD.2023.24},
annote = {Keywords: Combinatory logic, lambda calculus, quotient inductive types, Cubical Agda}
}
Document
Quotients and Extensionality in Relational Doctrines
Abstract
Taking a quotient roughly means changing the notion of equality on a given object, set or type. In a quantitative setting, equality naturally generalises to a distance, measuring how much elements are similar instead of just stating their equivalence. Hence, quotients can be understood quantitatively as a change of distance. Quotients are crucial in many constructions both in mathematics and computer science and have been widely studied using categorical tools. Among them, Lawvere’s doctrines stand out, providing a fairly simple functorial framework capable to unify many notions of quotient and related constructions. However, abstracting usual predicate logics, they cannot easily deal with quantitative settings. In this paper, we show how, combining doctrines and the calculus of relations, one can unify quantitative and usual quotients in a common picture. More in detail, we introduce relational doctrines as a functorial description of (the core of) the calculus of relations. Then, we define quotients and a universal construction adding them to any relational doctrine, generalising the quotient completion of existential elementary doctrine and also recovering many quantitative examples. This construction deals with an intensional notion of quotient and breaks extensional equality of morphisms. Then, we describe another construction forcing extensionality, showing how it abstracts several notions of separation in metric and topological structures.
Cite as
Francesco Dagnino and Fabio Pasquali. Quotients and Extensionality in Relational Doctrines. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 25:1-25:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{dagnino_et_al:LIPIcs.FSCD.2023.25,
author = {Dagnino, Francesco and Pasquali, Fabio},
title = {{Quotients and Extensionality in Relational Doctrines}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {25:1--25:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.25},
URN = {urn:nbn:de:0030-drops-180090},
doi = {10.4230/LIPIcs.FSCD.2023.25},
annote = {Keywords: Quantitative Reasoning, Calculus of Relations, Hyperdoctrines, Metric Spaces}
}
Document
Type Isomorphisms for Multiplicative-Additive Linear Logic
Abstract
We characterize type isomorphisms in the multiplicative-additive fragment of linear logic (MALL), and thus for ⋆-autonomous categories with finite products, extending a result for the multiplicative fragment by Balat and Di Cosmo [Vincent Balat and Roberto Di Cosmo, 1999]. This yields a much richer equational theory involving distributivity and annihilation laws. The unit-free case is obtained by relying on the proof-net syntax introduced by Hughes and Van Glabbeek [Dominic Hughes and Rob van Glabbeek, 2005]. We then use the sequent calculus to extend our results to full MALL (including all units).
Cite as
Rémi Di Guardia and Olivier Laurent. Type Isomorphisms for Multiplicative-Additive Linear Logic. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 26:1-26:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{diguardia_et_al:LIPIcs.FSCD.2023.26,
author = {Di Guardia, R\'{e}mi and Laurent, Olivier},
title = {{Type Isomorphisms for Multiplicative-Additive Linear Logic}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {26:1--26:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.26},
URN = {urn:nbn:de:0030-drops-180103},
doi = {10.4230/LIPIcs.FSCD.2023.26},
annote = {Keywords: Linear Logic, Type Isomorphisms, Multiplicative-Additive fragment, Proof nets, Sequent calculus, Star-autonomous categories with finite products}
}
Document
Cyclic Proofs for Arithmetical Inductive Definitions
Abstract
We investigate the cyclic proof theory of extensions of Peano Arithmetic by (finitely iterated) inductive definitions. Such theories are essential to proof theoretic analyses of certain "impredicative" theories; moreover, our cyclic systems naturally subsume Simpson’s Cyclic Arithmetic.
Our main result is that cyclic and inductive systems for arithmetical inductive definitions are equally powerful. We conduct a metamathematical argument, formalising the soundness of cyclic proofs within second-order arithmetic by a form of induction on closure ordinals, thence appealing to conservativity results. This approach is inspired by those of Simpson and Das for Cyclic Arithmetic, however we must further address a difficulty: the closure ordinals of our inductive definitions (around Church-Kleene) far exceed the proof theoretic ordinal of the appropriate metatheory (around Bachmann-Howard), so explicit induction on their notations is not possible. For this reason, we rather rely on formalisation of the theory of (recursive) ordinals within second-order arithmetic.
Cite as
Anupam Das and Lukas Melgaard. Cyclic Proofs for Arithmetical Inductive Definitions. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{das_et_al:LIPIcs.FSCD.2023.27,
author = {Das, Anupam and Melgaard, Lukas},
title = {{Cyclic Proofs for Arithmetical Inductive Definitions}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {27:1--27:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.27},
URN = {urn:nbn:de:0030-drops-180119},
doi = {10.4230/LIPIcs.FSCD.2023.27},
annote = {Keywords: cyclic proofs, inductive definitions, arithmetic, fixed points, proof theory}
}
Document
Concurrent Realizability on Conjunctive Structures
Abstract
This work aims at exploring the algebraic structure of concurrent processes and their behavior independently of a particular formalism used to define them. We propose a new algebraic structure called conjunctive involutive monoidal algebra (CIMA) as a basis for an algebraic presentation of concurrent realizability, following ideas of the algebrization program already developed in the realm of classical and intuitionistic realizability. In particular, we show how any CIMA provides a sound interpretation of multiplicative linear logic. This new structure involves, in addition to the tensor and the orthogonal map, a parallel composition. We define a reference model of this structure as induced by a standard process calculus and we use this model to prove that parallel composition cannot be defined from the conjunctive structure alone.
Cite as
Emmanuel Beffara, Félix Castro, Mauricio Guillermo, and Étienne Miquey. Concurrent Realizability on Conjunctive Structures. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 28:1-28:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{beffara_et_al:LIPIcs.FSCD.2023.28,
author = {Beffara, Emmanuel and Castro, F\'{e}lix and Guillermo, Mauricio and Miquey, \'{E}tienne},
title = {{Concurrent Realizability on Conjunctive Structures}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {28:1--28:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.28},
URN = {urn:nbn:de:0030-drops-180124},
doi = {10.4230/LIPIcs.FSCD.2023.28},
annote = {Keywords: Realizability, Process Algebras, Concurrent Processes, Linear Logic}
}
Document
A Quantitative Version of Simple Types
Abstract
This work introduces a quantitative version of the simple type assignment system, starting from a suitable restriction of non-idempotent intersection types. The resulting system is decidable and has the same typability power as the simple type system; thus, assigning types to terms supplies the very same qualitative information given by simple types, but at the same time can provide some interesting quantitative information. It is well known that typability for simple types is equivalent to unification; we prove a similar result for the newly introduced system. More precisely, we show that typability is equivalent to a unification problem which is a non-trivial extension of the classical one: in addition to unification rules, our typing algorithm makes use of an expansion operation that increases the cardinality of multisets whenever needed.
Cite as
Daniele Pautasso and Simona Ronchi Della Rocca. A Quantitative Version of Simple Types. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 29:1-29:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{pautasso_et_al:LIPIcs.FSCD.2023.29,
author = {Pautasso, Daniele and Ronchi Della Rocca, Simona},
title = {{A Quantitative Version of Simple Types}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {29:1--29:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.29},
URN = {urn:nbn:de:0030-drops-180137},
doi = {10.4230/LIPIcs.FSCD.2023.29},
annote = {Keywords: \lambda-calculus, intersection types, unification}
}
Document
Knowledge Problems in Security Protocols: Going Beyond Subterm Convergent Theories
Abstract
We introduce a new form of restricted term rewrite system, the graph-embedded term rewrite system. These systems, and thus the name, are inspired by the graph minor relation and are more flexible extensions of the well-known homeomorphic-embedded property of term rewrite systems. As a motivating application area, we consider the symbolic analysis of security protocols, and more precisely the two knowledge problems defined by the deduction problem and the static equivalence problem. In this field restricted term rewrite systems, such as subterm convergent ones, have proven useful since the knowledge problems are decidable for such systems. However, many of the same decision procedures still work for examples of systems which are "beyond subterm convergent". However, the applicability of the corresponding decision procedures to these examples must often be proven on an individual basis. This is due to the problem that they don't fit into an existing syntactic definition for which the procedures are known to work. Here we show that many of these systems belong to a particular subclass of graph-embedded convergent systems, called contracting convergent systems. On the one hand, we show that the knowledge problems are decidable for the subclass of contracting convergent systems. On the other hand, we show that the knowledge problems are undecidable for the class of graph-embedded systems.
Cite as
Saraid Dwyer Satterfield, Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen. Knowledge Problems in Security Protocols: Going Beyond Subterm Convergent Theories. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{dwyersatterfield_et_al:LIPIcs.FSCD.2023.30,
author = {Dwyer Satterfield, Saraid and Erbatur, Serdar and Marshall, Andrew M. and Ringeissen, Christophe},
title = {{Knowledge Problems in Security Protocols: Going Beyond Subterm Convergent Theories}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {30:1--30:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.30},
URN = {urn:nbn:de:0030-drops-180148},
doi = {10.4230/LIPIcs.FSCD.2023.30},
annote = {Keywords: Term rewriting, security protocols, verification}
}
Document
Labelled Tableaux for Linear Time Bunched Implication Logic
Abstract
In this paper, we define the logic of Linear Temporal Bunched Implications (LTBI), a temporal extension of the Bunched Implications logic BI that deals with resource evolution over time, by combining the BI separation connectives and the LTL temporal connectives. We first present the syntax and semantics of LTBI and illustrate its expressiveness with a significant example. Then we introduce a tableau calculus with labels and constraints, called TLTBI, and prove its soundness w.r.t. the Kripke-style semantics of LTBI. Finally we discuss and analyze the issues that make the completeness of the calculus not trivial in the general case of unbounded timelines and explain how to solve the issues in the more restricted case of bounded timelines.
Cite as
Didier Galmiche and Daniel Méry. Labelled Tableaux for Linear Time Bunched Implication Logic. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 31:1-31:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{galmiche_et_al:LIPIcs.FSCD.2023.31,
author = {Galmiche, Didier and M\'{e}ry, Daniel},
title = {{Labelled Tableaux for Linear Time Bunched Implication Logic}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {31:1--31:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.31},
URN = {urn:nbn:de:0030-drops-180159},
doi = {10.4230/LIPIcs.FSCD.2023.31},
annote = {Keywords: Temporal Logic, Bunched Implication Logic, Labelled Deduction, Tableaux}
}
Document
Diller-Nahm Bar Recursion
Abstract
We present a generalization of Spector’s bar recursion to the Diller-Nahm variant of Gödel’s Dialectica interpretation. This generalized bar recursion collects witnesses of universal formulas in sets of approximation sequences to provide an interpretation to the double-negation shift principle. The interpretation is presented in a fully computational way, implementing sets via lists. We also present a demand-driven version of this extended bar recursion manipulating partial sequences rather than initial segments. We explain why in a Diller-Nahm context there seems to be several versions of this demand-driven bar recursion, but no canonical one.
Cite as
Valentin Blot. Diller-Nahm Bar Recursion. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 32:1-32:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{blot:LIPIcs.FSCD.2023.32,
author = {Blot, Valentin},
title = {{Diller-Nahm Bar Recursion}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {32:1--32:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.32},
URN = {urn:nbn:de:0030-drops-180164},
doi = {10.4230/LIPIcs.FSCD.2023.32},
annote = {Keywords: Dialectica, Bar recursion}
}
Document
Dinaturality Meets Genericity: A Game Semantics of Bounded Polymorphism
Abstract
We study subtyping and parametric polymorphism, with the aim of providing direct and tractable semantic representations of type systems with these expressive features. The liveness order uses the Player-Opponent duality of game semantics to give a simple representation of subtyping: we generalize it to include graphs extracted directly from second-order intuitionistic types, and use the resulting complete lattice to interpret bounded polymorphic types in the style of System F_<:, but with a more tractable subtyping relation.
To extend this to a semantics of terms, we use the type-derived graphs as arenas, on which strategies correspond to dinatural transformations with respect to the canonical coercions ("on the nose" copycats) induced by the liveness ordering. This relationship between the interpretation of generic and subtype polymorphism thus provides the basis of the semantics of our type system.
Cite as
James Laird. Dinaturality Meets Genericity: A Game Semantics of Bounded Polymorphism. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 33:1-33:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{laird:LIPIcs.FSCD.2023.33,
author = {Laird, James},
title = {{Dinaturality Meets Genericity: A Game Semantics of Bounded Polymorphism}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {33:1--33:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.33},
URN = {urn:nbn:de:0030-drops-180171},
doi = {10.4230/LIPIcs.FSCD.2023.33},
annote = {Keywords: Subtyping, Bounded Polymorphism, Game Semantics, Dinaturality}
}
Document
Representing Guardedness in Call-By-Value
Abstract
Like the notion of computation via (strong) monads serves to classify various flavours of impurity, including exceptions, non-determinism, probability, local and global store, the notion of guardedness classifies well-behavedness of cycles in various settings. In its most general form, the guardedness discipline applies to general symmetric monoidal categories and further specializes to Cartesian and co-Cartesian categories, where it governs guarded recursion and guarded iteration respectively. Here, even more specifically, we deal with the semantics of call-by-value guarded iteration. It was shown by Levy, Power and Thielecke that call-by-value languages can be generally interpreted in Freyd categories, but in order to represent effectful function spaces, such a category must canonically arise from a strong monad. We generalize this fact by showing that representing guarded effectful function spaces calls for certain parametrized monads (in the sense of Uustalu). This provides a description of guardedness as an intrinsic categorical property of programs, complementing the existing description of guardedness as a predicate on a category.
Cite as
Sergey Goncharov. Representing Guardedness in Call-By-Value. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 34:1-34:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{goncharov:LIPIcs.FSCD.2023.34,
author = {Goncharov, Sergey},
title = {{Representing Guardedness in Call-By-Value}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {34:1--34:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.34},
URN = {urn:nbn:de:0030-drops-180181},
doi = {10.4230/LIPIcs.FSCD.2023.34},
annote = {Keywords: Fine-grain call-by-value, Abstract guardedness, Freyd category, Kleisli category, Elgot iteration}
}