Advertisement · 728 × 90

Posts by David Corfield

Preview
A unifying type-theory for higher-order (amortized) cost analysis | Proceedings of the ACM on Programming Languages This paper presents λ-amor, a new type-theoretic framework for amortized cost analysis of higher-order functional programs and shows that existing type systems for cost analysis can be embedded in it....

Yes, the work was done while the others were on the ARIA project. Their goal was to provide a graded monad understanding of dl.acm.org/doi/10.1145/..., and related work. I'm not working on that now, but what we did is being written up and has nearly reached first draft phase.

3 months ago 2 0 0 0

Then set-indexed families of Psh(M), as Riley notes. But then this is Psh(M+), where the + adjoins an initial object.

3 months ago 0 0 0 0
Post image Post image

Suddenly, we seemed very close to this section of Riley's thesis, but we didn't push things far in this direction:

3 months ago 1 0 1 0
The Quantum Monadology in Schreiber

My interest derived at first from the role of linear HoTT in the Sati-Schreiber program: ncatlab.org/schreiber/sh....

But then, oddly, working with Rajani and Orchard on a type theory for amortization, we found ourselves looking at models which were families of copresheaves on an ordered monoid.

3 months ago 2 0 1 0
Mitchell Riley in nLab

Bunched dependent types, like Mitchell Riley: ncatlab.org/nlab/show/Mi...?

3 months ago 1 0 1 0

I hope you find inspiration and an outlet. Nothing has come close for me to the thrill of writing on the n-Category Cafe c. 2006-2013.

5 months ago 2 0 0 0

Linked to "The unreasonable power of the lifting property in elementary mathematics"? Penultimate reference on 'nLab: factorization system':
ncatlab.org/nlab/show/fa...

6 months ago 3 0 0 0
Post image

The CW01 mentioned in the footnote is Caccamo & Winskel: A Higher-Order Calculus for Categories
www.brics.dk/RS/01/27/BRI.... It has rules such as

10 months ago 2 0 1 0
Advertisement
Post image

Maybe via ends/coends and this?:
arxiv.org/abs/1501.02503

10 months ago 1 0 1 0