Jason Gross (May 17 2020 at 03:23): Jason Gross (May 17 2020 at 03:23):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?
Hugo Herbelin (May 18 2020 at 10:22):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).
Maxime Dénès (May 18 2020 at 11:44):@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: Jun 05 2023 at 11:01 UTC