Post #1846822
2026-04-26 16:49 UTC
@carloangiuli @totbwf When I was inventing the cost-aware-logical-framework together with Yue Niu, one of my goals was to show that type theory WITH funext was a good place to study the difference between mergesort and insertion sort. I remember that certain people looked at me funny, like how can that possibly work... LOL
Replies (1)
-
@jonmsterling@mathstodon.xyz 2026-04-26 16:52
@carloangiuli @totbwf Today my main objection, by the way, to studying these things with type theory is that those terms really refer to in-place algorithms, period. I feel the "FP" version is too radical, and relies on theorems that are too difficult, in order to make any kind of connection to the in-place algorithms that make up the canon.