Brendan Zabarauskas on Twitter

Here is a bidirectional STλC type checker in string diagram Mercury, or something.

4

2

10

Looks a bit like the algebraic presentation of type checking in bentnib.org/posts/2015-04-

1

2

Replying to

and

Just went through the slides this afternoon with

. Super cool stuff and quite mind expanding - especially the tactic stuff! Have you experimented with this approach more since then?

Replying to

and

I've experimented a bit with more complex theories like Fomega. Keep meaning to write it up properly, but never getting round to it.

1

Conversation