Type-Based Termination in Coq

Developing the Coq system
1

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 :frowning: (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

1 Like
2

Hello!

I am not aware of any currently active work on implementing type-based termination, but it is certainly an interesting topic.

The work of Jorge and his co-authors is probably the closest to something ready to be implemented for the full Coq system, but I believe there are still some open research questions. For example, fully defining the inference rules for terms with size annotations (not just typechecking them, but elaborating them from user syntax, defining the rules of unification on such terms, etc).

1 Like
3

As far as I know the semantics of sized types is not entirely understood.
An alternative is to use guarded type theory. Like sized types, guarded (cubical) type theory is available in agda. It would be very interesting to understand how to include this in Coq.