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
And there's an Agda formalization too! 7/7
• • •
Missing some Tweet in this thread? You can try to
force a refresh
