Elektrine
EN
Log in Register
Paige Chat Timeline Communities Gallery Videos Email DNS VPN Uptime Kairo
Back to Timeline
Remote

jules

@hegeliantaco@mathstodon.xyz
mastodon 4.6.4
  • Open on mathstodon.xyz

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

0 Followers
0 Following
3 Posts
Joined September 23, 2023

Posts

Open post
hegeliantaco
jules @hegeliantaco@mathstodon.xyz · May 01, 2026
jules
@hegeliantaco@mathstodon.xyz

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

mathstodon.xyz
Replying to @hegeliantaco@mathstodon.xyz
@zanzi@mathstodon.xyz @julesh@mathstodon.xyz Also it might be worth fixing this typo in the last linear rule for coverings
1
2
0
0
Open post
hegeliantaco
jules @hegeliantaco@mathstodon.xyz · May 01, 2026
jules
@hegeliantaco@mathstodon.xyz

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

mathstodon.xyz
Replying to @zanzi@mathstodon.xyz
@zanzi@mathstodon.xyz @julesh@mathstodon.xyz another thing that might be interesting further work is generating the algorithm and typechecking witnesses together in one go from a set of colored inference rules. You claim in the paper that the rules yield an algorithm and I’ve been able to perform the translation by hand, but a proof and mechanization of this transformation would be nice.
2
2
0
0
Open post
hegeliantaco
jules @hegeliantaco@mathstodon.xyz · May 01, 2026
jules
@hegeliantaco@mathstodon.xyz

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

mathstodon.xyz

@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

1
2
3
0

Remote instance

mathstodon.xyz
Open on original server
313k7r1n3
Elektrine

Tor hidden service

elekhj7afj4qnrr4yd3bkzslsyo5jgfxw3orgjkhlcxifueodybyiiad.onion

Platform

  • Email
  • Chat
  • Timeline
  • Communities
  • VPN
  • DNS

Company

  • About
  • Contact
  • FAQ

Legal

  • Terms of Service
  • Privacy Policy
  • Warrant Canary
  • Lite (no JS)
  • VPN Policy
  • Source code

Support

  • support@elektrine.com
  • Report Security Issue
Mail client setup IMAP mail.elektrine.com:993 POP3 mail.elektrine.com:995 SMTP mail.elektrine.com:465
© 2026 Elektrine. All rights reserved. Server: 22:55:49 UTC