Renato Neves

Postdoctoral researcher at UCL, Univ. of Minho, & INESC TEC


nev(first name) // nev(first name)

Research Topics (Cyber-Physical and Quantum)

One of my main foci is the development of reasoning tools, syntax, and semantics for cyber-physical systems, a highly interesting class of devices that intertwines different aspects of analysis, control theory, and computer science. Cyber-physical systems are a main ingredient in the 21st century's technology, but even so they are still remarkably difficult to design and analyse in a systematic and disciplined way.

My other main focus is quantum computing. Specifically, the development of suitable (quantitative) semantics that, among other things, tracks the use of computational resources by a quantum program. Quantum computing is a computational paradigm with the potential to provide remarkable speedups to certain families of computational problems. However, quantum programs are still highly susceptible to noise (correlated with the use of certain computational resources) which hinders their application to real-world problems.

My collaborators and I have been tackling the challenges underlying cyber-physical and quantum computing by applying and advancing different mathematical frameworks. In particular,

Selected Publications

Implementing Hybrid Semantics (with Sergey Goncharov and José Proença). ICTAC'20. [link]
An Adequate While-Language for Hybrid Computation (with Sergey Goncharov). PPDP'19. [link]
Hybrid Programs. PhD Thesis. [link]
A Semantics for Hybrid Iteration (with Sergey Goncharov and Julian Jakob). CONCUR'18. [link]
Limits in Categories of Vietoris Coalgebras (with Dirk Hofmann and Pedro Nora). MSCS'18. [link]
Languages and Models for Hybrid Automata: A coalgebraic perspective (with Luís Barbosa). TCS'17. [link]

Google Scholar, DBLP, ResearchGate.

Recent (co)supervisions

Vítor F. (PhD) Timing constraints in quantum progr. languages (supervision with Benoît Valiron, funded by FCT). In progress.
Liu Ai (PhD) Quantum transition syst. & component-based progr. Finished in May 2020.
Eduardo B. (MSc) Implementation of a component based lambda-calculus in Agda. In progress.
Paulo R. (MSc) Implementation of a Kleene-like theorem for hybrid automata. In progress.
Vítor F. (MSc) Typing systems and timing constraints for quantum processes. Finished in December 2019.

Current Funded Projects

TimedQ Timing constraints in quantum progr. languages (supervision of a FCT-funded, PhD student) (2020-2024).
VetssQ Quantitative equational theories and quantitative program semantics (2020-2021).
Klee Coalgebraic Modeling and Analysis for Computational Synthetic Biology (2018 - 2021).
DaVinci Distributed Architectures: Variability and Interaction for Cyber-Physical Systems (2018 - 2021).

Recent Teaching Activities

Quantum Comp. MAP-i For PhD students; fundamental concepts and formal methods in Quantum Comp. (2020-21)
Quantum Logic For MSc students; logics, semantics, and calculi for Quantum Comp. (2019-20, 2020-21)
Arch. and Calculi For MSc students; core concepts of concurrency and cyber-physical systems (2019-20, 2020-21)
CyPhy. Comp. For PhD students; program semantics and analysis for cyber-physical systems (2019-20)
Program calculus For BSc students; program semantics and calculi (2018-19, 2019-20)
Inf. Labs I For 1st-year BSc students; a first introduction to programming (2019-20)

A full listing of my publications, teaching activities, and (co)supervisions (both in the cyber-physical and quantum domains) is available in my cv.