43 Search Results for "Pimentel, Elaine"

Volume

LIPIcs, Volume 252

31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

CSL 2023, February 13-16, 2023, Warsaw, Poland

Editors: Bartek Klin and Elaine Pimentel

Document
Invited Talk
DOI: 10.4230/LIPIcs.CALCO.2023.3
A Tour on Ecumenical Systems (Invited Talk)

Authors: Elaine Pimentel and Luiz Carlos Pereira

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

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

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

Copy BibTex To Clipboard

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

Authors: Bartek Klin and Elaine Pimentel

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

Abstract
LIPIcs, Volume 252, CSL 2023, Complete Volume
Cite as

Bartek Klin and Elaine Pimentel. LIPIcs, Volume 252, CSL 2023, Complete Volume. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 1-718, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Proceedings{klin_et_al:LIPIcs.CSL.2023,
  title =	{{LIPIcs, Volume 252, CSL 2023, Complete Volume}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{1--718},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023},
  URN =		{urn:nbn:de:0030-drops-174603},
  doi =		{10.4230/LIPIcs.CSL.2023},
  annote =	{Keywords: LIPIcs, Volume 252, CSL 2023, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.CSL.2023.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Bartek Klin and Elaine Pimentel

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

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

Bartek Klin and Elaine Pimentel. Front Matter, Table of Contents, Preface, Conference Organization. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 0:i-0:xviii, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{klin_et_al:LIPIcs.CSL.2023.0,
  author =	{Klin, Bartek and Pimentel, Elaine},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{0:i--0:xviii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.0},
  URN =		{urn:nbn:de:0030-drops-174614},
  doi =		{10.4230/LIPIcs.CSL.2023.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2023.1
Asymptotic Rewriting (Invited Talk)

Authors: Claudia Faggian

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

Abstract
Rewriting is a foundation for the operational theory of programming languages. The process of rewriting describes the computation of a result (typically, a normal form), with lambda-calculus being the paradigmatic example for rewriting as an abstract form of program execution. Taking this view, the execution of a program is formalized as a specific evaluation strategy, while the general rewriting theory allows for program transformations, optimizations, parallel/distributed implementations, and provides a base on which to reason about program equivalence. In this talk, we discuss what happens when the notion of termination is asymptotic, that is, the result of computation appears as a limit, as opposed to reaching a normal form in a finite number of steps. - Example 1. A natural example is probabilistic computation. A probabilistic program P is a stochastic model generating a distribution over all possible outputs of P. Even if the termination probability is 1 (almost sure termination), that degree of certitude is typically not reached in a finite number of steps, but as a limit. A standard example is a term M that reduces to either a normal form or M itself, with equal probability 1/2. After n steps, M is in normal form with probability 1/2 + 1/(2²) + … + 1/(2ⁿ). Only at the limit this computation terminates with probability 1. - Example 2. Infinitary lambda-calculi (where the limits are infinitary terms such as Böhm trees), streams, algebraic rewriting systems, effectful computation (e.g. computation with outputs), quantum lambda-calculi provide several other relevant examples. Instances of asymptotic computation are quite diverse, and moreover the specific syntax of each system may be rather complex. In the talk, we present asymptotic rewriting in a way which is independent of the specific details of each calculus, and we provide a toolkit of proof-techniques which are of general application. To do so, we rely on Quantitative Abstract Rewriting System [Claudia Faggian, 2022; Claudia Faggian and Giulio Guerrieri, 2022], building on work by Ariola and Blom [Ariola and Blom, 2002], which enrich with quantitative information the theory of Abstract Rewriting Systems (ARS) (see e.g. [Terese, 2003] or [Baader and Nipkow, 1998]). ARS are indeed the core of finitary rewriting, capturing the common substratum of rewriting theory and term transformation, independently from the particular structure of the objects. It seems then natural to seek a similar foundation for asymptotic computation. The issue is that the arguments relying on finitary termination do not transfer, in general, to limits (a game changer being that asymptotic termination does not provide a well-founded order): we need to develope an opportune formalization and suitable proof techniques. The goal is then to identify and develop methods which only rely on the asymptotic argument - abstracting from structure specific to a setting - and so will apply to any concrete instance. For example, in infinitary lambda calculus, the limit is usually a (possibly infinite) limit term, while in probabilistic lambda calculus, the limit is a distribution over (finite) terms. The former is concerned with the depth of the redexes, the latter with the probability of reaching a result. The abstract notions of limit and of normalization subsumes both, and so abstract results apply to either setting.
Cite as

Claudia Faggian. Asymptotic Rewriting (Invited Talk). In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 1:1-1:2, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{faggian:LIPIcs.CSL.2023.1,
  author =	{Faggian, Claudia},
  title =	{{Asymptotic Rewriting}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{1:1--1:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.1},
  URN =		{urn:nbn:de:0030-drops-174621},
  doi =		{10.4230/LIPIcs.CSL.2023.1},
  annote =	{Keywords: rewriting, probabilistic rewriting, confluence, strategies, asymptotic normalization, lambda calculus}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2023.2
Inductive Inference and Epistemic Modal Logic (Invited Talk)

Authors: Nina Gierasimczuk

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

Abstract
This paper is concerned with a link between inductive inference and dynamic epistemic logic. The bridge was first introduced in [Gierasimczuk, 2009; Nina Gierasimczuk, 2009; Gierasimczuk, 2010]. We present a synthetic view on subsequent contributions: inductive truth-tracking properties of belief revision policies seen as belief upgrade methods; topological interpretation and characterisation of inductive inference; discussion of the adequacy of the topological semantics of modal logic for characterising inductive inference. We briefly present the topological Dynamic Logic for Learning Theory. Finally, we discuss several surprising results obtained in computational inductive inference that challenge the usual understanding of certainty, and of rational inquiry as consistent and conservative learning.
Cite as

Nina Gierasimczuk. Inductive Inference and Epistemic Modal Logic (Invited Talk). In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 2:1-2:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{gierasimczuk:LIPIcs.CSL.2023.2,
  author =	{Gierasimczuk, Nina},
  title =	{{Inductive Inference and Epistemic Modal Logic}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{2:1--2:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.2},
  URN =		{urn:nbn:de:0030-drops-174634},
  doi =		{10.4230/LIPIcs.CSL.2023.2},
  annote =	{Keywords: modal logic, dynamic epistemic logic, inductive inference, topological semantics, computational learning theory, finite identifiability, identifiability in the limit}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2023.3
A Positive Perspective on Term Representation (Invited Talk)

Authors: Dale Miller and Jui-Hsuan Wu

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

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

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

Copy BibTex To Clipboard

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

Authors: Davide Sangiorgi

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

Abstract
We outline an attempt at transporting the well-known theory of enhancements for the coinduction proof method, widely used on behavioural relations such as bisimilarity, onto the realms of inductive behaviour relations, i.e., relations defined from inductive observables, and discuss relevant literature.
Cite as

Davide Sangiorgi. Enhanced Induction in Behavioural Relations (Invited Talk). In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 4:1-4:6, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{sangiorgi:LIPIcs.CSL.2023.4,
  author =	{Sangiorgi, Davide},
  title =	{{Enhanced Induction in Behavioural Relations}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{4:1--4:6},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.4},
  URN =		{urn:nbn:de:0030-drops-174658},
  doi =		{10.4230/LIPIcs.CSL.2023.4},
  annote =	{Keywords: coinduction, induction, semantics, behavioural relations}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.5
A Cyclic Proof System for Full Computation Tree Logic

Authors: Bahareh Afshari, Graham E. Leigh, and Guillermo Menéndez Turata

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

Abstract
Full Computation Tree Logic, commonly denoted CTL*, is the extension of Linear Temporal Logic LTL by path quantification for reasoning about branching time. In contrast to traditional Computation Tree Logic CTL, the path quantifiers are not bound to specific linear modalities, resulting in a more expressive language. We present a sound and complete hypersequent calculus for CTL*. The proof system is cyclic in the sense that proofs are finite derivation trees with back-edges. A syntactic success condition on non-axiomatic leaves guarantees soundness. Completeness is established by relating cyclic proofs to a natural ill-founded sequent calculus for the logic.
Cite as

Bahareh Afshari, Graham E. Leigh, and Guillermo Menéndez Turata. A Cyclic Proof System for Full Computation Tree Logic. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 5:1-5:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{afshari_et_al:LIPIcs.CSL.2023.5,
  author =	{Afshari, Bahareh and Leigh, Graham E. and Men\'{e}ndez Turata, Guillermo},
  title =	{{A Cyclic Proof System for Full Computation Tree Logic}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{5:1--5:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.5},
  URN =		{urn:nbn:de:0030-drops-174664},
  doi =		{10.4230/LIPIcs.CSL.2023.5},
  annote =	{Keywords: Full computation tree logic, Hypersequent calculus, Cyclic proofs}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.6
Functorial String Diagrams for Reverse-Mode Automatic Differentiation

Authors: Mario Alvarez-Picallo, Dan Ghica, David Sprunger, and Fabio Zanasi

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

Abstract
We formulate a reverse-mode automatic differentiation (RAD) algorithm for (applied) simply typed lambda calculus in the style of Pearlmutter and Siskind [Barak A. Pearlmutter and Jeffrey Mark Siskind, 2008], using the graphical formalism of string diagrams. Thanks to string diagram rewriting, we are able to formally prove for the first time the soundness of such an algorithm. Our approach requires developing a calculus of string diagrams with hierarchical features in the spirit of functorial boxes, in order to model closed monoidal (and cartesian closed) structure. To give an efficient yet principled implementation of the RAD algorithm, we use foliations of our hierarchical string diagrams.
Cite as

Mario Alvarez-Picallo, Dan Ghica, David Sprunger, and Fabio Zanasi. Functorial String Diagrams for Reverse-Mode Automatic Differentiation. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 6:1-6:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{alvarezpicallo_et_al:LIPIcs.CSL.2023.6,
  author =	{Alvarez-Picallo, Mario and Ghica, Dan and Sprunger, David and Zanasi, Fabio},
  title =	{{Functorial String Diagrams for Reverse-Mode Automatic Differentiation}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{6:1--6:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.6},
  URN =		{urn:nbn:de:0030-drops-174674},
  doi =		{10.4230/LIPIcs.CSL.2023.6},
  annote =	{Keywords: string diagrams, automatic differentiation, hierarchical hypergraphs}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.7
A Lattice-Theoretical View of Strategy Iteration

Authors: Paolo Baldan, Richard Eggert, Barbara König, and Tommaso Padoan

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

Abstract
Strategy iteration is a technique frequently used for two-player games in order to determine the winner or compute payoffs, but to the best of our knowledge no general framework for strategy iteration has been considered. Inspired by previous work on simple stochastic games, we propose a general formalisation of strategy iteration for solving least fixpoint equations over a suitable class of complete lattices, based on MV-chains. We devise algorithms that can be used for non-expansive fixpoint functions represented as so-called min- respectively max-decompositions. Correspondingly, we develop two different techniques: strategy iteration from above, which has to solve the problem that iteration might reach a fixpoint that is not the least, and from below, which is algorithmically simpler, but requires a more involved correctness argument. We apply our method to solve energy games and compute behavioural metrics for probabilistic automata.
Cite as

Paolo Baldan, Richard Eggert, Barbara König, and Tommaso Padoan. A Lattice-Theoretical View of Strategy Iteration. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 7:1-7:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{baldan_et_al:LIPIcs.CSL.2023.7,
  author =	{Baldan, Paolo and Eggert, Richard and K\"{o}nig, Barbara and Padoan, Tommaso},
  title =	{{A Lattice-Theoretical View of Strategy Iteration}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{7:1--7:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.7},
  URN =		{urn:nbn:de:0030-drops-174680},
  doi =		{10.4230/LIPIcs.CSL.2023.7},
  annote =	{Keywords: games, strategy iteration, fixpoints, energy games, behavioural metrics}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.8
Reductions in Higher-Order Rewriting and Their Equivalence

Authors: Pablo Barenbaum and Eduardo Bonelli

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

Abstract
Proof terms are syntactic expressions that represent computations in term rewriting. They were introduced by Meseguer and exploited by van Oostrom and de Vrijer to study equivalence of reductions in (left-linear) first-order term rewriting systems. We study the problem of extending the notion of proof term to higher-order rewriting, which generalizes the first-order setting by allowing terms with binders and higher-order substitution. In previous works that devise proof terms for higher-order rewriting, such as Bruggink’s, it has been noted that the challenge lies in reconciling composition of proof terms and higher-order substitution (β-equivalence). This led Bruggink to reject "nested" composition, other than at the outermost level. In this paper, we propose a notion of higher-order proof term we dub rewrites that supports nested composition. We then define two notions of equivalence on rewrites, namely permutation equivalence and projection equivalence, and show that they coincide.
Cite as

Pablo Barenbaum and Eduardo Bonelli. Reductions in Higher-Order Rewriting and Their Equivalence. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 8:1-8:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{barenbaum_et_al:LIPIcs.CSL.2023.8,
  author =	{Barenbaum, Pablo and Bonelli, Eduardo},
  title =	{{Reductions in Higher-Order Rewriting and Their Equivalence}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.8},
  URN =		{urn:nbn:de:0030-drops-174694},
  doi =		{10.4230/LIPIcs.CSL.2023.8},
  annote =	{Keywords: Term Rewriting, Higher-Order Rewriting, Proof terms, Equivalence of Computations}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.9
Proofs and Refutations for Intuitionistic and Second-Order Logic

Authors: Pablo Barenbaum and Teodoro Freund

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

Abstract
The λ^{PRK}-calculus is a typed λ-calculus that exploits the duality between the notions of proof and refutation to provide a computational interpretation for classical propositional logic. In this work, we extend λ^{PRK} to encompass classical second-order logic, by incorporating parametric polymorphism and existential types. The system is shown to enjoy good computational properties, such as type preservation, confluence, and strong normalization, which is established by means of a reducibility argument. We identify a syntactic restriction on proofs that characterizes exactly the intuitionistic fragment of second-order λ^{PRK}, and we study canonicity results.
Cite as

Pablo Barenbaum and Teodoro Freund. Proofs and Refutations for Intuitionistic and Second-Order Logic. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 9:1-9:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{barenbaum_et_al:LIPIcs.CSL.2023.9,
  author =	{Barenbaum, Pablo and Freund, Teodoro},
  title =	{{Proofs and Refutations for Intuitionistic and Second-Order Logic}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{9:1--9:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.9},
  URN =		{urn:nbn:de:0030-drops-174707},
  doi =		{10.4230/LIPIcs.CSL.2023.9},
  annote =	{Keywords: lambda-calculus, propositions-as-types, classical logic, proof normalization}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.10
The Functional Machine Calculus II: Semantics

Authors: Chris Barrett, Willem Heijltjes, and Guy McCusker

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

Abstract
The Functional Machine Calculus (FMC), recently introduced by the second author, is a generalization of the lambda-calculus which may faithfully encode the effects of higher-order mutable store, I/O and probabilistic/non-deterministic input. Significantly, it remains confluent and can be simply typed in the presence of these effects. In this paper, we explore the denotational semantics of the FMC. We have three main contributions: first, we argue that its syntax - in which both effects and lambda-calculus are realised using the same syntactic constructs - is semantically natural, corresponding closely to the structure of a Scott-style domain theoretic semantics. Second, we show that simple types confer strong normalization by extending Gandy’s proof for the lambda-calculus, including a small simplification of the technique. Finally, we show that the typed FMC (without considering the specifics of encoded effects), modulo an appropriate equational theory, is a complete language for Cartesian closed categories.
Cite as

Chris Barrett, Willem Heijltjes, and Guy McCusker. The Functional Machine Calculus II: Semantics. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 10:1-10:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{barrett_et_al:LIPIcs.CSL.2023.10,
  author =	{Barrett, Chris and Heijltjes, Willem and McCusker, Guy},
  title =	{{The Functional Machine Calculus II: Semantics}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{10:1--10:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.10},
  URN =		{urn:nbn:de:0030-drops-174716},
  doi =		{10.4230/LIPIcs.CSL.2023.10},
  annote =	{Keywords: lambda-calculus, computational effects, denotational semantics, strong normalization}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.11
Degree Spectra, and Relative Acceptability of Notations

Authors: Nikolay Bazhenov and Dariusz Kalociński

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

Abstract
We investigate the interplay between the degree spectrum of a computable relation R on the computable structure (ω, <), i.e., natural numbers with the standard order, and the computability of the successor, relativized to that relation, in all computable copies of the structure - the property we dub successor’s recoverability. In computable structure theory, this property is used to show that of all possible Turing degrees that could belong to the spectrum of R (namely, of all Δ₂ degrees), in fact only the computably enumerable degrees are contained in the spectrum. Interestingly, successor’s recoverability (in the unrelativized form) appears also in philosophy of computing where it is used to distinguish between acceptable and deviant encodings (notations) of natural numbers. Since Shapiro’s notations are rarely seen through the lens of computable structure theory, we first lay the elementary conceptual groundwork to understand notations in terms of computable structures and show how results pertinent to the former can fundamentally inform our understanding of the latter. Secondly, we prove a new result which shows that for a large class of computable relations (satisfying a certain effectiveness condition), having all c.e. degrees as a spectrum implies that the successor is recoverable from the relation. The recoverability of successor may be otherwise seen as relativized acceptability of every notation for the structure. We end with remarks about connections of our result to relative computable categoricity and to a similar direction pursued by Matthew Harrison-Trainor in [Harrison-Trainor, 2018], and with an open question.
Cite as

Nikolay Bazhenov and Dariusz Kalociński. Degree Spectra, and Relative Acceptability of Notations. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 11:1-11:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bazhenov_et_al:LIPIcs.CSL.2023.11,
  author =	{Bazhenov, Nikolay and Kaloci\'{n}ski, Dariusz},
  title =	{{Degree Spectra, and Relative Acceptability of Notations}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{11:1--11:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.11},
  URN =		{urn:nbn:de:0030-drops-174725},
  doi =		{10.4230/LIPIcs.CSL.2023.11},
  annote =	{Keywords: Computable structure theory, Degree spectra, \omega-type order, C.e. degrees, \Delta₂ degrees, Acceptable notation, Successor, Learnability}
}
  • Refine by Author
  • 4 Pimentel, Elaine
  • 2 Barenbaum, Pablo
  • 2 Ghica, Dan
  • 2 Jaakkola, Reijo
  • 2 Klin, Bartek
  • Show More...

  • Refine by Classification
  • 8 Theory of computation → Proof theory
  • 7 Theory of computation → Type theory
  • 6 Theory of computation → Modal and temporal logics
  • 5 Theory of computation → Equational logic and rewriting
  • 4 Theory of computation → Complexity theory and logic
  • Show More...

  • Refine by Keyword
  • 3 complexity
  • 2 Agda
  • 2 Cyclic proofs
  • 2 classical logic
  • 2 coalgebra
  • Show More...

  • Refine by Type
  • 42 document
  • 1 volume

  • Refine by Publication Year
  • 42 2023
  • 1 2021

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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact