Excited that "Is sized typing for Coq practical?", @ionchy's work, with Yufeng Li and me, has finally appeared in JFP:

In this work, we extended some past work on sized typing for CIC to Coq, extend Coq with sized typing with complete size inference, prove some stuff about size inference, study a set theoretic model, and analyze the performance of the implementation (which is bad).

You can find @ionchy's original summary on the bird site:

@ionchy @wilbowma who do you think you are? I bet you don't know more about sized types than the first author of the paper

Sign in to participate in the conversation

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.