boilnkettle

Logo

mail icon(λxy->y.x@up.pt) ramos miguel

ORCID iD icon0000-0002-1211-4270

github iconboilnkettle@github

Pure vs Effectful Morning Coffees

Hi, I’m Miguel! I recently completed my PhD in Computer Science at the Faculty of Sciences of the University of Porto, where my thesis focused on the quantitative analysis of higher-order computation with effects. My research interests lie at the intersection of programming languages, logic, and semantics. In particular, I study non-idempotent intersection types and their applications to the quantitative analysis of effectful higher-order programs, including features such as global state, exceptions, and pattern matching.

More recently, I have been investigating infinitary computation and the use of non-idempotent intersection types to characterize infinite computational behavior in both pure and effectful settings. Broadly speaking, my work aims to develop semantic and logical tools that provide a quantitative understanding of computation, bridging techniques from type theory, denotational semantics, and proof theory.

I am a researcher at LIACC and was a visiting researcher at IRIF from 2021 to 2025. My work has appeared in Mathematical Structures in Computer Science and in venues such as MFPS, APLAS, and WoLLIC. I have also been actively involved in teaching and academic service, including courses in Discrete Mathematics and Theory of Computation, reviewing for conferences such as FSCD, CSL, and MFPS, and the organization of scientific workshops.

Here is my dblp page, and here is some of my work:

Journal Papers

Conference Papers

Submitted/Under Review

Published

Workshops Papers

Program Committees

Peer-Reviewing

Presentations

PhD Thesis

MSc Thesis

Lately, I’ve also been working as a teaching assistant at FCUP and FEUP.

Teaching