DROPS

Volume

LIPIcs, Volume 84

2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

FSCD 2017, September 3-9, 2017, Oxford, UK

Editors: Dale Miller

Document

Invited Talk

DOI: 10.4230/LIPIcs.CALCO.2023.3

A Tour on Ecumenical Systems (Invited Talk)

Authors: Elaine Pimentel and Luiz Carlos Pereira

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

Abstract

Ecumenism can be understood as a pursuit of unity, where diverse thoughts, ideas, or points of view coexist harmoniously. In logic, ecumenical systems refer, in a broad sense, to proof systems for combining logics. One captivating area of research over the past few decades has been the exploration of seamlessly merging classical and intuitionistic connectives, allowing them to coexist peacefully. In this paper, we will embark on a journey through ecumenical systems, drawing inspiration from Prawitz' seminal work [Dag Prawitz, 2015]. We will begin by elucidating Prawitz' concept of "ecumenism" and present a pure sequent calculus version of his system. Building upon this foundation, we will expand our discussion to incorporate alethic modalities, leveraging Simpson’s meta-logical characterization. This will enable us to propose several proof systems for ecumenical modal logics. We will conclude our tour with some discussion towards a term calculus proposal for the implicational propositional fragment of the ecumenical logic, the quest of automation using a framework based in rewriting logic, and an ecumenical view of proof-theoretic semantics.

Cite as

Elaine Pimentel and Luiz Carlos Pereira. A Tour on Ecumenical Systems (Invited Talk). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 3:1-3:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{pimentel_et_al:LIPIcs.CALCO.2023.3,
  author =	{Pimentel, Elaine and Pereira, Luiz Carlos},
  title =	{{A Tour on Ecumenical Systems}},
  booktitle =	{10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
  pages =	{3:1--3:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-287-7},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{270},
  editor =	{Baldan, Paolo and de Paiva, Valeria},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.3},
  URN =		{urn:nbn:de:0030-drops-188003},
  doi =		{10.4230/LIPIcs.CALCO.2023.3},
  annote =	{Keywords: Intuitionistic logic, classical logic, modal logic, ecumenical systems, proof theory}
}

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

Invited Talk

DOI: 10.4230/LIPIcs.CSL.2023.3

A Positive Perspective on Term Representation (Invited Talk)

Authors: Dale Miller and Jui-Hsuan Wu

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract

We use the focused proof system LJF as a framework for describing term structures and substitution. Since the proof theory of LJF does not pick a canonical polarization for primitive types, two different approaches to term representation arise. When primitive types are given the negative polarity, LJF proofs encode terms as tree-like structures in a familiar fashion. In this situation, cut elimination also yields the familiar notion of substitution. On the other hand, when primitive types are given the positive polarity, LJF proofs yield a structure in which explicit sharing of term structures is possible. Such a representation of terms provides an explicit method for sharing term structures. In this setting, cut elimination yields a different notion of substitution. We illustrate these two approaches to term representation by applying them to the encoding of untyped λ-terms. We also exploit concurrency theory techniques - namely traces and simulation - to compare untyped λ-terms using such different structuring disciplines.

Cite as

