Coq Call 2024 02 12

• February 12th (Monday!), 4pm UTC+2 (Paris time zone offset)
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• Proposition to talk about primitive projections: which positive/negative simulations, which algebraic presentations, which optimized representations, which control of reduction, which disambiguation of names? (see Zulip, Hugo 10-30 minutes) [postponed]
• Proposition otherwise to talk about reduction strategies, if no other urgencies (CEP #85, Hugo):
  • do we want fixpoint/cofixpoint refolding in cbv and lazy and, if yes, or if yes at least optionally, how to implement it?
    • by modifying the reduction machines?
      • à la simpl, by computing an optimal refolding for each unfolded constant
      • à la cbn, by incorporating possible refolding in the evaluation stack and choosing the optimal one
    • by telling how to refold (co)fixpoint in the Fix/CoFix node when such refolding exist (drawback: we would refold only to the closest surrounding constant; on the other side, this is what we are doing already for mutual fix; it is also somehow a canonical refolding)?
  • do we try to unify the features of simpl/cbn/cbv/lazy?
    • adding support for selecting a pattern in all of them, and, if yes, with which syntax:
      • a possibility would be to reuse the with syntax of auto, e.g. lazy pattern with [constants], and documenting the syntax lazy [constants] as a shortcut for lazy pattern with [constants]
    • adding support for beta, iota, zeta, delta flags and [ ... ] lists to simpl (even if forbidding beta and iota in simpl looks a bit useless)
  • we may also allow constructors in the transparency state to control iota-reduction, the same way as we can already control primitive projections reduction by name of projection?
  • a syntax to combine databases of constants to unfold, see CEP #84
  • removal of the user access to hnf?

Roles

• Chairman: Nicolas Tabareau
• Secretary:

Notes