38 Search Results for "Kirchner, H�l�ne"

Document
Complete Volume
DOI: 10.4230/LIPIcs.FSCD.2018
LIPIcs, Volume 108, FSCD'18, Complete Volume

Authors: Hélène Kirchner

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
LIPIcs, Volume 108, FSCD'18, Complete Volume
Cite as

3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Proceedings{kirchner:LIPIcs.FSCD.2018,
  title =	{{LIPIcs, Volume 108, FSCD'18, Complete Volume}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018},
  URN =		{urn:nbn:de:0030-drops-92819},
  doi =		{10.4230/LIPIcs.FSCD.2018},
  annote =	{Keywords: Theory of computation, Models of computation, Formal languages and automata theory, Logic, Semantics and reasoning, Software and its engineering}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.FSCD.2018.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Hélène Kirchner

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

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

Copy BibTex To Clipboard

@InProceedings{kirchner:LIPIcs.FSCD.2018.0,
  author =	{Kirchner, H\'{e}l\`{e}ne},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{0:i--0:xx},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.0},
  URN =		{urn:nbn:de:0030-drops-91706},
  doi =		{10.4230/LIPIcs.FSCD.2018.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2018.1
Analysing Privacy-Type Properties in Cryptographic Protocols (Invited Talk)

Authors: Stéphanie Delaune

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
Cryptographic protocols aim at securing communications over insecure networks such as the Internet, where dishonest users may listen to communications and interfere with them. For example, passports are no more pure paper documents. Instead, they contain a chip that stores additional information such as pictures and fingerprints of their holder. In order to ensure privacy, these chips include a mechanism, i.e. a cryptographic protocol, that does not let the passport disclose private information to external users except the intended terminal. This is just a single example but of course privacy appears in many other contexts such as RFIDs technologies or electronic voting. Formal methods have been successfully applied to automatically analyse traditional protocols and discover their flaws. Privacy-type security properties (e.g. anonymity, unlinkability, vote secrecy, ...) are expressed relying on a notion of behavioural equivalence, and are actually more difficult to analyse than confidentiality and authentication properties. We will discuss some recent advances that have been done to analyse automatically equivalence-based security properties, and we will review some issues that remain to be solved in this field.
Cite as

Stéphanie Delaune. Analysing Privacy-Type Properties in Cryptographic Protocols (Invited Talk). In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 1:1-1:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{delaune:LIPIcs.FSCD.2018.1,
  author =	{Delaune, St\'{e}phanie},
  title =	{{Analysing Privacy-Type Properties in Cryptographic Protocols}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{1:1--1:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.1},
  URN =		{urn:nbn:de:0030-drops-91715},
  doi =		{10.4230/LIPIcs.FSCD.2018.1},
  annote =	{Keywords: cryptographic protocols, symbolic models, privacy-related properties, behavioural equivalence}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2018.2
Formal Design, Implementation and Verification of Blockchain Languages (Invited Talk)

Authors: Grigore Rosu

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
This invited paper describes recent, ongoing and planned work on the use of the rewrite-based semantic framework K to formally design, implement and verify blockchain languages and virtual machines. Both academic and commercial endeavors are discussed, as well as thoughts and directions for future research and development.
Cite as

Grigore Rosu. Formal Design, Implementation and Verification of Blockchain Languages (Invited Talk). In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 2:1-2:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{rosu:LIPIcs.FSCD.2018.2,
  author =	{Rosu, Grigore},
  title =	{{Formal Design, Implementation and Verification of Blockchain Languages}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{2:1--2:6},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.2},
  URN =		{urn:nbn:de:0030-drops-91722},
  doi =		{10.4230/LIPIcs.FSCD.2018.2},
  annote =	{Keywords: Formal semantics, Program verification, Blockchain}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2018.3
Challenges in Quantum Programming Languages (Invited Talk)

Authors: Peter Selinger

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
In this talk, I will give an overview of some recent progress and current challenges in the design of quantum programming languages. Unlike classical programs, which can in principle be debugged by stopping the program at critical moments and examining the contents of variables, quantum programs are not amenable to traditional debugging because the state of a quantum system cannot usually be examined in a meaningful way. Therefore, we need other methods for ensuring the correctness of quantum programs, such as formal verification. For this reason, I advocate the use of strongly typed, functional programming languages for quantum computing. As far as functional quantum programming languages are concerned, there is currently a relatively wide gap between theory and practice. On the one hand, we have languages with strong theoretical foundations, such as the quantum lambda calculus, which operate at a relatively low level of abstraction and lack many features that would be useful to practical quantum programmers. On the other hand, we have practical functional quantum programming languages such as Quipper, which is implemented as an embedded language in Haskell, has many high-level features, and has been used in large-scale projects, but lacks a theoretical basis and a strong type system [Green et al., 2013; Green et al., 2013; Green et al., 2013; Smith et al., 2014]. We have recently attempted to narrow this gap through a family of languages called Proto-Quipper, which are designed to offer Quipper-like features while having sound theoretical foundations [Ross, 2015; Rios and Selinger, 2018]. I will give an overview of Quipper and its most useful features, report on the progress we made with formalizing fragments of Quipper, and outline several of the still remaining challenges.
Cite as

Peter Selinger. Challenges in Quantum Programming Languages (Invited Talk). In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{selinger:LIPIcs.FSCD.2018.3,
  author =	{Selinger, Peter},
  title =	{{Challenges in Quantum Programming Languages}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{3:1--3:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.3},
  URN =		{urn:nbn:de:0030-drops-91730},
  doi =		{10.4230/LIPIcs.FSCD.2018.3},
  annote =	{Keywords: Quantum programming languages}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2018.4
Proof Techniques for Program Equivalence in Probabilistic Higher-Order Languages (Invited Talk)

Authors: Valeria Vignudelli

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
While the theory of functional higher-order languages, starting from lambda-calculi, is a well-established research field, it is only in recent years that the operational semantics of higher-order languages with probabilistic operators has started to be extensively studied. A fundamental notion in the semantics of programming languages is that of program equivalence. In higher-order languages, program equivalence is generally formalized as a contextual equivalence [Morris, 1968], which can be hard to prove directly. This has motivated the study of proof techniques for contextual equivalence, from inductive ones, such as logical relations [Andrew Pitts, 2005], to coinductive ones, mainly in the form of bisimulations [Abramsky, 1990]. In this talk I will discuss proof techniques for program equivalence in languages combining higher-order and probabilistic features. Several operational methods, traditionally developed in a deterministic setting, have been adapted to probabilistic higher-order languages [Ales Bizjak and Lars Birkedal, 2015; Dal Lago et al., 2014; Raphaëlle Crubillé and Ugo Dal Lago, 2014]. I will discuss these proof methods and focus on bisimulation-based techniques, showing how probabilities, combined with different language features, force a number of modifications to the definition of bisimulation [Crubillé et al., 2015; Sangiorgi and Vignudelli, 2016].
Cite as

Valeria Vignudelli. Proof Techniques for Program Equivalence in Probabilistic Higher-Order Languages (Invited Talk). In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{vignudelli:LIPIcs.FSCD.2018.4,
  author =	{Vignudelli, Valeria},
  title =	{{Proof Techniques for Program Equivalence in Probabilistic Higher-Order Languages}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{4:1--4:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.4},
  URN =		{urn:nbn:de:0030-drops-91749},
  doi =		{10.4230/LIPIcs.FSCD.2018.4},
  annote =	{Keywords: Lambda Calculus, Contextual Equivalence, Bisimulation, Probabilistic Programming Languages}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.5
A Unifying Framework for Type Inhabitation

Authors: Sandra Alves and Sabine Broda

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
In this paper we define a framework to address different kinds of problems related to type inhabitation, such as type checking, the emptiness problem, generation of inhabitants and counting, in a uniform way. Our framework uses an alternative representation for types, called the pre-grammar of the type, on which different methods for these problems are based. Furthermore, we define a scheme for a decision algorithm that, for particular instantiations of the parameters, can be used to show different inhabitation related problems to be in PSPACE.
Cite as

Sandra Alves and Sabine Broda. A Unifying Framework for Type Inhabitation. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{alves_et_al:LIPIcs.FSCD.2018.5,
  author =	{Alves, Sandra and Broda, Sabine},
  title =	{{A Unifying Framework for Type Inhabitation}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{5:1--5:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.5},
  URN =		{urn:nbn:de:0030-drops-91758},
  doi =		{10.4230/LIPIcs.FSCD.2018.5},
  annote =	{Keywords: simple types, type inhabitation, rewriting, PSPACE}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.6
Confluence of Prefix-Constrained Rewrite Systems

Authors: Nirina Andrianarivelo and Pierre Réty

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
Prefix-constrained rewriting is a strict extension of context-sensitive rewriting. We study the confluence of prefix-constrained rewrite systems, which are composed of rules of the form L: l -> r where L is a regular string language that defines the allowed rewritable positions. The usual notion of Knuth-Bendix's critical pair needs to be extended using regular string languages, and the convergence of all critical pairs is not enough to ensure local confluence. Thanks to an additional restriction we get local confluence, and then confluence for terminating systems, which makes the word problem decidable. Moreover we present an extended Knuth-Bendix completion procedure, to transform a non-confluent prefix-constrained rewrite system into a confluent one.
Cite as

Nirina Andrianarivelo and Pierre Réty. Confluence of Prefix-Constrained Rewrite Systems. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{andrianarivelo_et_al:LIPIcs.FSCD.2018.6,
  author =	{Andrianarivelo, Nirina and R\'{e}ty, Pierre},
  title =	{{Confluence of Prefix-Constrained Rewrite Systems}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{6:1--6:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.6},
  URN =		{urn:nbn:de:0030-drops-91762},
  doi =		{10.4230/LIPIcs.FSCD.2018.6},
  annote =	{Keywords: prefix-constrained term rewriting, confluence, critical pair}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.7
Fixed-Point Constraints for Nominal Equational Unification

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

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
We propose a new axiomatisation of the alpha-equivalence relation for nominal terms, based on a primitive notion of fixed-point constraint. We show that the standard freshness relation between atoms and terms can be derived from the more primitive notion of permutation fixed-point, and use this result to prove the correctness of the new alpha-equivalence axiomatisation. This gives rise to a new notion of nominal unification, where solutions for unification problems are pairs of a fixed-point context and a substitution. Although it may seem less natural than the standard notion of nominal unifier based on freshness constraints, the notion of unifier based on fixed-point constraints behaves better when equational theories are considered: for example, nominal unification remains finitary in the presence of commutativity, whereas it becomes infinitary when unifiers are expressed using freshness contexts.
Cite as

Mauricio Ayala-Rincón, Maribel Fernández, and Daniele Nantes-Sobrinho. Fixed-Point Constraints for Nominal Equational Unification. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 7:1-7:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{ayalarincon_et_al:LIPIcs.FSCD.2018.7,
  author =	{Ayala-Rinc\'{o}n, Mauricio and Fern\'{a}ndez, Maribel and Nantes-Sobrinho, Daniele},
  title =	{{Fixed-Point Constraints for Nominal Equational Unification}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{7:1--7:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.7},
  URN =		{urn:nbn:de:0030-drops-91777},
  doi =		{10.4230/LIPIcs.FSCD.2018.7},
  annote =	{Keywords: nominal terms, fixed-point equations, nominal unification, equational theories}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.8
Strict Ideal Completions of the Lambda Calculus

Authors: Patrick Bahr

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
The infinitary lambda calculi pioneered by Kennaway et al. extend the basic lambda calculus by metric completion to infinite terms and reductions. Depending on the chosen metric, the resulting infinitary calculi exhibit different notions of strictness. To obtain infinitary normalisation and infinitary confluence properties for these calculi, Kennaway et al. extend beta-reduction with infinitely many `bot-rules', which contract meaningless terms directly to bot. Three of the resulting Böhm reduction calculi have unique infinitary normal forms corresponding to Böhm-like trees. In this paper we develop a corresponding theory of infinitary lambda calculi based on ideal completion instead of metric completion. We show that each of our calculi conservatively extends the corresponding metric-based calculus. Three of our calculi are infinitarily normalising and confluent; their unique infinitary normal forms are exactly the Böhm-like trees of the corresponding metric-based calculi. Our calculi dispense with the infinitely many bot-rules of the metric-based calculi. The fully non-strict calculus (called 111) consists of only beta-reduction, while the other two calculi (called 001 and 101) require two additional rules that precisely state their strictness properties: lambda x.bot -> bot (for 001) and bot M -> bot (for 001 and 101).
Cite as

Patrick Bahr. Strict Ideal Completions of the Lambda Calculus. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bahr:LIPIcs.FSCD.2018.8,
  author =	{Bahr, Patrick},
  title =	{{Strict Ideal Completions of the Lambda Calculus}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{8:1--8:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.8},
  URN =		{urn:nbn:de:0030-drops-91787},
  doi =		{10.4230/LIPIcs.FSCD.2018.8},
  annote =	{Keywords: lambda calculus, infinitary rewriting, B\"{o}hm trees, meaningless terms, confluence}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.9
Term-Graph Anti-Unification

Authors: Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
We study anti-unification for possibly cyclic, unranked term-graphs and develop an algorithm, which computes a minimal complete set of generalizations for them. For bisimilar graphs the algorithm computes the join in the lattice generated by a functional bisimulation. These results generalize anti-unification for ranked and unranked terms to the corresponding term-graphs, and solve also anti-unification problems for rational terms and dags. Our results open a way to widen anti-unification based code clone detection techniques from a tree representation to a graph representation of the code.
Cite as

Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret. Term-Graph Anti-Unification. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{baumgartner_et_al:LIPIcs.FSCD.2018.9,
  author =	{Baumgartner, Alexander and Kutsia, Temur and Levy, Jordi and Villaret, Mateu},
  title =	{{Term-Graph Anti-Unification}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{9:1--9:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.9},
  URN =		{urn:nbn:de:0030-drops-91797},
  doi =		{10.4230/LIPIcs.FSCD.2018.9},
  annote =	{Keywords: Cyclic term-graps, anti-unification, least general generalization}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.10
Proof Nets for Bi-Intuitionistic Linear Logic

Authors: Gianluigi Bellin and Willem B. Heijltjes

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
Bi-Intuitionistic Linear Logic (BILL) is an extension of Intuitionistic Linear Logic with a par, dual to the tensor, and subtraction, dual to linear implication. It is the logic of categories with a monoidal closed and a monoidal co-closed structure that are related by linear distributivity, a strength of the tensor over the par. It conservatively extends Full Intuitionistic Linear Logic (FILL), which includes only the par. We give proof nets for the multiplicative, unit-free fragment MBILL-. Correctness is by local rewriting in the style of Danos contractibility, which yields sequentialization into a relational sequent calculus extending the existing one for FILL. We give a second, geometric correctness condition combining Danos-Regnier switching and Lamarche's Essential Net criterion, and demonstrate composition both inductively and as a one-off global operation.
Cite as

Gianluigi Bellin and Willem B. Heijltjes. Proof Nets for Bi-Intuitionistic Linear Logic. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bellin_et_al:LIPIcs.FSCD.2018.10,
  author =	{Bellin, Gianluigi and Heijltjes, Willem B.},
  title =	{{Proof Nets for Bi-Intuitionistic Linear Logic}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{10:1--10:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.10},
  URN =		{urn:nbn:de:0030-drops-91800},
  doi =		{10.4230/LIPIcs.FSCD.2018.10},
  annote =	{Keywords: proof nets, intuitionistic linear logic, contractibility, linear logic}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.11
Counting Environments and Closures

Authors: Maciej Bendkowski and Pierre Lescanne

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
Environments and closures are two of the main ingredients of evaluation in lambda-calculus. A closure is a pair consisting of a lambda-term and an environment, whereas an environment is a list of lambda-terms assigned to free variables. In this paper we investigate some dynamic aspects of evaluation in lambda-calculus considering the quantitative, combinatorial properties of environments and closures. Focusing on two classes of environments and closures, namely the so-called plain and closed ones, we consider the problem of their asymptotic counting and effective random generation. We provide an asymptotic approximation of the number of both plain environments and closures of size n. Using the associated generating functions, we construct effective samplers for both classes of combinatorial structures. Finally, we discuss the related problem of asymptotic counting and random generation of closed environments and closures.
Cite as

Maciej Bendkowski and Pierre Lescanne. Counting Environments and Closures. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bendkowski_et_al:LIPIcs.FSCD.2018.11,
  author =	{Bendkowski, Maciej and Lescanne, Pierre},
  title =	{{Counting Environments and Closures}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{11:1--11:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.11},
  URN =		{urn:nbn:de:0030-drops-91817},
  doi =		{10.4230/LIPIcs.FSCD.2018.11},
  annote =	{Keywords: lambda-calculus, combinatorics, functional programming, mathematical analysis, complexity}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.12
Higher-Order Equational Pattern Anti-Unification

Authors: David M. Cerna and Temur Kutsia

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
We consider anti-unification for simply typed lambda terms in associative, commutative, and associative-commutative theories and develop a sound and complete algorithm which takes two lambda terms and computes their generalizations in the form of higher-order patterns. The problem is finitary: the minimal complete set of generalizations contains finitely many elements. We define the notion of optimal solution and investigate special fragments of the problem for which the optimal solution can be computed in linear or polynomial time.
Cite as

David M. Cerna and Temur Kutsia. Higher-Order Equational Pattern Anti-Unification. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{cerna_et_al:LIPIcs.FSCD.2018.12,
  author =	{Cerna, David M. and Kutsia, Temur},
  title =	{{Higher-Order Equational Pattern Anti-Unification}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{12:1--12:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.12},
  URN =		{urn:nbn:de:0030-drops-91826},
  doi =		{10.4230/LIPIcs.FSCD.2018.12},
  annote =	{Keywords: Simply typed lambda calculus, anti-unification, equational theories}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.13
Term Rewriting Characterisation of LOGSPACE for Finite and Infinite Data

Authors: Lukasz Czajka

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
We show that LOGSPACE is characterised by finite orthogonal tail-recursive cons-free constructor term rewriting systems, contributing to a line of research initiated by Neil Jones. We describe a LOGSPACE algorithm which computes constructor normal forms. This algorithm is used in the proof of our main result: that simple stream term rewriting systems characterise LOGSPACE-computable stream functions as defined by Ramyaa and Leivant. This result concerns characterising logarithmic-space computation on infinite streams by means of infinitary rewriting.
Cite as

Lukasz Czajka. Term Rewriting Characterisation of LOGSPACE for Finite and Infinite Data. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 13:1-13:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{czajka:LIPIcs.FSCD.2018.13,
  author =	{Czajka, Lukasz},
  title =	{{Term Rewriting Characterisation of LOGSPACE for Finite and Infinite Data}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{13:1--13:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.13},
  URN =		{urn:nbn:de:0030-drops-91831},
  doi =		{10.4230/LIPIcs.FSCD.2018.13},
  annote =	{Keywords: LOGSPACE, implicit complexity, term rewriting, infinitary rewriting, streams}
}
  • Refine by Author
  • 4 Kirchner, Hélène
  • 3 Middeldorp, Aart
  • 2 Kirchner, Claude
  • 2 Kutsia, Temur
  • 2 Licata, Daniel R.
  • Show More...

  • Refine by Classification
  • 12 Theory of computation → Rewrite systems
  • 7 Theory of computation → Equational logic and rewriting
  • 7 Theory of computation → Type theory
  • 4 Theory of computation → Lambda calculus
  • 3 Theory of computation → Automated reasoning
  • Show More...

  • Refine by Keyword
  • 3 confluence
  • 2 anti-unification
  • 2 equational theories
  • 2 functional programming
  • 2 homotopy type theory
  • Show More...

  • Refine by Type
  • 38 document

  • Refine by Publication Year
  • 34 2018
  • 1 1992
  • 1 2008
  • 1 2015
  • 1 2017

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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact