Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
About

About

Academic activities: 

 Academic Degrees:
  • PhD in Computer Science, University of Porto (2007)
  • MSc in Informatics, University of Porto (2001)     
  • Bsc in Computer Science, University of Porto (1999) 
 Research Topics:
  • Linearity, Lambda Calculus, Type Theory
  • Formal Specifications, Access Control Models

Interest
Topics
Details

Details

  • Name

    Sandra Alves
  • Role

    Senior Researcher
  • Since

    01st March 2015
Publications

2023

Quantitative Global Memory

Authors
Alves, S; Kesner, D; Ramos, M;

Publication
LOGIC, LANGUAGE, INFORMATION, AND COMPUTATION, WOLLIC 2023

Abstract
We show that recent approaches to static analysis based on quantitative typing systems can be extended to programming languages with global state. More precisely, we define a call-by-value language equipped with operations to access a global memory, together with a semantic model based on a (tight) multi-type system that captures exact measures of time and space related to evaluation of programs. We show that the type system is quantitatively sound and complete with respect to the operational semantics of the language.

2022

Report on women in logic 2020 & 2021

Authors
Alves, S; Kiefer, S; Sokolova, A;

Publication
ACM SIGLOG News

Abstract

2022

Quantitative Weak Linearisation

Authors
Alves, S; Ventura, D;

Publication
Theoretical Aspects of Computing - ICTAC 2022 - 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, Proceedings

Abstract
Weak linearisation was defined years ago through a static characterization of the intuitive notion of virtual redex, based on (legal) paths computed from the (syntactical) term tree. Weak-linear terms impose a linearity condition only on functions that are applied (consumed by reduction) and functions that are not applied (therefore persist in the term along any reduction) can be non-linear. This class of terms was shown to be strongly normalising with deciding typability in polynomial time. We revisit this notion through non-idempotent intersection types (also called quantitative types). By using an effective characterisation of minimal typings, based on the notion of tightness, we are able to distinguish between “consumed” and “persistent” term constructors, which allows us to define an expansion relation, between general ? -terms and weak-linear ? -terms, whilst preserving normal forms by reduction. © 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.

2022

Structural Rules and Algebraic Properties of Intersection Types

Authors
Alves, S; Florido, M;

Publication
Theoretical Aspects of Computing - ICTAC 2022 - 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, Proceedings

Abstract
In this paper we define several notions of term expansion, used to define terms with less sharing, but with the same computational properties of terms typable in an intersection type system. Expansion relates terms typed by associative, commutative and idempotent intersections with terms typed in the Curry type system and the relevant type system; terms typed by non-idempotent intersections with terms typed in the affine and linear type systems; and terms typed by non-idempotent and non-commutative intersections with terms typed in an ordered type system. © 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.

2022

Linear Rank Intersection Types

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

Publication
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.

Supervised
thesis

2023

Quantitative Types for Programming Languages

Author
Jorge Miguel Soares Ramos

Institution
UP-FCUP

2022

Quantitative Types for Programming Languages

Author
Jorge Miguel Soares Ramos

Institution
UP-FCUP

2022

Linear Rank Quantitative Types

Author
Fábio Daniel Martins Reis

Institution
UP-FCUP

2021

Typed Port-Graphs for Access Control Verification

Author
Jorge Paulino Iglésias

Institution
UP-FCUP

2021

PortGraphs for Access Control Verification

Author
Jorge Paulino Iglésias

Institution
UP-FCUP