My paper's on arXiv
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!

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:
Still a bit buggy (not all of the stdlibs compiles) but examples work! (see README.v)

Show thread

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

Show thread

@nonphatic The abstract looks super interesting! 😀 I did something about this kind of problem a while ago, but it wasn't as general/practical as you announce it to be. Then Paco came along, making most people saying that it was all done… but you went further! 😀 I'm adding it to my reading list 😊 Thanks for sharing!

@MartinShadok I haven't heard of Paco before, do you have a link?



Paco is of more limited scope, for building coinductive proofs (Prop stuff).

Sign in to participate in the conversation

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!