3 Search Results for "Lopes, Luís"

Document

DOI: 10.4230/LIPIcs.FSCD.2024.15

Adjoint Natural Deduction

Authors: Junyoung Jang, Sophia Roshal, Frank Pfenning, and Brigitte Pientka

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract

Adjoint logic is a general approach to combining multiple logics with different structural properties, including linear, affine, strict, and (ordinary) intuitionistic logics, where each proposition has an intrinsic mode of truth. It has been defined in the form of a sequent calculus because the central concept of independence is most clearly understood in this form, and because it permits a proof of cut elimination following standard techniques. In this paper we present a natural deduction formulation of adjoint logic and show how it is related to the sequent calculus. As a consequence, every provable proposition has a verification (sometimes called a long normal form). We also give a computational interpretation of adjoint logic in the form of a functional language and prove properties of computations that derive from the structure of modes, including freedom from garbage (for modes without weakening and contraction), strictness (for modes disallowing weakening), and erasure (based on a preorder between modes). Finally, we present a surprisingly subtle algorithm for type checking.

Cite as

Junyoung Jang, Sophia Roshal, Frank Pfenning, and Brigitte Pientka. Adjoint Natural Deduction. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 15:1-15:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{jang_et_al:LIPIcs.FSCD.2024.15,
  author =	{Jang, Junyoung and Roshal, Sophia and Pfenning, Frank and Pientka, Brigitte},
  title =	{{Adjoint Natural Deduction}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{15:1--15:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.15},
  URN =		{urn:nbn:de:0030-drops-203441},
  doi =		{10.4230/LIPIcs.FSCD.2024.15},
  annote =	{Keywords: Substructural Logic, Type Systems, Functional Programming}
}

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 Jang, Junyoung
1 Lopes, Luís
1 Lópes-Vallejo, Marisa
1 Martins, Francisco
Show More...

Refine by Classification
1 Theory of computation → Linear logic
1 Theory of computation → Proof theory

Refine by Keyword
1 Functional Programming
1 Global computing
1 Register file
1 Substructural Logic
1 Type Systems
Show More...

Refine by Type
3 document

Refine by Publication Year
1 2005
1 2006
1 2024