Follow

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

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: twitter.com/ionathanch/status/

@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
types.pl

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