Search Results

Documents authored by Pimentel, Elaine

Document
DOI: 10.4230/DagRep.14.8.1
Proof Representations: From Theory to Applications (Dagstuhl Seminar 24341)

Authors: Anupam Das, Elaine Pimentel, Lutz Straßburger, and Robin Martinot

Published in: Dagstuhl Reports, Volume 14, Issue 8 (2025)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 24341 "Proof Representations: From Theory to Applications". Proof theory is the study of formal proofs as mathematical objects in their own right. The subject has enjoyed continued attention among computer scientists in particular due to its significance for formalization, metalogic, and automation. In recent decades there has been a surge of interest on the representations of formal proofs themselves. The outcomes of these investigations have been remarkable, in particular extending the scope of structural proof theory to novel and richer settings: Richer line structures (e.g. hypersequents, nested sequents, labelled sequents) have resulted in a uniform treatment of standard modal logics, streamlining their metatheory and providing new tools for metalogical problems. Richer proof structures (e.g., cyclic proofs, annotated systems, infinitely branching proofs) have significantly advanced our understanding of fixed points and (co)induction. Indeed, we are now seeing many of these previously disjoint techniques being combined to push the boundaries of proof theoretic approaches to computational logic. Graphical proof representations (e.g., proof nets, atomic flows, combinatorial proofs) originating from "linear" logics, now not only comprise a well-behaved computational model for resource-sensitive reasoning, but also provide an impressively uniform treatment for logics across the board. In fact, we are now seeing many of these previously disjoint techniques being combined to push the boundaries of proof theoretic approaches to computational logic, which has produced deep and fruitful cross-fertilizations between programming languages and proof theory. Arguably, the most well-known is the Curry-Howard correspondence ("propositions-as-types") where (functional) programs correspond to formal proofs and their execution to normalization. A complementary tradition, proof-search-as-computation ("propositions-as-processes"), instead interprets (logic) programs to formulas and their execution to proof search. The goal of this Dagstuhl Seminar was twofold. First and foremost, we aimed to bring together theorists and practitioners exploiting proof representations to identify new directions of application and, simultaneously, distill new theoretical directions from problems "in the wild". At the same time, this seminar was intended to expose the interface between the proof-normalization and proof-search traditions by probing proof representations from both directions.
Cite as

Anupam Das, Elaine Pimentel, Lutz Straßburger, and Robin Martinot. Proof Representations: From Theory to Applications (Dagstuhl Seminar 24341). In Dagstuhl Reports, Volume 14, Issue 8, pp. 1-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{das_et_al:DagRep.14.8.1,
  author =	{Das, Anupam and Pimentel, Elaine and Stra{\ss}burger, Lutz and Martinot, Robin},
  title =	{{Proof Representations: From Theory to Applications (Dagstuhl Seminar 24341)}},
  pages =	{1--23},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2025},
  volume =	{14},
  number =	{8},
  editor =	{Das, Anupam and Pimentel, Elaine and Stra{\ss}burger, Lutz and Martinot, Robin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.8.1},
  URN =		{urn:nbn:de:0030-drops-229975},
  doi =		{10.4230/DagRep.14.8.1},
  annote =	{Keywords: proof theory, proof calculi, computational interpretations, proof semantics, dynamic operators}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.STACS.2025
LIPIcs, Volume 327, STACS 2025, Complete Volume

Authors: Olaf Beyersdorff, Michał Pilipczuk, Elaine Pimentel, and Nguyễn Kim Thắng

Published in: LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Abstract
LIPIcs, Volume 327, STACS 2025, Complete Volume
Cite as

