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
  • Cluster

    Informática
  • Cargo

    Investigador Sénior
  • Desde

    01 janeiro 2014
003
Publicações

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.

2020

Implementing Hybrid Semantics: From Functional to Imperative

Autores
Goncharov, S; Neves, R; Proença, J;

Publicação
Theoretical Aspects of Computing - ICTAC 2020 - 17th International Colloquium, Macau, China, November 30 - December 4, 2020, Proceedings

Abstract

2020

Implementing Hybrid Semantics: From Functional to Imperative

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

Publicação
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.

2019

An Adequate While-Language for Hybrid Computation

Autores
Goncharov, S; Neves, R;

Publicação
PROCEEDINGS OF THE 21ST INTERNATIONAL SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING (PPDP 2019)

Abstract

2019

Limits in Categories of Vietoris Coalgebras

Autores
Hofmann, D; Neves, R; Nora, P;

Publicação
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE

Abstract