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!



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

Sign in to participate in the conversation

Cybrespace is an instance of Mastodon, a social network based on open web protocols and free, open-source software. It is decentralized like e-mail.