search

evertedsphere / shorshe

freshly-fermented, dependently-typed mustard, with a substructural aftertaste
31 stars 0 forks source link

Tracking: choice of base core calculus #1

Open mrkgnao opened 4 years ago

mrkgnao commented 4 years ago

Currently the plan is to start with Oxide and then bolt some sort of dependent typing and effect tracking on top of that, but I'm open to alternatives.

xldenis commented 4 years ago

By Oxide do you mean the system exposed in https://arxiv.org/pdf/1903.00982.pdf ?

mrkgnao commented 4 years ago

Correct. I'm working from a more up-to-date version privately shared with me by @aatxe, though.

xldenis commented 4 years ago

Ah, well there's not much I can contribute until you have time to share your conclusions.

mrkgnao commented 4 years ago

Haha, that's fair. Sharing links to any resources you know of that might be relevant would be more than enough by way of contribution!

On Wed, Mar 18, 2020 at 4:24 PM Xavier Denis notifications@github.com wrote:

Ah, well there's not much I can contribute until you have time to share your conclusions.

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/mrkgnao/shorshe/issues/1#issuecomment-600554964, or unsubscribe https://github.com/notifications/unsubscribe-auth/ADMF33TDN6662K7E53WMDSDRICR5JANCNFSM4LLBPUNQ .