Stream: Coq devs & plugin devs

Topic: History


view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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: Oct 16 2021 at 03:02 UTC