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

2008

Minimality in a Linear Calculus with Iteration

Autores
Alves, S; Florido, M; Mackie, I; Sinot, FR;

Publicação
Electronic Notes in Theoretical Computer Science

Abstract
System L is a linear version of Gödel's System T, where the ?-calculus is replaced with a linear calculus; or alternatively a linear ?-calculus enriched with some constructs including an iterator. There is thus at the same time in this system a lot of freedom in reduction and a lot of information about resources, which makes it an ideal framework to start a fresh attempt at studying reduction strategies in ?-calculi. In particular, we show that call-by-need, the standard strategy of functional languages, can be defined directly and effectively in System L, and can be shown minimal among weak strategies.

2010

Linearity and iterator types for Gödel's System I

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

Publicação
Higher-Order and Symbolic Computation

Abstract
System L I is a linear ?-calculus with numbers and an iterator, which, although imposing linearity restrictions on terms, has all the computational power of Gödel's System I. System LI 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 LI. © 2010 Springer Science+Business Media, LLC.

2007

Linear recursive functions

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

Publicação
Rewriting, Computation and Proof: ESSAYS DEDICATED TO JEAN-PIERRE JOUANNAUD ON THE OCCASION OF HIS 60TH BIRTHDAY

Abstract
With the recent trend of analysing the process of computation through the linear logic looking glass, it is well understood that the ability to copy and erase data is essential in order to obtain a Turing-complete computation model. However, erasing and copying don't need to be explicitly included in Turing-complete computation models: in this paper we show that the class of partial recursive functions that are syntactically linear (that is, partial recursive functions where no argument is erased or copied) is Turing-complete.

2003

Linearization by program transformation

Autores
Alves, S; Florido, M;

Publicação
LOGIC BASED PROGRAM SYNTHESIS AND TRNSFORMATION

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.

2006

The power of linear functions

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

Publicação
COMPUTER SCIENCE LOGIC, PROCEEDINGS

Abstract
The linear lambda calculus is very weak in terms of expressive power: in particular, all functions terminate in linear time. In this paper we consider a simple extension with Booleans, natural numbers and a linear iterator. We show properties of this linear version of Godels's System T and study the class of functions that can be represented. Surprisingly, this linear calculus is extremely expressive: it is as powerful as System T.

2022

Linear Rank Intersection Types

Autores
Reis, F; Alves, S; Florido, M;

Publicação
28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France

Abstract
Non-idempotent intersection types provide quantitative information about typed programs, and have been used to obtain time and space complexity measures. Intersection type systems characterize termination, so restrictions need to be made in order to make typability decidable. One such restriction consists in using a notion of finite rank for the idempotent intersection types. In this work, we define a new notion of rank for the non-idempotent intersection types. We then define a novel type system and a type inference algorithm for the ?-calculus, using the new notion of rank 2. In the second part of this work, we extend the type system and the type inference algorithm to use the quantitative properties of the non-idempotent intersection types to infer quantitative information related to resource usage. © Fábio Reis, Sandra Alves, and Mário Florido.

  • 7
  • 8