Lindsey Kuper on Nostr: ❤️ Interpretability ❤️ We think that what makes our diagrams useful and ...
❤️ Interpretability ❤️
We think that what makes our diagrams useful and interesting is their interpretability into various semantic domains: into types, into terms, into proofs relating types and terms. For the paper's case study on verified logical clocks, we wrote a series of interpreters for diagrams, culminating in an interpreter that *produces proofs about clocks*!
I'm really proud of this work, and there's lots more to do. We'll keep at it.
We think that what makes our diagrams useful and interesting is their interpretability into various semantic domains: into types, into terms, into proofs relating types and terms. For the paper's case study on verified logical clocks, we wrote a series of interpreters for diagrams, culminating in an interpreter that *produces proofs about clocks*!
I'm really proud of this work, and there's lots more to do. We'll keep at it.