Arthur Oliveira Vale

Ph.D Candidate in Computer Science

Yale University ‚óŹ

My research interests span logic, type theory, semantics, programming language foundations and formal verification.

I'm currently working on semantic domains for large-scale system verification. I'm using models of linear logic to build a denotational specification language. A game-semantics description of the specification language provides an operational description of the model. The model is stateful but has no explicit state. This is part of an effort to understand CAL and CCAL (the framework used by CertiKOS) through a more semantical lens while at the same time giving a more compositional and generic interface for CAL and CCAL.