My paper's on arXiv
arxiv.org/abs/1912.05601
It was rejected from CPP so I can't say anything fancy like "it's gonna be published at so-and-so!" or whatever but here it is!

Follow

I should say a little about this maybe
So there's some existing theory for sized types for CIC, which is the theory that Coq is based on, and I've extended it to cover a bit more of Gallina, which is Coq's specification language
Sized types are used for checking things like termination in Coq, in lieu of syntax-based guard predicates
I've implemented it in Coq's kernel here: github.com/ionathanch/coq/tree
Still a bit buggy (not all of the stdlibs compiles) but examples work! (see README.v)

My undergrad thesis is now ~~open source~~ github.com/PSTC/pstc-arxiv
I mean. It's on arXiv, so it was open source in the first place, but now it's actually accessible lmao

Show thread
Sign in to participate in the conversation
Cybrespace

cybrespace: the social hub of the information superhighway jack in to the mastodon fediverse today and surf the dataflow through our cybrepunk, slightly glitchy web portal support us on patreon or liberapay!