Volume
LIPIcs, Volume 52
1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Formal Structures for Computation and Deduction (FSCD)
Event
FSCD 2016, June 22-26, 2016, Porto, PortugalEditors
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
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 52, FSCD'16, Complete Volume
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.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
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.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
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.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
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.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
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.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
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.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.
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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
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.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}
}