Thread by @mattecapu

#PaperADay🦆 today is kindly offered by @jonmsterling & collaborators:

arxiv.org/abs/2107.04663

1/n

I'm not going to run a long thread on this because the paper is very detailed and quite enjoyable to read, but here's some of the things I loved 2/n

The central idea of the paper is beautifully laid out at the beginning: use an open/closed pair of modalities on types to treat *intension* as structure on *extension*. So cool! 3/n

These modalities are generated by a certain predicate ¶_E which classifies the extensional phase. This seemed odd to me at first, but then this example made it so intuitive: 4/n

The other key idea of calf is to use model computational cost as a side-effect. Hence 'cost structures' become effectively algebras of a writer monad for a monoid of cost (e.g. running-time would be Nat) 5/n

So basically the extension modality 'forgets' step^c: 6/n

In the paper you find a full specification of 'calf', some categorical model theory (to prove it is non-degenerate), and most importantly, examples of verifying the running time of a program (such as an implementation Euclid's algorithm)
And there's an Agda formalization too! 7/7