Interested in mathematics, philosophy, computer science, and the real movement to abolish the present state of things I am not Jules Hedges, you can find them at https://mathstodon.xyz/@julesh For my non-computer science/math related thoughts checkout @dialecticalrussell.bsky.social @analytichegel on Twitter
Interested in mathematics, philosophy, computer science, and the real movement to abolish the present state of things I am not Jules Hedges, you can find them at @julesh@mathstodon.xyz For my non-computer science/math related thoughts checkout @dialecticalrussell.bsky.social @analytichegel on Twitter
Posts
Interested in mathematics, philosophy, computer science, and the real movement to abolish the present state of things I am not Jules Hedges, you can find them at https://mathstodon.xyz/@julesh For my non-computer science/math related thoughts checkout @dialecticalrussell.bsky.social @analytichegel on Twitter
Interested in mathematics, philosophy, computer science, and the real movement to abolish the present state of things I am not Jules Hedges, you can find them at https://mathstodon.xyz/@julesh For my non-computer science/math related thoughts checkout @dialecticalrussell.bsky.social @analytichegel on Twitter
@zanzi@mathstodon.xyz @julesh@mathstodon.xyz have you (or anyone else) made progress on the "further work" section of "Canonical bidirectional typechecking"? I've been writing an implementation of the ideas of the paper and Agda and was thinking doing the embedding of λ-calculi, and was curious if this would be novel or if you've already done this