About

I am a postdoc in the Laboratory for Foundations of Computer Science at the University of Edinburgh working with Sam Lindley on the Effect Handler Oriented Programming project. Between October 2018 and October 2022 I was a PhD student at the University of Oxford, working with Sam Staton, and also a member of Balliol College. Previously, I obtained an MSc in Computer Science from Oxford and a BA from Cambridge. My research interests are semantics of programming languages, types, category theory, logic and verification. For my PhD thesis, I worked on models of programming languages built using logical relations and sheaves.

Publications

• Concrete categories and higher-order recursion (With applications including probability, differentiability, and full abstraction).
  Cristina Matache, Sean Moss, Sam Staton. LICS 2022. [slides]
  
• Recursion and sequentiality in categories of sheaves.
  Cristina Matache, Sean Moss, Sam Staton. FSCD 2021.
  
• A sound and complete logic for algebraic effects.
  Cristina Matache, Sam Staton. FoSSaCS 2019.
  
• Programming and proving with classical types.
  Cristina Matache, Victor B. F. Gomes, Dominic P. Mulligan. APLAS 2017. [slides]
  
• The λμ calculus.
  Cristina Matache, Victor B. F. Gomes, Dominic P. Mulligan.
  Archive of Formal Proofs, 2017.

Theses

• Concrete sheaf models of higher-order recursion.   PhD thesis.
  University of Oxford, Department of Computer Science.
• Program equivalence for algebraic effects via modalities.   Master's thesis.
  University of Oxford, Department of Computer Science, September 2018.
  (updated version)
• Formalisation of the λμ^T calculus in Isabelle/HOL.   Bachelor's thesis.
  University of Cambridge, Computer Laboratory, June 2017.

Misc

• A unified treatment of concrete sheaf models for higher-order recursion.   Talk at the Chocola meeting, 31 March 2022.
• Recursion and sequentiality in categories of sheaves.   Logic and Semantics seminar at Aarhus University.
• A sound and complete logic for algebraic effects.   Seminar talk at Bath, Birmingham and UCL.
• Formalisation of the λμ^T calculus in Isabelle/HOL.   Poster at ICFP 2017.

Teaching

• 2020--2021: Stipendiary Lecturer at Jesus College.
• Hilary term 2020: class tutor and marker for Lambda Calculus and Types.
• Michaelmas term 2019: tutoring Discrete Mathematics for first year undergraduates.