42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 1-1388, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Proceedings{beyersdorff_et_al:LIPIcs.STACS.2025,
  title =	{{LIPIcs, Volume 327, STACS 2025, Complete Volume}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{1--1388},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-365-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{327},
  editor =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025},
  URN =		{urn:nbn:de:0030-drops-229403},
  doi =		{10.4230/LIPIcs.STACS.2025},
  annote =	{Keywords: LIPIcs, Volume 327, STACS 2025, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.STACS.2025.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Olaf Beyersdorff, Michał Pilipczuk, Elaine Pimentel, and Nguyễn Kim Thắng

Published in: LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

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

42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 0:i-0:xxvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.STACS.2025.0,
  author =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine and Thắng, Nguy\~{ê}n Kim},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{0:i--0:xxvi},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-365-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{327},
  editor =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025.0},
  URN =		{urn:nbn:de:0030-drops-229393},
  doi =		{10.4230/LIPIcs.STACS.2025.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2025.4
Playing with Modalities (Invited Talk)

Authors: Elaine Pimentel, Carlos Olarte, Timo Lang, Robert Freiman, and Christian G. Fermüller

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
In this work, we will explore modalities through dialogical game lenses. Games provide a powerful tool for bridging the gap between intended and formal semantics, often offering a more conceptually natural approach to logic than traditional model-theoretic semantics. We begin by exploring substructural calculi from a game semantic perspective, driven by intuitions about resource-consciousness and, more specifically, cost-sensitive reasoning. The game comes into full swing as we introduce cost labels to assumptions and a corresponding budget. Different proofs of the same end-sequent are interpreted as strategies for a player to defend a claim, which vary in cost. This leads to a labelled calculus, which can be viewed as a fragment of subexponential linear logic. We conclude this first part with a discussion of cut-admissibility for the proposed system. In the second part, we show that our games offer an interesting insight also into modal logics. More precisely, we will focus on the modal logic PNL, characterised by Kripke frames with two types of disjoint and symmetric reachability relations. This framework is motivated by the study of group polarisation, where the opinions or beliefs of individuals within a group become more extreme or polarised after interaction. Our approach to reasoning about group polarisation is based on PNL and highlights a different aspect of formal reasoning about the corresponding models - using games and proof systems. We conclude by outlining potential directions for future research.
Cite as

Elaine Pimentel, Carlos Olarte, Timo Lang, Robert Freiman, and Christian G. Fermüller. Playing with Modalities (Invited Talk). In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 4:1-4:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{pimentel_et_al:LIPIcs.CSL.2025.4,
  author =	{Pimentel, Elaine and Olarte, Carlos and Lang, Timo and Freiman, Robert and Ferm\"{u}ller, Christian G.},
  title =	{{Playing with Modalities}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{4:1--4:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.4},
  URN =		{urn:nbn:de:0030-drops-227614},
  doi =		{10.4230/LIPIcs.CSL.2025.4},
  annote =	{Keywords: Linear logic, modal logic, proof theory, game semantics}
}
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

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

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.FSCD.2021.3
Process-As-Formula Interpretation: A Substructural Multimodal View (Invited Talk)

Authors: Elaine Pimentel, Carlos Olarte, and Vivek Nigam

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
In this survey, we show how the processes-as-formulas interpretation, where computations and proof-search are strongly connected, can be used to specify different concurrent behaviors as logical theories. The proposed interpretation is parametric and modular, and it faithfully captures behaviors such as: Linear and spatial computations, epistemic state of agents, and preferences in concurrent systems. The key for this modularity is the incorporation of multimodalities in a resource aware logic, together with the ability of quantifying on such modalities. We achieve tight adequacy theorems by relying on a focusing discipline that allows for controlling the proof search process.
Cite as

Elaine Pimentel, Carlos Olarte, and Vivek Nigam. Process-As-Formula Interpretation: A Substructural Multimodal View (Invited Talk). In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{pimentel_et_al:LIPIcs.FSCD.2021.3,
  author =	{Pimentel, Elaine and Olarte, Carlos and Nigam, Vivek},
  title =	{{Process-As-Formula Interpretation: A Substructural Multimodal View}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{3:1--3:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.3},
  URN =		{urn:nbn:de:0030-drops-142414},
  doi =		{10.4230/LIPIcs.FSCD.2021.3},
  annote =	{Keywords: Linear logic, proof theory, process calculi}
}
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact