For me it’s probably speech therapy and everything pertaining to that. I’m yet to encounter someone on here who is one apart from me (in training).
What about you?
For me it’s probably speech therapy and everything pertaining to that. I’m yet to encounter someone on here who is one apart from me (in training).
What about you?
Graded Modal Dependent Type Theory, but that’s mostly because only “dozens of” people know it exists.
What kind of grading do you give there? I guess the modal part is about the contexts for the type theory, but it has been some time I have looked into it.
I think “graded” in the name is there in contrast to “quantitative” type theory, which doesn’t have modalities/quantities at the type-level.
The “modal” is borrowed from modal logic. If you pick the correct semiring, you can recover linearity and affine-ity and the other substructural logic pieces.
The quantitative semiring I’ve been working with is
0, 1, ?, n, +, *, which I think will let me use static analysis to do very precise non-strictness and precise/early resource tracking/release. (But, my progress is so slow, that if this were an academic project, I don’t think I’d be getting any more grant funding.)