Carol Mak

Carol Mak

DPhil in Programming Languages

Posts by Collection

portfolio

publications

talks

Simply-typed Differential and Resource Lambda-Calculus

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.

Higher-Order Probability Theory on Interval Domain

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.

teaching