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
Publications

Publications by Sandra Alves

2021

A Graphical Framework for the Category-Based Metamodel for Access Control and Obligations

Authors
Alves, S; Iglésias, J;

Publication
CoRR

Abstract

2021

EVL: a typed functional language for event processing

Authors
Alves, S; Fernández, M; Ramos, M;

Publication
CoRR

Abstract

2016

The G-ACM Tool: using the Drools Rule Engine for Access Control Management

Authors
Sá, J; Alves, S; Broda, S;

Publication
CoRR

Abstract

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.

2024

Extending the Quantitative Pattern-Matching Paradigm

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

Publication
Programming Languages and Systems - 22nd Asian Symposium, APLAS 2024, Kyoto, Japan, October 22-24, 2024, Proceedings

Abstract
We show how (well-established) type systems based on non-idempotent intersection types can be extended to characterize termination properties of functional programming languages with pattern matching features. To model such programming languages, we use a (weak and closed) ?-calculus integrating a pattern matching mechanism on algebraic data types (ADTs). Remarkably, we also show that this language not only encodes Plotkin’s CBV and CBN ?-calculus as well as other subsuming frameworks, such as the bang-calculus, but can also be used to interpret the semantics of effectful languages with exceptions. After a thorough study of the untyped language, we introduce a type system based on intersection types, and we show through purely logical methods that the set of terminating terms of the language corresponds exactly to that of well-typed terms. Moreover, by considering non-idempotent intersection types, this characterization turns out to be quantitative, i.e. the size of the type derivation of a term t gives an upper bound for the number of evaluation steps from t to its normal form. © The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd. 2025.

2024

Proceedings 13th International Workshop on Developments in Computational Models

Authors
Alves, S; Mackie, I;

Publication
CoRR

Abstract

  • 8
  • 9