Dale Miller and Jui-Hsuan Wu. A Positive Perspective on Term Representation (Invited Talk). In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 3:1-3:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{miller_et_al:LIPIcs.CSL.2023.3,
  author =	{Miller, Dale and Wu, Jui-Hsuan},
  title =	{{A Positive Perspective on Term Representation}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{3:1--3:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.3},
  URN =		{urn:nbn:de:0030-drops-174648},
  doi =		{10.4230/LIPIcs.CSL.2023.3},
  annote =	{Keywords: term representation, sharing, focused proof systems}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2022.21

Linear Lambda-Calculus is Linear

Authors: Alejandro Díaz-Caro and Gilles Dowek

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract

We prove a linearity theorem for an extension of linear logic with addition and multiplication by a scalar: the proofs of some propositions in this logic are linear in the algebraic sense. This work is part of a wider research program that aims at defining a logic whose proof language is a quantum programming language.

Cite as

Alejandro Díaz-Caro and Gilles Dowek. Linear Lambda-Calculus is Linear. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 21:1-21:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{diazcaro_et_al:LIPIcs.FSCD.2022.21,
  author =	{D{\'\i}az-Caro, Alejandro and Dowek, Gilles},
  title =	{{Linear Lambda-Calculus is Linear}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{21:1--21:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.21},
  URN =		{urn:nbn:de:0030-drops-163024},
  doi =		{10.4230/LIPIcs.FSCD.2022.21},
  annote =	{Keywords: Proof theory, Lambda calculus, Linear logic, Quantum computing}
}

Document

DOI: 10.4230/LIPIcs.TYPES.2020.10

Two Applications of Logic Programming to Coq

Authors: Matteo Manighetti, Dale Miller, and Alberto Momigliano

Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)

Abstract

The logic programming paradigm provides a flexible setting for representing, manipulating, checking, and elaborating proof structures. This is particularly true when the logic programming language allows for bindings in terms and proofs. In this paper, we make use of two recent innovations at the intersection of logic programming and proof checking. One of these is the foundational proof certificate (FPC) framework which provides a flexible means of defining the semantics of a range of proof structures for classical and intuitionistic logic. A second innovation is the recently released Coq-Elpi plugin for Coq in which the Elpi implementation of λProlog can send and retrieve information to and from the Coq kernel. We illustrate the use of both this Coq plugin and FPCs with two example applications. First, we implement an FPC-driven sequent calculus for a fragment of the Calculus of Inductive Constructions and we package it into a tactic to perform property-based testing of inductive types corresponding to Horn clauses. Second, we implement in Elpi a proof checker for first-order intuitionistic logic and demonstrate how proof certificates can be supplied by external (to Coq) provers and then elaborated into the fully detailed proof terms that can be checked by the Coq kernel.

Cite as

Matteo Manighetti, Dale Miller, and Alberto Momigliano. Two Applications of Logic Programming to Coq. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 10:1-10:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{manighetti_et_al:LIPIcs.TYPES.2020.10,
  author =	{Manighetti, Matteo and Miller, Dale and Momigliano, Alberto},
  title =	{{Two Applications of Logic Programming to Coq}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{10:1--10:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-182-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{188},
  editor =	{de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.10},
  URN =		{urn:nbn:de:0030-drops-138896},
  doi =		{10.4230/LIPIcs.TYPES.2020.10},
  annote =	{Keywords: Proof assistants, logic programming, Coq, \lambdaProlog, property-based testing}
}

Document

Invited Paper

DOI: 10.4230/LIPIcs.TYPES.2016.1

Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper)

Authors: Dale Miller

Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)

Abstract

Proof assistants and the programming languages that implement them need to deal with a range of linguistic expressions that involve bindings. Since most mature proof assistants do not have built-in methods to treat this aspect of syntax, many of them have been extended with various packages and libraries that allow them to encode bindings using, for example, de Bruijn numerals and nominal logic features. I put forward the argument that bindings are such an intimate aspect of the structure of expressions that they should be accounted for directly in the underlying programming language support for proof assistants and not added later using packages and libraries. One possible approach to designing programming languages and proof assistants that directly supports such an approach to bindings in syntax is presented. The roots of such an approach can be found in the mobility of binders between term-level bindings, formula-level bindings (quantifiers), and proof-level bindings (eigenvariables). In particular, by combining Church's approach to terms and formulas (found in his Simple Theory of Types) and Gentzen's approach to sequent calculus proofs, we can learn how bindings can declaratively interact with the full range of logical connectives and quantifiers. I will also illustrate how that framework provides an intimate and semantically clean treatment of computation and reasoning with syntax containing bindings. Some implemented systems, which support this intimate and built-in treatment of bindings, will be briefly described.

Cite as

Dale Miller. Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper). In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 1:1-1:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{miller:LIPIcs.TYPES.2016.1,
  author =	{Miller, Dale},
  title =	{{Mechanized Metatheory Revisited: An Extended Abstract}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{1:1--1:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.1},
  URN =		{urn:nbn:de:0030-drops-98603},
  doi =		{10.4230/LIPIcs.TYPES.2016.1},
  annote =	{Keywords: mechanized metatheory, mobility of binders, lambda-tree syntax, higher-order abstract syntax}
}

Document

Complete Volume

DOI: 10.4230/LIPIcs.FSCD.2017

LIPIcs, Volume 84, FSCD'17, Complete Volume

Authors: Dale Miller

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract

LIPIcs, Volume 84, FSCD'17, Complete Volume

Cite as

Dale Miller. LIPIcs, Volume 84, FSCD'17, Complete Volume. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Proceedings{miller:LIPIcs.FSCD.2017,
  title =	{{LIPIcs, Volume 84, FSCD'17, Complete Volume}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017},
  URN =		{urn:nbn:de:0030-drops-79063},
  doi =		{10.4230/LIPIcs.FSCD.2017},
  annote =	{Keywords: Theory of Computation, Computation by Abstract Devices, Analysis of Algorithms and Problem Complexity, Logics and Meanings of Programs, Mathematical Logic and Formal Languages, Programming Techniques, Software/Program Verification, Programming Languages, Deduction and Theorem Proving}
}

Document

Front Matter

DOI: 10.4230/LIPIcs.FSCD.2017.0

Front Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers

Authors: Dale Miller

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract

Front Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers

Cite as

Dale Miller. Front Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 0:i-0:xiv, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{miller:LIPIcs.FSCD.2017.0,
  author =	{Miller, Dale},
  title =	{{Front Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{0:i--0:xiv},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.0},
  URN =		{urn:nbn:de:0030-drops-77126},
  doi =		{10.4230/LIPIcs.FSCD.2017.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.FSCD.2017.1

Type Systems for the Relational Verification of Higher Order Programs (Invited Talk)

Authors: Marco Gaboardi

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract

Relational program verification is a variant of program verification where one focuses on guaranteeing properties about the executions of two programs, and as a special case about two executions of a single program on different inputs. Relational verification becomes particularly interesting when non-functional aspects of a computation, like probabilities or resource cost, are considered. Several approached to relational program verification have been developed, from relational program logics to relational abstract interpretation. In this talk, I will introduce two approaches to relational program verification for higher-order computations based on the use of type systems. The first approach consists in developing powerful type system where a rich language of assertions can be used to express complex relations between two programs. The second approach consists in developing more restrictive type systems enriched with effects expressing in a lightweight way relations between different runs of the same program. I will discuss the pros and cons of these two approaches on a concrete example: relational cost analysis, which aims at giving a bound on the difference in cost of running two programs, and as a special case the difference in cost of two executions of a single program on different inputs.

Cite as

Marco Gaboardi. Type Systems for the Relational Verification of Higher Order Programs (Invited Talk). In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, p. 1:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{gaboardi:LIPIcs.FSCD.2017.1,
  author =	{Gaboardi, Marco},
  title =	{{Type Systems for the Relational Verification of Higher Order Programs}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{1:1--1:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.1},
  URN =		{urn:nbn:de:0030-drops-77429},
  doi =		{10.4230/LIPIcs.FSCD.2017.1},
  annote =	{Keywords: Relational verification, refinement types, type and effect systems, complexity analysis}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.FSCD.2017.2

Uniform Resource Analysis by Rewriting: Strenghts and Weaknesses (Invited Talk)

Authors: Georg Moser

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract

In this talk, I'll describe how rewriting techniques can be successfully employed to built state-of-the-art automated resource analysis tools which favourably compare to other approaches. Furthermore I'll sketch the genesis of a uniform framework for resource analysis, emphasising success stories, without hiding intricate weaknesses. The talk ends with the discussion of open problems.

Cite as

Georg Moser. Uniform Resource Analysis by Rewriting: Strenghts and Weaknesses (Invited Talk). In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 2:1-2:10, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{moser:LIPIcs.FSCD.2017.2,
  author =	{Moser, Georg},
  title =	{{Uniform Resource Analysis by Rewriting: Strenghts and Weaknesses}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{2:1--2:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.2},
  URN =		{urn:nbn:de:0030-drops-77438},
  doi =		{10.4230/LIPIcs.FSCD.2017.2},
  annote =	{Keywords: resource analysis, term rewriting, automation}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.FSCD.2017.3

Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages (Invited Talk)

Authors: Alexandra Silva

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract

Concurrent Kleene Algebra (CKA) is a mathematical formalism to study programs that exhibit concurrent behaviour. As with previous extensions of Kleene Algebra, characterizing the free model is crucial in order to develop the foundations of the theory and potential applications. For CKA, this has been an open question for a few years and this talk will overview why the problem is so difficult. We will then pave the way towards a solution, by presenting a new automaton model and a Kleene-like theorem for CKA. More precisely, we connect a relaxed version of CKA to series-parallel pomset languages, which are a natural candidate for the free model. There are two substantial differences with previous work: from expressions to automata, we use Brzozowski derivatives, which enable a direct construction of the automaton; from automata to expressions, we provide a syntactic characterization of the automata that denote valid CKA behaviours. We also survey how the present work can be used to to extend the network specification language NetKAT with primitives for concurrency so as to model and reason about concurrency within networks. This is joint work with Tobias Kappe, Paul Brunet, Bas Luttik, and Fabio Zanasi.

Cite as

Alexandra Silva. Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages (Invited Talk). In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, p. 3:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{silva:LIPIcs.FSCD.2017.3,
  author =	{Silva, Alexandra},
  title =	{{Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{3:1--3:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.3},
  URN =		{urn:nbn:de:0030-drops-77445},
  doi =		{10.4230/LIPIcs.FSCD.2017.3},
  annote =	{Keywords: Kleene algebras, Pomset languages, concurrency, NetKAT}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.FSCD.2017.4

Quantitative Semantics for Probabilistic Programming (Invited Talk)

Authors: Christine Tasson

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract

Probabilistic programming has many applications in statistics, physics, ... so that all programming languages have been equipped with probabilistic library. However, there is a need in developing semantical tools in order to formalize higher order and recursive probabilistic languages. Indeed, it is well known that categories of measurable spaces are not Cartesian closed. We have been studying quantitative semantics of probabilistic spaces to fill this gap. A first step has been to focus on probabilistic programming languages with discrete types such as integers and booleans. In this setting, probabilistic programs can be seen as linear combinations of deterministic programs. Probabilistic Coherent Spaces constitute a Cartesian closed category that is fully abstract with respect to probabilistic Call-By-Push-Value. Moreover, this toy language is endowed with a memorization operator that allow to encode most discrete probabilistic programs. The second step is to move on probabilistic programming with continuous types representing for instance reals endowed with Lebesgue measurable sets. We introduce the category of cones and stable functions which is Cartesian closed. The trick is to enlarge the category of measurable spaces to gain closeness and to embrace measurable spaces. Besides, the category of cones is a sound and adequate model of a higher order and recursive probabilistic language in which most classical distributions and probabilistic tools can be encoded. This is joint work with Thomas Ehrhard and Michele Pagani.

Cite as

Christine Tasson. Quantitative Semantics for Probabilistic Programming (Invited Talk). In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, p. 4:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{tasson:LIPIcs.FSCD.2017.4,
  author =	{Tasson, Christine},
  title =	{{Quantitative Semantics for Probabilistic Programming}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{4:1--4:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.4},
  URN =		{urn:nbn:de:0030-drops-77456},
  doi =		{10.4230/LIPIcs.FSCD.2017.4},
  annote =	{Keywords: denotational semantics, probabilistic programming, programming language, probability}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2017.5

Displayed Categories

Authors: Benedikt Ahrens and Peter LeFanu Lumsdaine

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract

We introduce and develop the notion of displayed categories. A displayed category over a category C is equivalent to "a category D and functor F : D -> C", but instead of having a single collection of "objects of D" with a map to the objects of C, the objects are given as a family indexed by objects of C, and similarly for the morphisms. This encapsulates a common way of building categories in practice, by starting with an existing category and adding extra data/properties to the objects and morphisms. The interest of this seemingly trivial reformulation is that various properties of functors are more naturally defined as properties of the corresponding displayed categories. Grothendieck fibrations, for example, when defined as certain functors, use equality on objects in their definition. When defined instead as certain displayed categories, no reference to equality on objects is required. Moreover, almost all examples of fibrations in nature are, in fact, categories whose standard construction can be seen as going via displayed categories. We therefore propose displayed categories as a basis for the development of fibrations in the type-theoretic setting, and similarly for various other notions whose classical definitions involve equality on objects. Besides giving a conceptual clarification of such issues, displayed categories also provide a powerful tool in computer formalisation, unifying and abstracting common constructions and proof techniques of category theory, and enabling modular reasoning about categories of multi-component structures. As such, most of the material of this article has been formalised in Coq over the UniMath library, with the aim of providing a practical library for use in further developments.

Cite as

Benedikt Ahrens and Peter LeFanu Lumsdaine. Displayed Categories. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 5:1-5:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{ahrens_et_al:LIPIcs.FSCD.2017.5,
  author =	{Ahrens, Benedikt and Lumsdaine, Peter LeFanu},
  title =	{{Displayed Categories}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{5:1--5:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.5},
  URN =		{urn:nbn:de:0030-drops-77220},
  doi =		{10.4230/LIPIcs.FSCD.2017.5},
  annote =	{Keywords: Category theory, Dependent type theory, Computer proof assistants, Coq, Univalent mathematics}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2017.6

The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type

Authors: Yohji Akama

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract

For the lambda-calculus with surjective pairing and terminal type, Curien and Di Cosmo, inspired by Knuth-Bendix completion, introduced a confluent rewriting system of the naive rewriting system. Their system is a confluent (CR) rewriting system stable under contexts. They left the strong normalization (SN) of their rewriting system open. By Girard's reducibility method with restricting reducibility theorem, we prove SN of their rewriting, and SN of the extensions by polymorphism and (terminal types caused by parametric polymorphism). We extend their system by sum types and eta-like reductions, and prove the SN. We compare their system to type-directed expansions.

Cite as

Yohji Akama. The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 6:1-6:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{akama:LIPIcs.FSCD.2017.6,
  author =	{Akama, Yohji},
  title =	{{The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{6:1--6:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.6},
  URN =		{urn:nbn:de:0030-drops-77346},
  doi =		{10.4230/LIPIcs.FSCD.2017.6},
  annote =	{Keywords: reducibility method, restricted reducibility theorem, sum type, typedirected expansion, strong normalization}
}

46 Search Results for "Miller, Dale"

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