LIPIcs, Volume 52

1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)



Thumbnail PDF

Event

FSCD 2016, June 22-26, 2016, Porto, Portugal

Editors

Delia Kesner
Brigitte Pientka

Publication Details

  • published at: 2016-06-17
  • Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
  • ISBN: 978-3-95977-010-1
  • DBLP: db/conf/rta/fscd2016

Access Numbers

Documents

No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 52, FSCD'16, Complete Volume

Authors: Delia Kesner and Brigitte Pientka


Abstract
LIPIcs, Volume 52, FSCD'16, Complete Volume

Cite as

1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@Proceedings{kesner_et_al:LIPIcs.FSCD.2016,
  title =	{{LIPIcs, Volume 52, FSCD'16, Complete Volume}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016},
  URN =		{urn:nbn:de:0030-drops-60595},
  doi =		{10.4230/LIPIcs.FSCD.2016},
  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
Front Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers, Organising Commitee

Authors: Delia Kesner and Brigitte Pientka


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

Cite as

1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{kesner_et_al:LIPIcs.FSCD.2016.0,
  author =	{Kesner, Delia and Pientka, Brigitte},
  title =	{{Front Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers, Organising Commitee}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{0:i--0:xviii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.0},
  URN =		{urn:nbn:de:0030-drops-59672},
  doi =		{10.4230/LIPIcs.FSCD.2016.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers, Organising Commitee}
}
Document
Compositional Compiler Verification for a Multi-Language World

Authors: Amal Ahmed


Abstract
Verified compilers are typically proved correct under severe restrictions on what the compiler's output may be linked with, from no linking at all to linking only with code compiled from the same source language. Such assumptions contradict the reality of how we use these compilers since most software systems today are comprised of components written in different languages compiled by different compilers to a common target, as well as low-level libraries that may be handwritten in the target language. The key challenge in verifying compilers for today's world of multi-language software is how to formally state a compiler correctness theorem that is compositional along two dimensions. First, the theorem must guarantee correct compilation of components while allowing compiled code to be composed (linked) with target-language components of arbitrary provenance, including those compiled from other languages. Second, the theorem must support verification of multi-pass compilers by composing correctness proofs for individual passes. In this talk, I will describe a methodology for verifying compositional compiler correctness for a higher-order typed language and discuss the challenges that lie ahead. I will argue that compositional compiler correctness is, in essence, a language interoperability problem: for viable solutions in the long term, high-level languages must be equipped with principled foreign-function interfaces that specify safe interoperability between high-level and low-level components, and between more precisely and less precisely typed code.

Cite as

Amal Ahmed. Compositional Compiler Verification for a Multi-Language World. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{ahmed:LIPIcs.FSCD.2016.1,
  author =	{Ahmed, Amal},
  title =	{{Compositional Compiler Verification for a Multi-Language World}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{1:1--1:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.1},
  URN =		{urn:nbn:de:0030-drops-59680},
  doi =		{10.4230/LIPIcs.FSCD.2016.1},
  annote =	{Keywords: verified compilation; compositional compiler correctness, multi-language semantics, typed low-level languages}
}
Document
Coalgebras and Higher-Order Computation: a GoI Approach

Authors: Ichiro Hasuo


Abstract
Girard's geometry of interaction (GoI) can be seen---in one practical aspect of it---as a compositional compilation method from functional programs to sequential machines. There tokens move around and express interactions between (parts of) programs. Intrigued by the combination of abstract structures and concrete dynamics in GoI, our line of work has aimed at exploiting, in GoI, results from the theory of coalgebra---a categorical abstraction of state-based transition systems that has found its use principally in concurrency theory. Such reinforced connection between higher-order computation and state-based dynamics is made possible thanks to an elegant categorical axiomatization of GoI by Abramsky, Haghverdi and Scott, where traced monoidal categories are identified to be the essential structure behind. In the talk I shall lay out these basic ideas, together with some of our results on: GoI semantics for a quantum programming language; and our ``memoryful'' extension of GoI with algebraic effects. The talk is based on my joint work with my colleague Naohiko Hoshino (RIMS, Kyoto Univer- sity) and my (former) students Koko Muroya (University of Birmingham) and Toshiki Kataoka (University of Tokyo), to whom I owe special thanks.

Cite as

Ichiro Hasuo. Coalgebras and Higher-Order Computation: a GoI Approach. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{hasuo:LIPIcs.FSCD.2016.2,
  author =	{Hasuo, Ichiro},
  title =	{{Coalgebras and Higher-Order Computation: a GoI Approach}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{2:1--2:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.2},
  URN =		{urn:nbn:de:0030-drops-59698},
  doi =		{10.4230/LIPIcs.FSCD.2016.2},
  annote =	{Keywords: functional programming, geometry of interaction, categorical semantics, coalgebra}
}
Document
Teaching Foundations of Computation and Deduction Through Literate Functional Programming and Type Theory Formalization

Authors: Gérard Huet


Abstract
We describe experiments in teaching fundamental informatics notions around mathematical structures for formal concepts, and effective algorithms to manipulate them. The major themes of lambda-calculus and type theory served as guides for the effective implementation of functional programming languages and higher-order proof assistants, appropriate for reflecting the theoretical material into effective tools to represent constructively the concepts and formally certify the proofs of their properties. Progressively, a literate programming and proving style replaced informal mathematics in the presentation of the material as executable course notes. The talk will evoke the various stages of (in)completion of the corresponding set of notes along the years, and tell how their elaboration proved to be essential to the discovery of fundamental results.

Cite as

Gérard Huet. Teaching Foundations of Computation and Deduction Through Literate Functional Programming and Type Theory Formalization. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{huet:LIPIcs.FSCD.2016.3,
  author =	{Huet, G\'{e}rard},
  title =	{{Teaching Foundations of Computation and Deduction Through Literate Functional Programming and Type Theory Formalization}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{3:1--3:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.3},
  URN =		{urn:nbn:de:0030-drops-60020},
  doi =		{10.4230/LIPIcs.FSCD.2016.3},
  annote =	{Keywords: Foundations, Computation, Deduction, Programming, Proofs}
}
Document
Verified Analysis of Functional Data Structures

Authors: Tobias Nipkow


Abstract
In recent work the author has analyzed a number of classical functional search tree and priority queue implementations with the help of the theorem prover Isabelle/HOL. The functional correctness proofs of AVL trees, red-black trees, 2-3 trees, 2-3-4 trees, 1-2 brother trees, AA trees and splay trees could be automated. The amortized logarithmic complexity of skew heaps, splay trees, splay heaps and pairing heaps had to be proved manually.

Cite as

Tobias Nipkow. Verified Analysis of Functional Data Structures. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{nipkow:LIPIcs.FSCD.2016.4,
  author =	{Nipkow, Tobias},
  title =	{{Verified Analysis of Functional Data Structures}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{4:1--4:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.4},
  URN =		{urn:nbn:de:0030-drops-59701},
  doi =		{10.4230/LIPIcs.FSCD.2016.4},
  annote =	{Keywords: Program Verification, Algorithm Analysis, Functional Programming}
}
Document
Strong Normalization for the Parameter-Free Polymorphic Lambda Calculus Based on the Omega-Rule.

Authors: Ryota Akiyoshi and Kazushige Terui


Abstract
Following Aehlig, we consider a hierarchy F^p= { F^p_n }_{n in Nat} of parameter-free subsystems of System F, where each F^p_n corresponds to ID_n, the theory of n-times iterated inductive definitions (thus our F^p_n corresponds to the n+1th system of Aehlig). We here present two proofs of strong normalization for F^p_n, which are directly formalizable with inductive definitions. The first one, based on the Joachimski-Matthes method, can be fully formalized in ID_n+1. This provides a tight upper bound on the complexity of the normalization theorem for System F^p_n. The second one, based on the Godel-Tait method, can be locally formalized in ID_n. This provides a direct proof to the known result that the representable functions in F^p_n are provably total in ID_n. In both cases, Buchholz' Omega-rule plays a central role.

Cite as

Ryota Akiyoshi and Kazushige Terui. Strong Normalization for the Parameter-Free Polymorphic Lambda Calculus Based on the Omega-Rule.. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 5:1-5:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{akiyoshi_et_al:LIPIcs.FSCD.2016.5,
  author =	{Akiyoshi, Ryota and Terui, Kazushige},
  title =	{{Strong Normalization for the Parameter-Free Polymorphic Lambda Calculus Based on the Omega-Rule.}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{5:1--5:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.5},
  URN =		{urn:nbn:de:0030-drops-59718},
  doi =		{10.4230/LIPIcs.FSCD.2016.5},
  annote =	{Keywords: Polymorphic Lambda Calculus, Strong Normalization, Computability Predicate, Infinitary Proof Theory}
}
Document
Normalisation by Evaluation for Dependent Types

Authors: Thorsten Altenkirch and Ambrus Kaposi


Abstract
We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated using internal type theory using quotient inductive types. We use a typed presentation hence there are no preterms or realizers in our construction. NBE for simple types is using a logical relation between the syntax and the presheaf interpretation. In our construction, we merge the presheaf interpretation and the logical relation into a proof-relevant logical predicate. We have formalized parts of the construction in Agda.

Cite as

Thorsten Altenkirch and Ambrus Kaposi. Normalisation by Evaluation for Dependent Types. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{altenkirch_et_al:LIPIcs.FSCD.2016.6,
  author =	{Altenkirch, Thorsten and Kaposi, Ambrus},
  title =	{{Normalisation by Evaluation for Dependent Types}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{6:1--6:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.6},
  URN =		{urn:nbn:de:0030-drops-59727},
  doi =		{10.4230/LIPIcs.FSCD.2016.6},
  annote =	{Keywords: normalisation by evaluation, dependent types, internal type theory, logical relations, Agda}
}
Document
Minimal Paradefinite Logics for Reasoning with Incompleteness and Inconsistency

Authors: Ofer Arieli and Arnon Avron


Abstract
Paradefinite (`beyond the definite') logics are logics that can be used for handling contradictory or partial information. As such, paradefinite logics should be both paraconsistent and paracomplete. In this paper we consider the simplest semantic framework for defining paradefinite logics, consisting of four-valued matrices, and study the better accepted logics that are induced by these matrices.

Cite as

Ofer Arieli and Arnon Avron. Minimal Paradefinite Logics for Reasoning with Incompleteness and Inconsistency. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{arieli_et_al:LIPIcs.FSCD.2016.7,
  author =	{Arieli, Ofer and Avron, Arnon},
  title =	{{Minimal Paradefinite Logics for Reasoning with Incompleteness and Inconsistency}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{7:1--7:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.7},
  URN =		{urn:nbn:de:0030-drops-59731},
  doi =		{10.4230/LIPIcs.FSCD.2016.7},
  annote =	{Keywords: Paraconsistecy, Paracompleteness, 4-valued logics}
}
Document
Structural Interactions and Absorption of Structural Rules in BI Sequent Calculus

Authors: Ryuta Arisaka


Abstract
Development of a contraction-free BI sequent calculus, be the contraction-freeness implicit or explicit, has not been successful in the literature. We address this problem by presenting such a sequent system. Our calculus involves no structural rules. It should be an insight into non-formula contraction absorption in other non-classical logics. Contraction absorption in sequent calculus is associated to simpler cut elimination and to efficient proof searches.

Cite as

Ryuta Arisaka. Structural Interactions and Absorption of Structural Rules in BI Sequent Calculus. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{arisaka:LIPIcs.FSCD.2016.8,
  author =	{Arisaka, Ryuta},
  title =	{{Structural Interactions and Absorption of Structural Rules in BI Sequent Calculus}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.8},
  URN =		{urn:nbn:de:0030-drops-59742},
  doi =		{10.4230/LIPIcs.FSCD.2016.8},
  annote =	{Keywords: cut-elimination, contraction-free, sequent calculus, proof theory, BI, logic combination}
}
Document
Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation

Authors: Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk


Abstract
We present sound and complete environmental bisimilarities for a variant of Dybvig et al.'s calculus of multi-prompted delimited-control operators with dynamic prompt generation. The reasoning principles that we obtain generalize and advance the existing techniques for establishing program equivalence in calculi with single-prompted delimited control. The basic theory that we develop is presented using Madiot et al.'s framework that allows for smooth integration and composition of up-to techniques facilitating bisimulation proofs. We also generalize the framework in order to express environmental bisimulations that support equivalence proofs of evaluation contexts representing continuations. This change leads to a novel and powerful up-to technique enhancing bisimulation proofs in the presence of control operators.

Cite as

Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{aristizabal_et_al:LIPIcs.FSCD.2016.9,
  author =	{Aristiz\'{a}bal, Andr\'{e}s and Biernacki, Dariusz and Lenglet, Sergue\"{i} and Polesiuk, Piotr},
  title =	{{Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{9:1--9:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.9},
  URN =		{urn:nbn:de:0030-drops-59756},
  doi =		{10.4230/LIPIcs.FSCD.2016.9},
  annote =	{Keywords: delimited continuation, dynamic prompt generation, contextual equivalence, environmental bisimulation, up-to technique}
}
Document
Complexity of Acyclic Term Graph Rewriting

Authors: Martin Avanzini and Georg Moser


Abstract
Term rewriting has been used as a formal model to reason about the complexity of logic, functional, and imperative programs. In contrast to term rewriting, term graph rewriting permits sharing of common sub-expressions, and consequently is able to capture more closely reasonable implementations of rule based languages. However, the automated complexity analysis of term graph rewriting has received little to no attention. With this work, we provide first steps towards overcoming this situation. We present adaptions of two prominent complexity techniques from term rewriting, viz, the interpretation method and dependency tuples. Our adaptions are non-trivial, in the sense that they can observe not only term but also graph structures, i.e. take sharing into account. In turn, the developed methods allow us to more precisely estimate the runtime complexity of programs where sharing of sub-expressions is essential.

Cite as

Martin Avanzini and Georg Moser. Complexity of Acyclic Term Graph Rewriting. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{avanzini_et_al:LIPIcs.FSCD.2016.10,
  author =	{Avanzini, Martin and Moser, Georg},
  title =	{{Complexity of Acyclic Term Graph Rewriting}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{10:1--10:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.10},
  URN =		{urn:nbn:de:0030-drops-59901},
  doi =		{10.4230/LIPIcs.FSCD.2016.10},
  annote =	{Keywords: Program Analysis, Graph Rewriting, Complexity Analysis}
}
Document
Nominal Narrowing

Authors: Mauricio Ayala-Rincón, Maribel Fernández, and Daniele Nantes-Sobrinho


Abstract
Nominal unification is a generalisation of first-order unification that takes alpha-equivalence into account. In this paper, we study nominal unification in the context of equational theories. We introduce nominal narrowing and design a general nominal E-unification procedure, which is sound and complete for a wide class of equational theories. We give examples of application.

Cite as

Mauricio Ayala-Rincón, Maribel Fernández, and Daniele Nantes-Sobrinho. Nominal Narrowing. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 11:1-11:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{ayalarincon_et_al:LIPIcs.FSCD.2016.11,
  author =	{Ayala-Rinc\'{o}n, Mauricio and Fern\'{a}ndez, Maribel and Nantes-Sobrinho, Daniele},
  title =	{{Nominal Narrowing}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{11:1--11:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.11},
  URN =		{urn:nbn:de:0030-drops-59832},
  doi =		{10.4230/LIPIcs.FSCD.2016.11},
  annote =	{Keywords: Nominal Rewriting, Nominal Unification, Matching, Narrowing, Equational Theories}
}
Document
Synthesis of Functional Programs with Help of First-Order Intuitionistic Logic

Authors: Marcin Benke, Aleksy Schubert, and Daria Walukiewicz-Chrzaszcz


Abstract
Curry-Howard isomorphism makes it possible to obtain functional programs from proofs in logic. We analyse the problem of program synthesis for ML programs with algebraic types and relate it to the proof search problems in appropriate logics. The problem of synthesis for closed programs is easily equivalent to the proof construction in intuitionistic propositional logic and thus fits in the class of PSPACE-complete problems. We focus further attention on the synthesis problem relative to a given external library of functions. It turns out that the problem is undecidable for unbounded instantiation in ML. However its restriction to instantiations with atomic types only results in a case equivalent to proof search in a restricted fragment of intuitionistic first-order logic, being the core of Sigma_1 level of the logic in the Mints hierarchy. This results in EXPSPACE-completeness for this special case of the ML program synthesis problem.

Cite as

Marcin Benke, Aleksy Schubert, and Daria Walukiewicz-Chrzaszcz. Synthesis of Functional Programs with Help of First-Order Intuitionistic Logic. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{benke_et_al:LIPIcs.FSCD.2016.12,
  author =	{Benke, Marcin and Schubert, Aleksy and Walukiewicz-Chrzaszcz, Daria},
  title =	{{Synthesis of Functional Programs with Help of First-Order Intuitionistic Logic}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{12:1--12:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.12},
  URN =		{urn:nbn:de:0030-drops-59765},
  doi =		{10.4230/LIPIcs.FSCD.2016.12},
  annote =	{Keywords: ML, program synthesis}
}
Document
Classical Extraction in Continuation Models

Authors: Valentin Blot


Abstract
We use the control features of continuation models to interpret proofs in first-order classical theories. This interpretation is suitable for extracting algorithms from proofs of Pi^0_2 formulas. It is fundamentally different from the usual direct interpretation, which is shown to be equivalent to Friedman's trick. The main difference is that atomic formulas and natural numbers are interpreted as distinct objects. Nevertheless, the control features inherent to the continuation models permit extraction using a special "channel" on which the extracted value is transmitted at toplevel without unfolding the recursive calls. We prove that the technique fails in Scott domains, but succeeds in the refined setting of Laird's bistable bicpos, as well as in game semantics.

Cite as

Valentin Blot. Classical Extraction in Continuation Models. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{blot:LIPIcs.FSCD.2016.13,
  author =	{Blot, Valentin},
  title =	{{Classical Extraction in Continuation Models}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{13:1--13:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.13},
  URN =		{urn:nbn:de:0030-drops-59913},
  doi =		{10.4230/LIPIcs.FSCD.2016.13},
  annote =	{Keywords: Extraction, Classical Logic, Control Operators, Game Semantics}
}
Document
Proving Correctness of Logically Decorated Graph Rewriting Systems

Authors: Jon Haël Brenas, Rachid Echahed, and Martin Strecker


Abstract
We first introduce the notion of logically decorated rewriting systems where the left-hand sides are endowed with logical formulas which help to express positive as well as negative application conditions, in addition to classical pattern-matching. These systems are defined using graph structures and an extension of combinatory propositional dynamic logic, CPDL, with restricted universal programs, called C2PDL. In a second step, we tackle the problem of proving the correctness of logically decorated graph rewriting systems by using a Hoare-like calculus. We introduce a notion of specification defined as a tuple (Pre, Post, R, S) with Pre and Post being formulas of C2PDL, R a rewriting system and S a rewriting strategy. We provide a sound calculus which infers proof obligations of the considered specifications and establish the decidability of the verification problem of the (partial) correctness of the considered specifications.

Cite as

Jon Haël Brenas, Rachid Echahed, and Martin Strecker. Proving Correctness of Logically Decorated Graph Rewriting Systems. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 14:1-14:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{brenas_et_al:LIPIcs.FSCD.2016.14,
  author =	{Brenas, Jon Ha\"{e}l and Echahed, Rachid and Strecker, Martin},
  title =	{{Proving Correctness of Logically Decorated Graph Rewriting Systems}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{14:1--14:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.14},
  URN =		{urn:nbn:de:0030-drops-59778},
  doi =		{10.4230/LIPIcs.FSCD.2016.14},
  annote =	{Keywords: Graph Rewriting, Hoare Logic,Combinatory PDL, Rewrite Strategies, Program Verification}
}
Document
New Results on Morris's Observational Theory: The Benefits of Separating the Inseparable

Authors: Flavien Breuvart, Giulio Manzonetto, Andrew Polonsky, and Domenico Ruoppolo


Abstract
Working in the untyped lambda calculus, we study Morris's lambda-theory H+. Introduced in 1968, this is the original extensional theory of contextual equivalence. On the syntactic side, we show that this lambda-theory validates the omega-rule, thus settling a long-standing open problem.On the semantic side, we provide sufficient and necessary conditions for relational graph models to be fully abstract for H+. We show that a relational graph model captures Morris's observational preorder exactly when it is extensional and lambda-Konig. Intuitively, a model is lambda-Konig when every lambda-definable tree has an infinite path which is witnessed by some element of the model. Both results follow from a weak separability property enjoyed by terms differing only because of some infinite eta-expansion, which is proved through a refined version of the Böhm-out technique.

Cite as

Flavien Breuvart, Giulio Manzonetto, Andrew Polonsky, and Domenico Ruoppolo. New Results on Morris's Observational Theory: The Benefits of Separating the Inseparable. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{breuvart_et_al:LIPIcs.FSCD.2016.15,
  author =	{Breuvart, Flavien and Manzonetto, Giulio and Polonsky, Andrew and Ruoppolo, Domenico},
  title =	{{New Results on Morris's Observational Theory: The Benefits of Separating the Inseparable}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{15:1--15:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.15},
  URN =		{urn:nbn:de:0030-drops-59924},
  doi =		{10.4230/LIPIcs.FSCD.2016.15},
  annote =	{Keywords: Lambda calculus, relational models, fully abstract, B\"{o}hm-out, omega-rule}
}
Document
Modular Focused Proof Systems for Intuitionistic Modal Logics

Authors: Kaustuv Chaudhuri, Sonia Marin, and Lutz Straßburger


Abstract
Focusing is a general technique for syntactically compartmentalizing the non-deterministic choices in a proof system, which not only improves proof search but also has the representational benefit of distilling sequent proofs into synthetic normal forms. However, since focusing is usually specified as a restriction of the sequent calculus, the technique has not been transferred to logics that lack a (shallow) sequent presentation, as is the case for some of the logics of the modal cube. We have recently extended the focusing technique to classical nested sequents, a generalization of ordinary sequents. In this work we further extend focusing to intuitionistic nested sequents, which can capture all the logics of the intuitionistic S5 cube in a modular fashion. We present an internal cut-elimination procedure for the focused system which in turn is used to show its completeness.

Cite as

Kaustuv Chaudhuri, Sonia Marin, and Lutz Straßburger. Modular Focused Proof Systems for Intuitionistic Modal Logics. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{chaudhuri_et_al:LIPIcs.FSCD.2016.16,
  author =	{Chaudhuri, Kaustuv and Marin, Sonia and Stra{\ss}burger, Lutz},
  title =	{{Modular Focused Proof Systems for Intuitionistic Modal Logics}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.16},
  URN =		{urn:nbn:de:0030-drops-59947},
  doi =		{10.4230/LIPIcs.FSCD.2016.16},
  annote =	{Keywords: intuitionistic modal logic, focusing, proof search, cut elimination, nested sequents}
}
Document
The Independence of Markov’s Principle in Type Theory

Authors: Thierry Coquand and Bassel Mannaa


Abstract
In this paper, we show that Markov's principle is not derivable in dependent type theory with natural numbers and one universe. One tentative way to prove this would be to remark that Markov's principle does not hold in a sheaf model of type theory over Cantor space, since Markov's principle does not hold for the generic point of this model. It is however not clear how to interpret the universe in a sheaf model. Instead we design an extension of type theory, which intuitively extends type theory by the addition of a generic point of Cantor space. We then show the consistency of this extension by a normalization argument. Markov's principle does not hold in this extension, and it follows that it cannot be proved in type theory.

Cite as

Thierry Coquand and Bassel Mannaa. The Independence of Markov’s Principle in Type Theory. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 17:1-17:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{coquand_et_al:LIPIcs.FSCD.2016.17,
  author =	{Coquand, Thierry and Mannaa, Bassel},
  title =	{{The Independence of Markov’s Principle in Type Theory}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{17:1--17:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.17},
  URN =		{urn:nbn:de:0030-drops-59939},
  doi =		{10.4230/LIPIcs.FSCD.2016.17},
  annote =	{Keywords: Forcing, Dependent type theory, Markov's Principle, Cantor Space}
}
Document
On Undefined and Meaningless in Lambda Definability

Authors: Fer-Jan de Vries


Abstract
We distinguish between undefined terms as used in lambda definability of partial recursive functions and meaningless terms as used in infinite lambda calculus for the infinitary terms models that generalise the Bohm model. While there are uncountable many known sets of meaningless terms, there are four known sets of undefined terms. Two of these four are sets of meaningless terms. In this paper we first present set of sufficient conditions for a set of lambda terms to serve as set of undefined terms in lambda definability of partial functions. The four known sets of undefined terms satisfy these conditions. Next we locate the smallest set of meaningless terms satisfying these conditions. This set sits very low in the lattice of all sets of meaningless terms. Any larger set of meaningless terms than this smallest set is a set of undefined terms. Thus we find uncountably many new sets of undefined terms. As an unexpected bonus of our careful analysis of lambda definability we obtain a natural modification, strict lambda-definability, which allows for a Barendregt style of proof in which the representation of composition is truly the composition of representations.

Cite as

Fer-Jan de Vries. On Undefined and Meaningless in Lambda Definability. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 18:1-18:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{devries:LIPIcs.FSCD.2016.18,
  author =	{de Vries, Fer-Jan},
  title =	{{On Undefined and Meaningless in Lambda Definability}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{18:1--18:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.18},
  URN =		{urn:nbn:de:0030-drops-59785},
  doi =		{10.4230/LIPIcs.FSCD.2016.18},
  annote =	{Keywords: lambda calculus, lambda definability, partial recursive function, undefined term, meaningless term}
}
Document
The Intersection Type Unification Problem

Authors: Andrej Dudenhefner, Moritz Martens, and Jakob Rehof


Abstract
The intersection type unification problem is an important component in proof search related to several natural decision problems in intersection type systems. It is unknown and remains open whether the unification problem is decidable. We give the first nontrivial lower bound for the problem by showing (our main result) that it is exponential time hard. Furthermore, we show that this holds even under rank 1 solutions (substitutions whose codomains are restricted to contain rank 1 types). In addition, we provide a fixed-parameter intractability result for intersection type matching (one-sided unification), which is known to be NP-complete. We place the intersection type unification problem in the context of unification theory. The equational theory of intersection types can be presented as an algebraic theory with an ACI (associative, commutative, and idempotent) operator (intersection type) combined with distributivity properties with respect to a second operator (function type). Although the problem is algebraically natural and interesting, it appears to occupy a hitherto unstudied place in the theory of unification, and our investigation of the problem suggests that new methods are required to understand the problem. Thus, for the lower bound proof, we were not able to reduce from known results in ACI-unification theory and use game-theoretic methods for two-player tiling games.

Cite as

Andrej Dudenhefner, Moritz Martens, and Jakob Rehof. The Intersection Type Unification Problem. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 19:1-19:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{dudenhefner_et_al:LIPIcs.FSCD.2016.19,
  author =	{Dudenhefner, Andrej and Martens, Moritz and Rehof, Jakob},
  title =	{{The Intersection Type Unification Problem}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{19:1--19:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.19},
  URN =		{urn:nbn:de:0030-drops-59955},
  doi =		{10.4230/LIPIcs.FSCD.2016.19},
  annote =	{Keywords: Intersection Type, Equational Theory, Unification, Tiling, Complexity}
}
Document
Computing Connected Proof(-Structure)s From Their Taylor Expansion

Authors: Giulio Guerrieri, Luc Pellissier, and Lorenzo Tortora de Falco


Abstract
We show that every connected Multiplicative Exponential Linear Logic (MELL) proof-structure (with or without cuts) is uniquely determined by a well-chosen element of its Taylor expansion: the one obtained by taking two copies of the content of each box. As a consequence, the relational model is injective with respect to connected MELL proof-structures.

Cite as

Giulio Guerrieri, Luc Pellissier, and Lorenzo Tortora de Falco. Computing Connected Proof(-Structure)s From Their Taylor Expansion. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{guerrieri_et_al:LIPIcs.FSCD.2016.20,
  author =	{Guerrieri, Giulio and Pellissier, Luc and Tortora de Falco, Lorenzo},
  title =	{{Computing Connected Proof(-Structure)s From Their Taylor Expansion}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{20:1--20:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.20},
  URN =		{urn:nbn:de:0030-drops-60031},
  doi =		{10.4230/LIPIcs.FSCD.2016.20},
  annote =	{Keywords: proof-nets, (differential) linear logic, relational model, Taylor expansion}
}
Document
Strongly Normalising Cyclic Data Computation by Iteration Categories of Second-Order Algebraic Theories

Authors: Makoto Hamana


Abstract
Cyclic data structures, such as cyclic lists, in functional programming are tricky to handle because of their cyclicity. This paper presents an investigation of categorical, algebraic, and computational foundations of cyclic datatypes. Our framework of cyclic datatypes is based on second-order algebraic theories of Fiore et al., which give a uniform setting for syntax, types, and computation rules for describing and reasoning about cyclic datatypes. We extract the ``fold'' computation rules from the categorical semantics based on iteration categories of Bloom and Esik. Thereby, the rules are correct by construction. Finally, we prove strong normalisation using the General Schema criterion for second-order computation rules. Rather than the fixed point law, we particularly choose Bekic law for computation, which is a key to obtaining strong normalisation.

Cite as

Makoto Hamana. Strongly Normalising Cyclic Data Computation by Iteration Categories of Second-Order Algebraic Theories. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{hamana:LIPIcs.FSCD.2016.21,
  author =	{Hamana, Makoto},
  title =	{{Strongly Normalising Cyclic Data Computation by Iteration Categories of Second-Order Algebraic Theories}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{21:1--21:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.21},
  URN =		{urn:nbn:de:0030-drops-59792},
  doi =		{10.4230/LIPIcs.FSCD.2016.21},
  annote =	{Keywords: cyclic data structures, traced cartesian category, fixed point, functional programming, fold}
}
Document
Non-Omega-Overlapping TRSs are UN

Authors: Stefan Kahrs and Connor Smith


Abstract
This paper solves problem #79 of RTA's list of open problems --- in the positive. If the rules of a TRS do not overlap w.r.t. substitutions of infinite terms then the TRS has unique normal forms. We solve the problem by reducing the problem to one of consistency for "similar" constructor term rewriting systems. For this we introduce a new proof technique. We define a relation ⇓ that is consistent by construction, and which --- if transitive --- would coincide with the rewrite system's equivalence relation =R. We then prove the transitivity of ⇓ by coalgebraic reasoning. Any concrete proof for instances of this relation only refers to terms of some finite coalgebra, and we then construct an equivalence relation on that coalgebra which coincides with ⇓.

Cite as

Stefan Kahrs and Connor Smith. Non-Omega-Overlapping TRSs are UN. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{kahrs_et_al:LIPIcs.FSCD.2016.22,
  author =	{Kahrs, Stefan and Smith, Connor},
  title =	{{Non-Omega-Overlapping TRSs are UN}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{22:1--22:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.22},
  URN =		{urn:nbn:de:0030-drops-59968},
  doi =		{10.4230/LIPIcs.FSCD.2016.22},
  annote =	{Keywords: consistency, omega-substitutions, uniqueness of normal forms}
}
Document
Complexity Hierarchies and Higher-Order Cons-Free Rewriting

Authors: Cynthia Kop and Jakob Grue Simonsen


Abstract
Constructor rewriting systems are said to be cons-free if, roughly, constructor terms in the right-hand sides of rules are subterms of constructor terms in the left-hand side; the computational intuition is that rules cannot build new data structures. It is well-known that cons-free programming languages can be used to characterize computational complexity classes, and that cons-free first-order term rewriting can be used to characterize the set of polynomial-time decidable sets. We investigate cons-free higher-order term rewriting systems, the complexity classes they characterize, and how these depend on the order of the types used in the systems. We prove that, for every k >= 1, left-linear cons-free systems with type order k characterize E^kTIME if arbitrary evaluation is used (i.e., the system does not have a fixed reduction strategy). The main difference with prior work in implicit complexity is that (i) our results hold for non-orthogonal term rewriting systems with possible rule overlaps with no assumptions about reduction strategy, (ii) results for such term rewriting systems have previously only been obtained for k = 1, and with additional syntactic restrictions on top of cons-freeness and left-linearity. Our results are apparently among the first implicit characterizations of the hierarchy E^1TIME != E^2TIME != .... Our work confirms prior results that having full non-determinism (via overlaps of rules) does not directly allow for characterization of non-deterministic complexity classes like NE. We also show that non-determinism makes the classes characterized highly sensitive to minor syntactic changes such as admitting product types or non-left-linear rules.

Cite as

Cynthia Kop and Jakob Grue Simonsen. Complexity Hierarchies and Higher-Order Cons-Free Rewriting. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{kop_et_al:LIPIcs.FSCD.2016.23,
  author =	{Kop, Cynthia and Grue Simonsen, Jakob},
  title =	{{Complexity Hierarchies and Higher-Order Cons-Free Rewriting}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.23},
  URN =		{urn:nbn:de:0030-drops-59972},
  doi =		{10.4230/LIPIcs.FSCD.2016.23},
  annote =	{Keywords: higher-order term rewriting, implicit complexity, cons-freeness, ETIME hierarchy}
}
Document
Weighted Relational Models for Mobility

Authors: James Laird


Abstract
We investigate operational and denotational semantics for computational and concurrent systems with mobile names which capture their computational properties. For example, various properties of fixed networks, such as shortest or longest path, transition probabilities, and secure data flows, correspond to the ``sum'' in a semiring of the weights of paths through the network: we aim to model networks with a dynamic topology in a similar way. Alongside rich computational formalisms such as the lambda-calculus, these can be represented as terms in a calculus of solos with weights from a complete semiring $R$, so that reduction associates a weight in R to each reduction path. Taking inspiration from differential nets, we develop a denotational semantics for this calculus in the category of sets and R-weighted relations, based on its differential and compact-closed structure, but giving a simple, syntax-independent representation of terms as matrices over R. We show that this corresponds to the sum in R of the values associated to its independent reduction paths, and that our semantics is fully abstract with respect to the observational equivalence induced by sum-of-paths evaluation.

Cite as

James Laird. Weighted Relational Models for Mobility. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 24:1-24:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{laird:LIPIcs.FSCD.2016.24,
  author =	{Laird, James},
  title =	{{Weighted Relational Models for  Mobility}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{24:1--24:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.24},
  URN =		{urn:nbn:de:0030-drops-59982},
  doi =		{10.4230/LIPIcs.FSCD.2016.24},
  annote =	{Keywords: Concurrency, Mobility, Denotational Semantics}
}
Document
Focusing in Orthologic

Authors: Olivier Laurent


Abstract
We propose new sequent calculus systems for orthologic (also known as minimal quantum logic) which satisfy the cut elimination property. The first one is a very simple system relying on the involutive status of negation. The second one incorporates the notion of focusing (coming from linear logic) to add constraints on proofs and thus to facilitate proof search. We demonstrate how to take benefits from the new systems in automatic proof search for orthologic.

Cite as

Olivier Laurent. Focusing in Orthologic. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 25:1-25:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{laurent:LIPIcs.FSCD.2016.25,
  author =	{Laurent, Olivier},
  title =	{{Focusing in Orthologic}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{25:1--25:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.25},
  URN =		{urn:nbn:de:0030-drops-59805},
  doi =		{10.4230/LIPIcs.FSCD.2016.25},
  annote =	{Keywords: orthologic, focusing, minimal quantum logic, linear logic, automatic proof search, cut elimination}
}
Document
Functions-as-Constructors Higher-Order Unification

Authors: Tomer Libal and Dale Miller


Abstract
Unification is a central operation in the construction of a range of computational logic systems based on first-order and higher-order logics. First-order unification has a number of properties that dominates the way it is incorporated within such systems. In particular, first-order unification is decidable, unary, and can be performed on untyped term structures. None of these three properties hold for full higher-order unification: unification is undecidable, unifiers can be incomparable, and term-level typing can dominate the search for unifiers. The so-called pattern subset of higher-order unification was designed to be a small extension to first-order unification that respected the basic laws governing lambda-binding (the equalities of alpha, beta, and eta-conversion) but which also satisfied those three properties. While the pattern fragment of higher-order unification has been popular in various implemented systems and in various theoretical considerations, it is too weak for a number of applications. In this paper, we define an extension of pattern unification that is motivated by some existing applications and which satisfies these three properties. The main idea behind this extension is that the arguments to a higher-order, free variable can be more than just distinct bound variables: they can also be terms constructed from (sufficient numbers of) such variables using term constructors and where no argument is a subterm of any other argument. We show that this extension to pattern unification satisfies the three properties mentioned above.

Cite as

Tomer Libal and Dale Miller. Functions-as-Constructors Higher-Order Unification. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 26:1-26:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{libal_et_al:LIPIcs.FSCD.2016.26,
  author =	{Libal, Tomer and Miller, Dale},
  title =	{{Functions-as-Constructors Higher-Order Unification}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{26:1--26:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.26},
  URN =		{urn:nbn:de:0030-drops-59810},
  doi =		{10.4230/LIPIcs.FSCD.2016.26},
  annote =	{Keywords: higher-order unification, pattern unification}
}
Document
Homological Computations for Term Rewriting Systems

Authors: Philippe Malbos and Samuel Mimram


Abstract
An important problem in universal algebra consists in finding presentations of algebraic theories by generators and relations, which are as small as possible. Exhibiting lower bounds on the number of those generators and relations for a given theory is a difficult task because it a priori requires considering all possible sets of generators for a theory and no general method exists. In this article, we explain how homological computations can provide such lower bounds, in a systematic way, and show how to actually compute those in the case where a presentation of the theory by a convergent rewriting system is known. We also introduce the notion of coherent presentation of a theory in order to consider finer homotopical invariants. In some aspects, this work generalizes, to term rewriting systems, Squier's celebrated homological and homotopical invariants for string rewriting systems.

Cite as

Philippe Malbos and Samuel Mimram. Homological Computations for Term Rewriting Systems. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{malbos_et_al:LIPIcs.FSCD.2016.27,
  author =	{Malbos, Philippe and Mimram, Samuel},
  title =	{{Homological Computations for Term Rewriting Systems}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{27:1--27:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.27},
  URN =		{urn:nbn:de:0030-drops-59821},
  doi =		{10.4230/LIPIcs.FSCD.2016.27},
  annote =	{Keywords: term rewriting system, Lawvere theory, Tietze equivalence, resolution, homology, convergent pres entation, coherent presentation}
}
Document
Reversible Term Rewriting

Authors: Naoki Nishida, Adrián Palacios, and Germán Vidal


Abstract
Essentially, in a reversible programming language, for each forward computation step from state S to state S', there exists a constructive and deterministic method to go backwards from state S' to state S. Besides its theoretical interest, reversible computation is a fundamental concept which is relevant in many different areas like cellular automata, bidirectional program transformation, or quantum computing, to name a few. In this paper, we focus on term rewriting, a computation model that underlies most rule-based programming languages. In general, term rewriting is not reversible, even for injective functions; namely, given a rewrite step t1 -> t2, we do not always have a decidable and deterministic method to get t1 from t2. Here, we introduce a conservative extension of term rewriting that becomes reversible. Furthermore, we also define a transformation to make a rewrite system reversible using standard term rewriting.

Cite as

Naoki Nishida, Adrián Palacios, and Germán Vidal. Reversible Term Rewriting. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{nishida_et_al:LIPIcs.FSCD.2016.28,
  author =	{Nishida, Naoki and Palacios, Adri\'{a}n and Vidal, Germ\'{a}n},
  title =	{{Reversible Term Rewriting}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{28:1--28:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.28},
  URN =		{urn:nbn:de:0030-drops-59841},
  doi =		{10.4230/LIPIcs.FSCD.2016.28},
  annote =	{Keywords: term rewriting, reversible computation, program transformation}
}
Document
Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion

Authors: Christian Sternagel and Thomas Sternagel


Abstract
Suzuki et al. showed that properly oriented, right-stable, orthogonal, and oriented conditional term rewrite systems with extra variables in right-hand sides are confluent. We present our Isabelle/HOL formalization of this result, including two generalizations. On the one hand, we relax proper orientedness and orthogonality to extended proper orientedness and almost orthogonality modulo infeasibility, as suggested by Suzuki et al. On the other hand, we further loosen the requirements of the latter, enabling more powerful methods for proving infeasibility of conditional critical pairs. Furthermore, we formalized a construction by Jacquemard that employs exact tree automata completion for non-reachability analysis and apply it to certify infeasibility of conditional critical pairs. Combining these two results and extending the conditional confluence checker ConCon accordingly, we are able to automatically prove and certify confluence of an important class of conditional term rewrite systems.

Cite as

Christian Sternagel and Thomas Sternagel. Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 29:1-29:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{sternagel_et_al:LIPIcs.FSCD.2016.29,
  author =	{Sternagel, Christian and Sternagel, Thomas},
  title =	{{Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{29:1--29:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.29},
  URN =		{urn:nbn:de:0030-drops-59996},
  doi =		{10.4230/LIPIcs.FSCD.2016.29},
  annote =	{Keywords: certification, conditional term rewriting, confluence, infeasible critical pairs, non-reachability}
}
Document
Category Theory in Coq 8.5

Authors: Amin Timany and Bart Jacobs


Abstract
We report on our experience implementing category theory in Coq 8.5. Our work formalizes most of basic category theory, including concepts not covered by existing formalizations, in a library that is fit to be used as a general-purpose category-theoretical foundation. Our development particularly takes advantage of two features new to Coq 8.5: primitive projections for records and universe polymorphism. Primitive projections allow for well-behaved dualities while universe polymorphism provides a relative notion of largeness and smallness. The latter is one of the main contributions of this paper. It pushes the limits of the new universe polymorphism and constraint inference algorithm of Coq 8.5. In this paper we present in detail smallness and largeness in categories and the foundation they are built on top of. We furthermore explain how we have used the universe polymorphism of Coq 8.5 to represent smallness and largeness arguments by simply ignoring them and entrusting them to the universe inference algorithm of Coq 8.5. We also briefly discuss our experience throughout this implementation, discuss concepts formalized in this development and give a comparison with a few other developments of similar extent.

Cite as

Amin Timany and Bart Jacobs. Category Theory in Coq 8.5. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{timany_et_al:LIPIcs.FSCD.2016.30,
  author =	{Timany, Amin and Jacobs, Bart},
  title =	{{Category Theory in Coq 8.5}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{30:1--30:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.30},
  URN =		{urn:nbn:de:0030-drops-60003},
  doi =		{10.4230/LIPIcs.FSCD.2016.30},
  annote =	{Keywords: Category Theory, Coq 8.5, Universe Polymorphism, Homotopy Type Theory}
}
Document
Formal Languages, Formally and Coinductively

Authors: Dmitriy Traytel


Abstract
Traditionally, formal languages are defined as sets of words. More recently, the alternative coalgebraic or coinductive representation as infinite tries, i.e., prefix trees branching over the alphabet, has been used to obtain compact and elegant proofs of classic results in language theory. In this paper, we study this representation in the Isabelle proof assistant. We define regular operations on infinite tries and prove the axioms of Kleene algebra for those operations. Thereby, we exercise corecursion and coinduction and confirm the coinductive view being profitable in formalizations, as it improves over the set-of-words view with respect to proof automation.

Cite as

Dmitriy Traytel. Formal Languages, Formally and Coinductively. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 31:1-31:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{traytel:LIPIcs.FSCD.2016.31,
  author =	{Traytel, Dmitriy},
  title =	{{Formal Languages, Formally and Coinductively}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{31:1--31:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.31},
  URN =		{urn:nbn:de:0030-drops-59853},
  doi =		{10.4230/LIPIcs.FSCD.2016.31},
  annote =	{Keywords: Formal languages, codatatypes, corecursion, coinduction, interactive theorem proving, Isabelle HOL}
}
Document
Normalisation by Random Descent

Authors: Vincent van Oostrom and Yoshihito Toyama


Abstract
We present abstract hyper-normalisation results for strategies. These results are then applied to term rewriting systems, both first and higher-order. For example, we show hyper-normalisation of the left--outer strategy for, what we call, left--outer pattern rewrite systems, a class comprising both Combinatory Logic and the lambda-calculus but also systems with critical pairs. Our results apply to strategies that need not be deterministic but do have Newman's random descent property: all reductions to normal form have the same length, with Huet and Lévy's external strategy being an example. Technically, we base our development on supplementing the usual notion of commutation diagram with a notion of order, expressing that the measure of its right leg does not exceed that of its left leg, where measure is an abstraction of the usual notion of length. We give an exact characterisation of such global commutation diagrams, for pairs of reductions, by means of local ones, for pairs of steps, we dub Dyck diagrams.

Cite as

Vincent van Oostrom and Yoshihito Toyama. Normalisation by Random Descent. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 32:1-32:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{vanoostrom_et_al:LIPIcs.FSCD.2016.32,
  author =	{van Oostrom, Vincent and Toyama, Yoshihito},
  title =	{{Normalisation by Random Descent}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{32:1--32:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.32},
  URN =		{urn:nbn:de:0030-drops-59862},
  doi =		{10.4230/LIPIcs.FSCD.2016.32},
  annote =	{Keywords: strategy, hyper-normalisation, commutation, random descent}
}
Document
Ground Confluence Prover based on Rewriting Induction

Authors: Takahito Aoto and Yoshihito Toyama


Abstract
Ground confluence of term rewriting systems guarantees that all ground terms are confluent. Recently, interests in proving confluence of term rewriting systems automatically has grown, and confluence provers have been developed. But they mainly focus on confluence and not ground confluence. In fact, little interest has been paid to developing tools for proving ground confluence automatically. We report an implementation of a ground confluence prover based on rewriting induction, which is a method originally developed for proving inductive theorems.

Cite as

Takahito Aoto and Yoshihito Toyama. Ground Confluence Prover based on Rewriting Induction. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 33:1-33:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{aoto_et_al:LIPIcs.FSCD.2016.33,
  author =	{Aoto, Takahito and Toyama, Yoshihito},
  title =	{{Ground Confluence Prover based on Rewriting Induction}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{33:1--33:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.33},
  URN =		{urn:nbn:de:0030-drops-59873},
  doi =		{10.4230/LIPIcs.FSCD.2016.33},
  annote =	{Keywords: Ground Confluence, Rewriting Induction, Non-Orientable Equations, Term Rewriting Systems}
}
Document
Globular: An Online Proof Assistant for Higher-Dimensional Rewriting

Authors: Krzysztof Bar, Aleks Kissinger, and Jamie Vicary


Abstract
This article introduces Globular, an online proof assistant for the formalization and verification of proofs in higher-dimensional category theory. The tool produces graphical visualizations of higher-dimensional proofs, assists in their construction with a point-and-click interface, and performs type checking to prevent incorrect rewrites. Hosted on the web, it has a low barrier to use, and allows hyperlinking of formalized proofs directly from research papers. It allows the formalization of proofs from logic, topology and algebra which are not formalizable by other methods, and we give several examples.

Cite as

Krzysztof Bar, Aleks Kissinger, and Jamie Vicary. Globular: An Online Proof Assistant for Higher-Dimensional Rewriting. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 34:1-34:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{bar_et_al:LIPIcs.FSCD.2016.34,
  author =	{Bar, Krzysztof and Kissinger, Aleks and Vicary, Jamie},
  title =	{{Globular: An Online Proof Assistant for Higher-Dimensional Rewriting}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{34:1--34:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.34},
  URN =		{urn:nbn:de:0030-drops-59880},
  doi =		{10.4230/LIPIcs.FSCD.2016.34},
  annote =	{Keywords: higher category theory, higher-dimensional rewriting, interactive theorem proving}
}
Document
Interaction Automata and the ia2d Interpreter

Authors: Stéphane Gimenez and David Obwaller


Abstract
We introduce interaction automata as a topological model of computation and present the conceptual plane interpreter ia2d. Interaction automata form a refinement of both interaction nets and cellular automata models that combine data deployment, memory management and structured computation mechanisms. Their local structure is inspired from pointer machines and allows an asynchronous spatial distribution of the computation. Our tool can be considered as a proof-of-concept piece of abstract hardware on which functional programs can be run in parallel.

Cite as

Stéphane Gimenez and David Obwaller. Interaction Automata and the ia2d Interpreter. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 35:1-35:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{gimenez_et_al:LIPIcs.FSCD.2016.35,
  author =	{Gimenez, St\'{e}phane and Obwaller, David},
  title =	{{Interaction Automata and the ia2d Interpreter}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{35:1--35:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.35},
  URN =		{urn:nbn:de:0030-drops-59896},
  doi =		{10.4230/LIPIcs.FSCD.2016.35},
  annote =	{Keywords: Interaction nets, computation models, parallel computation, functional programming}
}
Document
Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems

Authors: Franziska Rapp and Aart Middeldorp


Abstract
The first-order theory of rewriting is decidable for finite left-linear right-ground rewrite systems. We present a new tool that implements the decision procedure for this theory. It is based on tree automata techniques. The tool offers the possibility to synthesize rewrite systems that satisfy properties that are expressible in the first-order theory of rewriting.

Cite as

Franziska Rapp and Aart Middeldorp. Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 36:1-36:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{rapp_et_al:LIPIcs.FSCD.2016.36,
  author =	{Rapp, Franziska and Middeldorp, Aart},
  title =	{{Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{36:1--36:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.36},
  URN =		{urn:nbn:de:0030-drops-60018},
  doi =		{10.4230/LIPIcs.FSCD.2016.36},
  annote =	{Keywords: first-order theory, ground rewrite systems, automation, synthesis}
}

Filters


Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail