Arthur Oliveira Vale
Ph.D Candidate in Computer Science
Yale University ● email@example.com
Broadly, my research interests span semantics, logic, theory of computation, programming language foundations and formal verification.
My current work seeks to clarify the computational content of software engineering techniques, 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.