## Portfolio item number 1

Short description of portfolio item number 1

Short description of portfolio item number 1

Short description of portfolio item number 2

** Published:**

The differential λ-calculus augments the λ-calculus with differential operators that mimic the rules of the standard differential calculus. The extension, and an equivalent calculus, the resource λ-calculus, give expression to resource usage of a computation. Bucciarelli et al. have shown that cartesian closed differential categories are models of simply-typed differential λ-theories. This project proves the converse, which is a form of completeness: given a typed differential λ-theory, we construct the “smallest” category in which one can soundly model the theory. Moreover, we show that, under reasonable assumptions, differential λ-theory is the internal language of cartesian closed differential category. Finally, we present the relational model as a cartesian closed differential category and show that it is in- complete.

** Published:**

This talk presented a correct and adequate model for probabilistic PCF extended with partial real numbers using omega quasi-Borel spaces and interval integration monad, with future work in proving the model is also fully abstract.

Undergraduate course, *St. Catherine's College, University of Oxford*, 2017

Carol taught first year St. Catherine’s College students Discrete Mathematics from 2017 to 2019.

Undergraduate course, *St. Catherine's College, University of Oxford*, 2017

Carol taught second and third St. Catherine’s College students Lambda Calculus and Types from 2017 to 2020.