3 Search Results for "Lopes, Luís"

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
DOI: 10.4230/DagSemProc.05081.6
MiKO---Mikado Koncurrent Objects

Authors: Francisco Martins, Liliana Salvador, Vasco T. Vasconcelos, and Luís Lopes

Published in: Dagstuhl Seminar Proceedings, Volume 5081, Foundations of Global Computing (2006)

Abstract
The motivation for the Mikado migration model is to provide programming constructs for controlling code mobility that are as independent as possible from the particular programming language used to program the code. The main idea is to regard a domain (or site, or locality), where mobile code may enter or exit, as a membrane enclosing running processes, and offering services that have to be called for entering or exiting the domain. MiKO---Mikado Koncurrent Objects is a particular instance of this model, where the membrane is explicitly split in two parts: the methods defining the interface, and a process part describing the data for, and the behavior of, the interface. The talk presents the syntax, operational semantics, and type system of MiKO, together with an example. It concludes by briefly mentioning the implementation of a language based on the calculus.
Cite as

Francisco Martins, Liliana Salvador, Vasco T. Vasconcelos, and Luís Lopes. MiKO---Mikado Koncurrent Objects. In Foundations of Global Computing. Dagstuhl Seminar Proceedings, Volume 5081, pp. 1-43, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{martins_et_al:DagSemProc.05081.6,
  author =	{Martins, Francisco and Salvador, Liliana and Vasconcelos, Vasco T. and Lopes, Lu{\'\i}s},
  title =	{{MiKO---Mikado Koncurrent Objects}},
  booktitle =	{Foundations of Global Computing},
  pages =	{1--43},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5081},
  editor =	{Jos\'{e} Luiz Fiadeiro and Ugo Montanari and Martin Wirsing},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05081.6},
  URN =		{urn:nbn:de:0030-drops-3014},
  doi =		{10.4230/DagSemProc.05081.6},
  annote =	{Keywords: Global computing, code migration, administrative domains, process calculus}
}
Document
DOI: 10.4230/DagSemProc.05141.4
Compiler-Driven Power Optimizations in the Register File of Processor-Based Systems

Authors: José Luis Ayala and Marisa Lópes-Vallejo

Published in: Dagstuhl Seminar Proceedings, Volume 5141, Power-aware Computing Systems (2005)

Abstract
The complexity of the register file is currently one of the main factors on determining the cycle time of high performance wide-issue microprocessors due to its access time and size. Both parameters are directly related to the number of read and write ports of the register file and can be managed from a code compilation-level. Therefore, it is a priority goal to reduce this complexity in order to allow the efficient implementation of complex superscalar machines. This work presents a modified register assignment and a banked architecture which efficiently reduce the number of required ports. Also, the effect of the loop unrollling optimization performed by the compiler is analyzed and several power-efficient modifications to this mechanism are proposed. Both register assignment and loop unrolling mechanisms are modified to improve the energy savings while avoiding a hard performance impact.
Cite as

José Luis Ayala and Marisa Lópes-Vallejo. Compiler-Driven Power Optimizations in the Register File of Processor-Based Systems. In Power-aware Computing Systems. Dagstuhl Seminar Proceedings, Volume 5141, pp. 1-17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{ayala_et_al:DagSemProc.05141.4,
  author =	{Ayala, Jos\'{e} Luis and L\'{o}pes-Vallejo, Marisa},
  title =	{{Compiler-Driven Power Optimizations in the Register File of Processor-Based Systems}},
  booktitle =	{Power-aware Computing Systems},
  pages =	{1--17},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{5141},
  editor =	{Luca Benini and Ulrich Kremer and Christian W. Probst and Peter Schelkens},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05141.4},
  URN =		{urn:nbn:de:0030-drops-3053},
  doi =		{10.4230/DagSemProc.05141.4},
  annote =	{Keywords: Register file, power reduction, compiler optimization, loop unrolling, banked architecture}
}
  • Refine by Author
  • 1 Ayala, José Luis
  • 1 Lopes, Luís
  • 1 Lópes-Vallejo, Marisa
  • 1 Martins, Francisco
  • 1 Pereira, Luiz Carlos
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Modal and temporal logics
  • 1 Theory of computation → Proof theory
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 1 Global computing
  • 1 Intuitionistic logic
  • 1 Register file
  • 1 administrative domains
  • 1 banked architecture
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2005
  • 1 2006
  • 1 2023

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