Is there currently any work done towards implementing some form of type-based termination in Coq’s kernel, like sized types [0]? From searching the GitHub repo I’ve found a mention of sized types from 2010 about Jorge Sacchini’s work [1] and a comment about Sacchini’s PhD on sized types [2], but no further discussions lately. From [3] I see that Sacchini’s done further work with linear sized types in 2014, and I found some slides from 2015 on well-founded sized types [4] as well as a draft paper last archived in 2016 [5], so maybe there’s further issue of which type theory to implement, but I haven’t seen any further discussion about it, and that last paper was never published it seems. I also found Sacchini’s implementations of what seem to be well-founded sized types on his GitHub [6], last pushed to in 2017, although the commits were made in 2015. Aside from Sacchini’s work, in the discussion from 2010 there also seems to be work by Andreas Abel on type-based termination. There just doesn’t seem to be any existing efforts in implementing sized types in Coq, though.

Sorry for all the non-linky links! Apparently as a new user I can only post two links (FIXED)

[0] https://github.com/coq/coq/wiki/CoqTerminationDiscussion#sized

[1] https://github.com/coq/coq/wiki/CRADT20100202

[2] https://github.com/coq/coq/issues/5530#issuecomment-337553933

[3] https://dblp.org/pers/hd/s/Sacchini:Jorge_Luis

[4] http://cs.ioc.ee/types15/slides/sacchini-slides.pdf

[5] http://web.archive.org/web/20160606143713/http://www.qatar.cmu.edu/~sacchini/well-founded/well-founded.pdf

[6] https://github.com/jsacchini