Follow

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!

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)

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!

@nonphatic

@MartinShadok

plv.mpi-sws.org/paco/

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

Sign in to participate in the conversation
Cybrespace

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.