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
Tópicos
de interesse
Detalhes

Detalhes

  • Nome

    Renato Jorge Neves
  • Cargo

    Investigador Sénior
  • Desde

    01 janeiro 2014
003
Publicações

2023

A Complete V-Equational System for Graded lambda-Calculus

Autores
Dahlqvist, F; Neves, R;

Publicação
CoRR

Abstract

2023

The syntactic side of autonomous categories enriched over generalised metric spaces

Autores
Dahlqvist, F; Neves, R;

Publicação
Log. Methods Comput. Sci.

Abstract

2023

THE SYNTACTIC SIDE OF AUTONOMOUS CATEGORIES ENRICHED OVER GENERALISED METRIC SPACES

Autores
Dahlqvist, F; Neves, R;

Publicação
LOGICAL METHODS IN COMPUTER SCIENCE

Abstract
Programs with a continuous state space or that interact with physical processes often require notions of equivalence going beyond the standard binary setting in which equivalence either holds or does not hold. In this paper we explore the idea of equivalence taking values in a quantale V, which covers the cases of (in)equations and (ultra)metric equations among others.Our main result is the introduction of a V-equational deductive system for linear lambda-calculus together with a proof that it is sound and complete. In fact we go further than this, by showing that linear lambda-theories based on this V-equational system form a category equivalent to a category of autonomous categories enriched over 'generalised metric spaces'. If we instantiate this result to inequations, we get an equivalence with autonomous categories enriched over partial orders. In the case of (ultra)metric equations, we get an equivalence with autonomous categories enriched over (ultra)metric spaces. Additionally, we show that this syntax-semantics correspondence extends to the affine setting.We use our results to develop examples of inequational and metric equational systems for higher-order programming in the setting of real-time, probabilistic, and quantum computing.

2022

An Internal Language for Categories Enriched over Generalised Metric Spaces

Autores
Dahlqvist, F; Neves, R;

Publicação
30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference).

Abstract
Programs with a continuous state space or that interact with physical processes often require notions of equivalence going beyond the standard binary setting in which equivalence either holds or does not hold. In this paper we explore the idea of equivalence taking values in a quantale V, which covers the cases of (in)equations and (ultra)metric equations among others. Our main result is the introduction of a V-equational deductive system for linear ?-calculus together with a proof that it is sound and complete (in fact, an internal language) for a class of enriched autonomous categories. In the case of inequations, we get an internal language for autonomous categories enriched over partial orders. In the case of (ultra)metric equations, we get an internal language for autonomous categories enriched over (ultra)metric spaces. We use our results to obtain examples of inequational and metric equational systems for higher-order programs that contain real-time and probabilistic behaviour.

2021

An Internal Language for Categories Enriched over Generalised Metric Spaces

Autores
Dahlqvist, F; Neves, R;

Publicação
CoRR

Abstract

Teses
supervisionadas

2022

Approximate Equivalence for Hybrid Programs

Autor
Juliana Patrício de Souza

Instituição
UM