I'm reading "Inductive Families Need Not Store Their Indices" by Edwin Brady, Conor McBride, and James McKinna; it seems to me like Coq's VM does half of the thing they suggest (it doesn't store inductive parameters), but the paper doesn't mention Coq's VM as an example (it does mention Coq's extraction though). Is there a paper that Coq's VM not storing inductive parameters is based on?

Jason Gross said:

Is there a paper that Coq's VM not storing inductive parameters is based on?

I'm afraid few people might be able to answer this at once (Benjamin Grégoire or @maximedenes typically).

@JasonGross I believe the paper is "On the Role of Type Decorations in the Calculus of Inductive Constructions" by Grégoire and Barras

Last updated: Dec 05 2023 at 06:01 UTC