The workshop brought together researchers who are applying logic, category theory and set theory to the study of the abstract syntax and semantics of computer languages and systems for symbolic computation and proof.