Arthur Oliveira Vale

Ph.D Candidate in Computer Science

Yale University ‚óŹ arthur dot oliveiravale at yale dot edu

Broadly, my research interests span semantics, logic, theory of computation, programming language foundations and formal verification.

My current work seeks to use techniques that have been often used to provide the theory and semantics of programming languages to instead describe systems at a high-level of abstraction, in particular helping clarify the computational content of software engineering techniques, and with a focus on compositional semantic domains for large-scale system verification. My toolbox for this comprises the following tools:

Linear Logic
In order to have an expressive language for describing system interfaces I use linear logic types.
Denotational Semantics
For the sake of generality and in order to handle heterogenous systems the emphasis is often on semantics rather than syntax.
Intensional Semantics
An intensional semantics allows to give an operational account of these models. I use models such as game semantics, most commonly used to describe the fine-grained semantics of programming languages, to instead describe the coarse-grained behavior of systems.
Category Theory
I use category theory as the underlying theory of compositionality, often in the enriched setting in order to model behavior refinement.