DROPS

Volume

LIPIcs, Volume 167

5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

FSCD 2020, June 29 to July 6, 2020, Paris, France (Virtual Conference)

Editors: Zena M. Ariola

Document

DOI: 10.4230/LIPIcs.CSL.2026.40

The Groupoid-Syntax of Type Theory Is a Set

Authors: Thorsten Altenkirch, Ambrus Kaposi, and Szumi Xie

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract

Categories with families (CwFs) have been used to define the semantics of type theory in type theory. In the setting of Homotopy Type Theory (HoTT), one of the limitations of the traditional notion of CwFs is the requirement to set-truncate types, which excludes models based on univalent categories, such as the standard set model. To address this limitation, we introduce the concept of a Groupoid Category with Families (GCwF). This framework truncates types at the groupoid level and incorporates coherence equations, providing a natural extension of the CwF framework when starting from a 1-category. We demonstrate that the initial GCwF for a type theory with a base family of sets and Π-types (groupoid-syntax) is set-truncated. Consequently, this allows us to utilize the conventional intrinsic syntax of type theory while enabling interpretations in semantically richer and more natural models. All constructions in this paper were formalised in Cubical Agda.

Cite as

Thorsten Altenkirch, Ambrus Kaposi, and Szumi Xie. The Groupoid-Syntax of Type Theory Is a Set. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 40:1-40:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{altenkirch_et_al:LIPIcs.CSL.2026.40,
  author =	{Altenkirch, Thorsten and Kaposi, Ambrus and Xie, Szumi},
  title =	{{The Groupoid-Syntax of Type Theory Is a Set}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{40:1--40:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.40},
  URN =		{urn:nbn:de:0030-drops-254650},
  doi =		{10.4230/LIPIcs.CSL.2026.40},
  annote =	{Keywords: Categorical models of type theory, category with families, groupoids, coherence, homotopy type theory}
}

Document

DOI: 10.4230/LIPIcs.CSL.2026.39

A Canonical Form for Universe Levels in Impredicative Type Theory

Authors: Yoan Géran

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract

The 0-imax-successor algebra, where imax: ℕ × ℕ → ℕ is the function defined by imax(n, 0) = 0 and imax(n, S(m)) = max(n, S(m)), is used to represent universe levels in impredicative type theory, in particular with universe polymorphism which introduces level variables, so it is present in proof systems such as Rocq and Lean. In particular, we need to know when two elements of this algebra are equivalent, and we may also want to decide the inequality. In this article, we introduce a canonical form for the terms of this algebra, and we provide a canonization algorithm. It permits deciding level equivalence by checking the canonical form equality, and also permits easily checking if a level is smaller than another one.

Cite as

Yoan Géran. A Canonical Form for Universe Levels in Impredicative Type Theory. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 39:1-39:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{geran:LIPIcs.CSL.2026.39,
  author =	{G\'{e}ran, Yoan},
  title =	{{A Canonical Form for Universe Levels in Impredicative Type Theory}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{39:1--39:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.39},
  URN =		{urn:nbn:de:0030-drops-254640},
  doi =		{10.4230/LIPIcs.CSL.2026.39},
  annote =	{Keywords: universe levels, canonical form, impredicativity, imax algebra}
}

Document

DOI: 10.4230/LIPIcs.CSL.2026.47

Useful Call-by-Value: A Semantic Interpretation via Quantitative Types

Authors: Pablo Barenbaum, Delia Kesner, and Mariana Milicich

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract

Useful evaluation is an optimised evaluation mechanism for functional programming languages. It relies on representing terms with sharing and imposing a restricted notion of useful substitutions, that intuitively disallows copying subterms that do not contribute to the progress of the computation. In particular, useful call-by-value evaluation optimises the standard call-by-value strategy by preserving its original semantics. This preservation result has been shown by means of syntactical rewriting techniques, difficult to adapt to alternative variants of the calculi at play. In this work, we present the first semantic model of useful call-by-value evaluation through the non-idempotent intersection type system 𝒰. Our first contribution is a characterisation of termination for useful call-by-value evaluation via system 𝒰. That is, a term is typable in system 𝒰 if and only if it terminates in the useful call-by-value strategy. As a second contribution, we show that system 𝒰 provides a quantitative interpretation for useful call-by-value evaluation, offering exact step-count information for program evaluation. Our third contribution is that termination in call-by-value and useful call-by-value are equivalent. This ensures in particular that call-by-value, which is (potentially) erasing, and useful call-by-value, which is non-erasing, are observationally equivalent. Even though the specification of the operational semantics of useful evaluation is highly complex, system 𝒰 is notably simple. As far as we know, system 𝒰 is one of the scarce quantitative type systems capturing exactly the substitution step-count for variables and abstractions in an open call-by-value strategy.

Cite as

Pablo Barenbaum, Delia Kesner, and Mariana Milicich. Useful Call-by-Value: A Semantic Interpretation via Quantitative Types. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 47:1-47:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{barenbaum_et_al:LIPIcs.CSL.2026.47,
  author =	{Barenbaum, Pablo and Kesner, Delia and Milicich, Mariana},
  title =	{{Useful Call-by-Value: A Semantic Interpretation via Quantitative Types}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{47:1--47:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.47},
  URN =		{urn:nbn:de:0030-drops-254721},
  doi =		{10.4230/LIPIcs.CSL.2026.47},
  annote =	{Keywords: Lambda calculus, Evaluation strategies, Call-by-Value, Useful Evaluation, Intersection types, Quantitative models}
}

Document

DOI: 10.4230/LIPIcs.CALCO.2025.10

EGGs Are Adhesive!

Authors: Roberto Biondo, Davide Castelnovo, and Fabio Gadducci

Published in: LIPIcs, Volume 342, 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Abstract

The use of rewriting-based visual formalisms is on the rise. In the formal methods community, this is due also to the introduction of adhesive categories, where most properties of classical approaches to graph transformation, such as those on parallelism and confluence, can be rephrased and proved in a general and uniform way. E-graphs (EGGs) are a formalism for program optimisation via an efficient implementation of equality saturation. In short, EGGs can be defined as (acyclic) term graphs with an additional notion of equivalence on nodes that is closed under the operators of the signature. Instead of replacing the components of a program, the optimisation step is performed by adding new components and linking them to the existing ones via an equivalence relation, until an optimal program is reached. This work describes EGGs via adhesive categories. Besides the benefits in itself of a formal presentation, which renders precise the properties of the data structure, the description of the addition of equivalent program components using standard graph transformation tools offers the advantages of the adhesive framework in modelling, for example, concurrent updates.

Cite as

Roberto Biondo, Davide Castelnovo, and Fabio Gadducci. EGGs Are Adhesive!. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{biondo_et_al:LIPIcs.CALCO.2025.10,
  author =	{Biondo, Roberto and Castelnovo, Davide and Gadducci, Fabio},
  title =	{{EGGs Are Adhesive!}},
  booktitle =	{11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
  pages =	{10:1--10:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-383-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{342},
  editor =	{C\^{i}rstea, Corina and Knapp, Alexander},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.10},
  URN =		{urn:nbn:de:0030-drops-235690},
  doi =		{10.4230/LIPIcs.CALCO.2025.10},
  annote =	{Keywords: Hypergraphs, terms graphs, e-graphs, adhesive categories}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.FSCD.2025.1

Computation First: Rebuilding Constructivism with Effects (Invited Talk)

Authors: Liron Cohen

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract

Constructive logic and type theory have traditionally been grounded in pure, effect-free model of computation. This paper argues that such a restriction is not a foundational necessity but a historical artifact, and it advocates for a broader perspective of effectful constructivism, where computational effects, such as state, non-determinism, and exceptions, are directly and internally embedded in the logical and computational foundations. We begin by surveying examples where effects reshape logical principles, and then outline three approaches to effectful constructivism, focusing on realizability models: Monadic Combinatory Algebras, which extend classical partial combinatory algebras with effectful computation; Evidenced Frames, a flexible semantic structure capable of uniformly capturing a wide range of effects; and Effectful Higher-Order Logic (EffHOL), a syntactic approach that directly translates logical propositions into specifications for effectful programs. We further illustrate how concrete type theories can internalize effects, via the family of type theories TT^□_C. Together, these works demonstrate that effectful constructivism is not merely possible but a natural and robust extension of traditional frameworks.

Cite as

Liron Cohen. Computation First: Rebuilding Constructivism with Effects (Invited Talk). In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 1:1-1:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cohen:LIPIcs.FSCD.2025.1,
  author =	{Cohen, Liron},
  title =	{{Computation First: Rebuilding Constructivism with Effects}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{1:1--1:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.1},
  URN =		{urn:nbn:de:0030-drops-236167},
  doi =		{10.4230/LIPIcs.FSCD.2025.1},
  annote =	{Keywords: Effectful constructivism, realizability, type theory, monadic combinatory algebras, evidenced frame}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2025.5

The Cost of Skeletal Call-By-Need, Smoothly

Authors: Beniamino Accattoli, Francesco Magliocca, Loïc Peyrot, and Claudio Sacerdoti Coen

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract

Skeletal call-by-need is an optimization of call-by-need evaluation also known as "fully lazy sharing": when the duplication of a value has to take place, it is first split into "skeleton", which is then duplicated, and "flesh" which is instead kept shared. Here, we provide two cost analyses of skeletal call-by-need. Firstly, we provide a family of terms showing that skeletal call-by-need can be asymptotically exponentially faster than call-by-need in both time and space; it is the first such evidence, to our knowledge. Secondly, we prove that skeletal call-by-need can be implemented efficiently, that is, with bi-linear overhead. This result is obtained by providing a new smooth presentation of ideas by Shivers and Wand for the reconstruction of skeletons, which is then smoothly plugged into the study of an abstract machine following the distillation technique by Accattoli et al.

Cite as

Beniamino Accattoli, Francesco Magliocca, Loïc Peyrot, and Claudio Sacerdoti Coen. The Cost of Skeletal Call-By-Need, Smoothly. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{accattoli_et_al:LIPIcs.FSCD.2025.5,
  author =	{Accattoli, Beniamino and Magliocca, Francesco and Peyrot, Lo\"{i}c and Sacerdoti Coen, Claudio},
  title =	{{The Cost of Skeletal Call-By-Need, Smoothly}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{5:1--5:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.5},
  URN =		{urn:nbn:de:0030-drops-236206},
  doi =		{10.4230/LIPIcs.FSCD.2025.5},
  annote =	{Keywords: \lambda-calculus, abstract machines, call-by-need, cost models}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2025.7

Combining Generalization Algorithms in Regular Collapse-Free Theories

Authors: Mauricio Ayala-Rincón, David M. Cerna, Temur Kutsia, and Christophe Ringeissen

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract

We look at the generalization problem modulo some equational theories. This problem is dual to the unification problem: given two input terms, we want to find a common term whose respective two instances are equivalent to the original terms modulo the theory. There exist algorithms for finding generalizations over various equational theories. We focus on modular construction of equational generalization algorithms for the union of signature-disjoint theories. Specifically, we consider the class of regular and collapse-free theories, showing how to combine existing generalization algorithms to produce specific solutions in these cases. Additionally, we identify a class of theories that admit a generalization algorithm based on the application of axioms to resolve the problem. To define this class, we rely on the notion of syntactic theories, a concept originally introduced to develop unification procedures similar to the one known for syntactic unification. We demonstrate that syntactic theories are also helpful in developing generalization procedures similar to those used for syntactic generalization.

Cite as

Mauricio Ayala-Rincón, David M. Cerna, Temur Kutsia, and Christophe Ringeissen. Combining Generalization Algorithms in Regular Collapse-Free Theories. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ayalarincon_et_al:LIPIcs.FSCD.2025.7,
  author =	{Ayala-Rinc\'{o}n, Mauricio and Cerna, David M. and Kutsia, Temur and Ringeissen, Christophe},
  title =	{{Combining Generalization Algorithms in Regular Collapse-Free Theories}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{7:1--7:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.7},
  URN =		{urn:nbn:de:0030-drops-236228},
  doi =		{10.4230/LIPIcs.FSCD.2025.7},
  annote =	{Keywords: Generalization, Anti-unification, Equational theories, Combination}
}

Document

DOI: 10.4230/LIPIcs.CSL.2025.47

A Rewriting Theory for Quantum λ-Calculus

Authors: Claudia Faggian, Gaetan Lopez, and Benoît Valiron

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract

Quantum lambda calculus has been studied mainly as an idealized programming language - the evaluation essentially corresponds to a deterministic abstract machine. Very little work has been done to develop a rewriting theory for quantum lambda calculus. Recent advances in the theory of probabilistic rewriting give us a way to tackle this task with tools unavailable a decade ago. Our primary focus are standardization and normalization results.

Cite as

Claudia Faggian, Gaetan Lopez, and Benoît Valiron. A Rewriting Theory for Quantum λ-Calculus. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 47:1-47:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{faggian_et_al:LIPIcs.CSL.2025.47,
  author =	{Faggian, Claudia and Lopez, Gaetan and Valiron, Beno\^{i}t},
  title =	{{A Rewriting Theory for Quantum \lambda-Calculus}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{47:1--47:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.47},
  URN =		{urn:nbn:de:0030-drops-228046},
  doi =		{10.4230/LIPIcs.CSL.2025.47},
  annote =	{Keywords: quantum lambda-calculus, probabilistic rewriting, operational semantics, asymptotic normalization, principles of quantum programming languages}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.FSCD.2021.1

Duality in Action (Invited Talk)

Authors: Paul Downen and Zena M. Ariola

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

Abstract

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

Cite as

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

Copy BibTex To Clipboard

@InProceedings{downen_et_al:LIPIcs.FSCD.2021.1,
  author =	{Downen, Paul and Ariola, Zena M.},
  title =	{{Duality in Action}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{1:1--1:32},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.1},
  URN =		{urn:nbn:de:0030-drops-142390},
  doi =		{10.4230/LIPIcs.FSCD.2021.1},
  annote =	{Keywords: Duality, Logic, Curry-Howard, Sequent Calculus, Rewriting, Compilation}
}

Document

Complete Volume

DOI: 10.4230/LIPIcs.FSCD.2020

LIPIcs, Volume 167, FSCD 2020, Complete Volume

Authors: Zena M. Ariola

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract

LIPIcs, Volume 167, FSCD 2020, Complete Volume

Cite as

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

Copy BibTex To Clipboard

@Proceedings{ariola:LIPIcs.FSCD.2020,
  title =	{{LIPIcs, Volume 167, FSCD 2020, Complete Volume}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{1--732},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020},
  URN =		{urn:nbn:de:0030-drops-123219},
  doi =		{10.4230/LIPIcs.FSCD.2020},
  annote =	{Keywords: LIPIcs, Volume 167, FSCD 2020, Complete Volume}
}

Document

Front Matter

DOI: 10.4230/LIPIcs.FSCD.2020.0

Front Matter, Table of Contents, Preface, Conference Organization

Authors: Zena M. Ariola

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract

Front Matter, Table of Contents, Preface, Conference Organization

Cite as

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

Copy BibTex To Clipboard

@InProceedings{ariola:LIPIcs.FSCD.2020.0,
  author =	{Ariola, Zena M.},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{0:i--0:xx},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.0},
  URN =		{urn:nbn:de:0030-drops-123228},
  doi =		{10.4230/LIPIcs.FSCD.2020.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.FSCD.2020.1

Solvability in a Probabilistic Setting (Invited Talk)

Authors: Simona Ronchi Della Rocca, Ugo Dal Lago, and Claudia Faggian

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract

The notion of solvability, crucial in the λ-calculus, is conservatively extended to a probabilistic setting, and a complete characterization of it is given. The employed technical tool is a type assignment system, based on non-idempotent intersection types, whose typable terms turn out to be precisely the terms which are solvable with nonnull probability. We also supply an operational characterization of solvable terms, through the notion of head normal form, and a denotational model of Λ_⊕, itself induced by the type system, which equates all the unsolvable terms.

Cite as

Simona Ronchi Della Rocca, Ugo Dal Lago, and Claudia Faggian. Solvability in a Probabilistic Setting (Invited Talk). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 1:1-1:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{ronchidellarocca_et_al:LIPIcs.FSCD.2020.1,
  author =	{Ronchi Della Rocca, Simona and Dal Lago, Ugo and Faggian, Claudia},
  title =	{{Solvability in a Probabilistic Setting}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{1:1--1:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.1},
  URN =		{urn:nbn:de:0030-drops-123237},
  doi =		{10.4230/LIPIcs.FSCD.2020.1},
  annote =	{Keywords: Probabilistic Computation, Lambda Calculus, Solvability, Intersection Types}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.FSCD.2020.2

A Modal Analysis of Metaprogramming, Revisited (Invited Talk)

Authors: Brigitte Pientka

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract

Metaprogramming is the art of writing programs that produce or manipulate other programs. This opens the possibility to eliminate boilerplate code and exploit domain-specific knowledge to build high-performance programs. Unfortunately, designing language extensions to support type-safe multi-staged metaprogramming remains very challenging. In this talk, we outline a modal type-theoretic foundation for multi-staged metaprogramming which supports the generation and the analysis of polymorphic code. It has two main ingredients: first, we exploit contextual modal types to describe open code together with the context in which it is meaningful; second, we model code as a higher-order abstract syntax (HOAS) tree within a context. These two ideas provide the appropriate abstractions for both generating and pattern matching on open code without committing to a concrete representation of variable binding and contexts. Our work is a first step towards building a general type-theoretic foundation for multi-staged metaprogramming which on the one hand enforces strong type guarantees and on the other hand makes it easy to generate and manipulate code. This will allow us to exploit the full potential of metaprogramming without sacrificing reliability of and trust in the code we are producing and running.

Cite as

Brigitte Pientka. A Modal Analysis of Metaprogramming, Revisited (Invited Talk). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{pientka:LIPIcs.FSCD.2020.2,
  author =	{Pientka, Brigitte},
  title =	{{A Modal Analysis of Metaprogramming, Revisited}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{2:1--2:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.2},
  URN =		{urn:nbn:de:0030-drops-123242},
  doi =		{10.4230/LIPIcs.FSCD.2020.2},
  annote =	{Keywords: Type systems, Metaprogramming, Modal Type System}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.FSCD.2020.3

Quotients in Dependent Type Theory (Invited Talk)

Authors: Andrew M. Pitts

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract

Constructs that involve taking a quotient are commonplace in mathematics. Here I will consider how they are treated within dependent type theory. The notion of quotient type has its origins in the Nuprl theorem-proving system [R. L. Constable et al., 1986] for extensional type theory. Later Hofmann formulated a version for intensional type theory in his thesis [M. Hofmann, 1995]. This depends on having a pre-existing notion of intensional identity type. Hofmann used Martin-Löf’s notion, the indexed family inductively generated from proofs of reflexivity [B. Nordström et al., 1990]. The recent homotopical view of identity in terms of path types [The Univalent Foundations Program, 2013] gives a more liberal perspective and has brought with it the notion of higher inductive type (HIT) [P. L. Lumsdaine and M. Shulman, 2019], subsuming both inductive and quotient types. Inductively defined indexed families of types (in all their various forms) are perhaps the most useful concept that dependent type theory has contributed to the practice of computer assistance for formalizing mathematical proofs. However, it is often the case that a particular application of such types needs not only to inductively generate a collection of objects, but also to make identifications between the objects. In classical mathematics one can first generate and then identify, using the Axiom of Choice to lift infinitary constructions to the quotient. HITs can allow one to avoid such non-constructive uses of choice by inter-twining generation and identification. Perhaps more important than the constructive/non-constructive issue is that simultaneously declaring how to generate and how to identify can be a very natural way of defining some construct from the user’s point of view. This is why HITs promise to be so useful, once we have robust and convenient mechanisms in theorem-proving systems for defining HITs and defining functions out of HITs. Although some HITs have been axiomatized in various systems, at the moment the only system I know of with built in support for defining quite general forms of HIT and using them is the implementation of cubical type theory [C. Cohen et al., 2018] within recent versions of the Agda system [A. Vezzosi et al., 2019]. The higher dimensional aspect of identity in cubical type theory is fascinating; nevertheless, the simpler one-dimensional version of identity, in which one has uniqueness of identity proofs (UIP), is adequate for many applications. Although some regard UIP as a bug of early versions of Agda with it’s original form of dependent pattern matching [T. Coquand, 1992], it is by choice a feature of the Lean prover [J. Avigad et al., 2020]. Altenkirch and Kaposi [T. Altenkirch and A. Kaposi, 2016] have termed the one-dimensional version of HITs quotient inductive types (QITs) and they promise to be very useful even in the setting of type theory with UIP. In this talk I survey some of these developments, including a recent reduction of QITs to quotients [M. P. Fiore et al., 2020], and the prospects for better support in theorem-provers for quotient constructions.

Cite as

Andrew M. Pitts. Quotients in Dependent Type Theory (Invited Talk). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{pitts:LIPIcs.FSCD.2020.3,
  author =	{Pitts, Andrew M.},
  title =	{{Quotients in Dependent Type Theory}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{3:1--3:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.3},
  URN =		{urn:nbn:de:0030-drops-123256},
  doi =		{10.4230/LIPIcs.FSCD.2020.3},
  annote =	{Keywords: dependent type theory, quotient, quotient inductive type, theorem-proving systems}
}

50 Search Results for "Ariola, Zena M."

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