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

I'm a PhD student, under the MAP-i doctoral programme, whose theme is logics and calculi for cyber–physical components.

I'm mainly interested in the foundations of cyber physical systems; coalgebras, proof theory and institutional theory; also, in a myriad of logics, but particularly in modal logics.

I participated in project Mondrian and I'm currently a member of the project Dalí.

Google scholar

DBLP

Contacts : nevrenato at di dot uminho dot pt

My Website gathers all the information about my academical activities.

Interest
Topics
Details

Details

  • Name

    Renato Jorge Neves
  • Cluster

    Computer Science
  • Role

    Senior Researcher
  • Since

    01st January 2014
003
Publications

2023

A Complete V-Equational System for Graded lambda-Calculus

Authors
Dahlqvist, F; Neves, R;

Publication
CoRR

Abstract

2022

An Internal Language for Categories Enriched over Generalised Metric Spaces

Authors
Dahlqvist, F; Neves, R;

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

2022

The syntactic dual of autonomous categories enriched over generalised metric spaces

Authors
Dahlqvist, F; Neves, R;

Publication
CoRR

Abstract

2021

An Internal Language for Categories Enriched over Generalised Metric Spaces

Authors
Dahlqvist, F; Neves, R;

Publication
CoRR

Abstract

2020

Implementing Hybrid Semantics: From Functional to Imperative

Authors
Goncharov, S; Neves, R; Proenca, J;

Publication
THEORETICAL ASPECTS OF COMPUTING, ICTAC 2020

Abstract
Hybrid programs combine digital control with differential equations, and naturally appear in a wide range of application domains, from biology and control theory to real-time software engineering. The entanglement of discrete and continuous behaviour inherent to such programs goes beyond the established computer science foundations, producing challenges related to e.g. infinite iteration and combination of hybrid behaviour with other effects. A systematic treatment of hybridness as a dedicated computational effect has emerged recently. In particular, a generic idealized functional language HYBCORE with a sound and adequate operational semantics has been proposed. The latter semantics however did not provide hints to implementing HYBCORE as a runnable language, suitable for hybrid system simulation (e.g. the semantics features rules with uncountably many premises). We introduce an imperative counterpart of HYBCORE, whose semantics is simpler and runnable, and yet intimately related with the semantics of HYBCORE at the level of hybrid monads. We then establish a corresponding soundness and adequacy theorem. To attest that the resulting semantics can serve as a firm basis for the implementation of typical tools of programming oriented to the hybrid domain, we present a web-based prototype implementation to evaluate and inspect hybrid programs, in the spirit of GHCI for HASKELL and UTOP for OCAML. The major asset of our implementation is that it formally follows the operational semantic rules.

Supervised
thesis

2022

Approximate Equivalence for Hybrid Programs

Author
Juliana Patrício de Souza

Institution
UM