DROPS

Volume

LIPIcs, Volume 260

8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

FSCD 2023, July 3-6, 2023, Rome, Italy

Editors: Marco Gaboardi and Femke van Raamsdonk

Document

Invited Talk

DOI: 10.4230/LIPIcs.FSCD.2023.1

Nominal Techniques for Software Specification and Verification (Invited Talk)

Authors: Maribel Fernández

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

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.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

DOI: 10.4230/LIPIcs.FSCD.2023.2

How Can We Make Trustworthy AI? (Invited Talk)

Authors: Mateja Jamnik

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

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.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

DOI: 10.4230/LIPIcs.FSCD.2023.3

A Lambda Calculus Satellite (Invited Talk)

Authors: Giulio Manzonetto

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

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.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

DOI: 10.4230/LIPIcs.FSCD.2023.4

Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition (Invited Talk)

Authors: Akihisa Yamada

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

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.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

DOI: 10.4230/LIPIcs.FSCD.2023.5

Homotopy Type Theory as Internal Languages of Diagrams of ∞-Logoses

Authors: Taichi Uemura

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

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.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

DOI: 10.4230/LIPIcs.FSCD.2023.6

The Formal Theory of Monads, Univalently

Authors: Niels van der Weide

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

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.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

DOI: 10.4230/LIPIcs.FSCD.2023.7

Automata-Based Verification of Relational Properties of Functions over Algebraic Data Structures

Authors: Théo Losekoot, Thomas Genet, and Thomas Jensen

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

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.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

DOI: 10.4230/LIPIcs.FSCD.2023.8

The Sum-Product Algorithm For Quantitative Multiplicative Linear Logic

Authors: Thomas Ehrhard, Claudia Faggian, and Michele Pagani

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

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

DOI: 10.4230/LIPIcs.FSCD.2023.9

Generalized Newman’s Lemma for Discrete and Continuous Systems

Authors: Ievgen Ivanov

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

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.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

DOI: 10.4230/LIPIcs.FSCD.2023.10

E-Unification for Second-Order Abstract Syntax

Authors: Nikolai Kudasov

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

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.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

DOI: 10.4230/LIPIcs.FSCD.2023.11

Two Decreasing Measures for Simply Typed λ-Terms

Authors: Pablo Barenbaum and Cristian Sottile

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

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.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

DOI: 10.4230/LIPIcs.FSCD.2023.12

Hydra Battles and AC Termination

Authors: Nao Hirokawa and Aart Middeldorp

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

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.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

DOI: 10.4230/LIPIcs.FSCD.2023.13

Strategies as Resource Terms, and Their Categorical Semantics

Authors: Lison Blondeau-Patissier, Pierre Clairambault, and Lionel Vaux Auclair

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

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.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

DOI: 10.4230/LIPIcs.FSCD.2023.14

Rewriting Modulo Traced Comonoid Structure

Authors: Dan R. Ghica and George Kaye

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

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.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}
}

46 Search Results for "Gaboardi, Marco"

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Thanks for your feedback!

Could not send message