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 work employs techniques from programming language theory and semantics to describe systems at a high-level of abstraction. This helps clarify the computational content of systems engineering techniques and is beneficial in the compositional verification of large-scale systems. My toolbox for this comprises the following tools:
- Linear Logic
- Provides an expressive setting to define interface 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.
