BOOOKS
Conversation
Hit me up if you ever want talk verified compilation (Appel et al. also on my bookshelf)
1
1
Replying to
Oh lovely!
Trying to start getting my head around it. I'm wanting to try out type preserving compilation for Pikelet, at least up to ANF and Closure Conversion, using some of et al.'s work on doing it for dependent types!
Still need to figure out a nice way to set up Coq on my system... 😅
1
1
Oh, and yes, always up for a chat (if that wasn't obvious). I'm just always bad at getting around to organising stuff! Trying to get better though.
Let me know how it goes! Would be interesting to see an implementation and where the practical issues start to come up.
1
2
One thing I'm curious about is how well ANF plays with effectful code... I want to eventually do useful stuff with Pikelet, but I'm unsure if you need CPS for that... ie. because in ANF the order of control flow is not explicit? github.com/pikelet-lang/p
2
Show replies