Cookies
O website necessita de alguns cookies e outros recursos semelhantes para funcionar. Caso o permita, o INESC TEC irá utilizar cookies para recolher dados sobre as suas visitas, contribuindo, assim, para estatísticas agregadas que permitem melhorar o nosso serviço. Ver mais
Aceitar Rejeitar
  • Menu
Publicações

Publicações por Sandra Alves

2012

Proceedings 2nd International Workshop on Linearity

Autores
Alves, S; Mackie, I;

Publicação
Electron. Proc. Theor. Comput. Sci. - Electronic Proceedings in Theoretical Computer Science - EPTCS

Abstract

2007

The Power of Closed Reduction Strategies

Autores
Alves, S; Fernandez, M; Florido, M; Mackie, I;

Publicação
Electronic Notes in Theoretical Computer Science

Abstract
The computational efficiency of linear ?-calculi with iterators is evaluated using closed reduction strategies. The interaction between linearity and closed reduction and the computational power of linear systems with and without closed reduction is analyzed. A linear version of Gödel's System T with closed reductions is defined to analyze the computational power of linear systems. Closed reduction strategies in the ?-calculus restrict the reduction rules since closed reduction strategies can take place when certain terms are closed and do not contain free variables. Closed reduction strategies impose strong constraints on the application of reduction rules. Closed reduction strategies can simulate call-by-name and call-by-value evaluations in the ?-calculus. Linear ?-calculus with iterators can be efficiently analyzed by relaxing the constraints on the construction of iterator terms.

2007

Iterator types

Autores
Alves, S; Fernndez, M; Florido, M; Mackie, I;

Publicação
Foundations of Software Science and Computational Structures, Proceedings

Abstract
System L is a linear A-calculus with numbers and an iterator, which, although imposing linearity restrictions on terms, has all the computational power of Godel's System T. System C owes its power to two features: the use of a closed reduction strategy (which permits the construction of an iterator on an open function, but only iterates the function after it becomes closed), and the use of a liberal typing rule for iterators based on iterative types. In this paper, we study these new types, and show how they relate to intersection types. We also give a sound and complete type reconstruction algorithm for System L.

2011

Linearity and Recursion in a Typed Lambda-Calculus

Autores
Alves, S; Fernandez, M; Florido, M; Mackie, I;

Publicação
PPDP 11 - PROCEEDINGS OF THE 2011 SYMPOSIUM ON PRINCIPLES AND PRACTICES OF DECLARATIVE PROGRAMMING

Abstract
We show that the full PCF language can be encoded in L-rec, a syntactically linear lambda-calculus extended with numbers, pairs, and an unbounded recursor that preserves the syntactic linearity of the calculus. We give call-by-name and call-by-value evaluation strategies and discuss implementation techniques for L-rec, exploiting its linearity.

2002

Type inference using constraint handling rules

Autores
Alves, S; Florido, M;

Publicação
Electronic Notes in Theoretical Computer Science

Abstract
In this paper we present an implementation of the general system for type inference algorithms HM(X), using Prolog and Constraint Handling Rules. In our implementation the difference between the general aspects of the type inference algorithms and the constraint resolution module becomes clearer, when compared to other implementations of the same systems, usually made in a functional programming language. In the constraint module, solving equality constraints, here implemented by Prolog unification, is completely separated from constraint simplification, which is made by a solver implemented in CHR for each system. CHR rules become a clear and natural way of specifying the simplification mechanism. © 2002 Publishd by Elsevier Science B.V.

2005

Weak linearization of the lambda calculus

Autores
Alves, S; Florido, M;

Publicação
THEORETICAL COMPUTER SCIENCE

Abstract
We identify a restricted class of terms of the lambda calculus, here called weak linear, that includes the linear lambda-terms keeping their good properties of strong normalization, non-duplicating reductions and typability in polynomial time. The advantage of this class over the linear lambda-calculus is the possibility of transforming general terms into weak linear terms with the same normal form. We present such transformation and prove its correctness by showing that it preserves normal forms.

  • 6
  • 8