Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Docs on module system should cite papers by Jacek Chrząszcz etc. #14717

Open
Blaisorblade opened this issue Jul 28, 2021 · 1 comment
Open
Labels
kind: documentation Additions or improvement to documentation.

Comments

@Blaisorblade
Copy link
Contributor

Description of the problem

@robbertkrebbers were discussing whether the Coq's module system design is documented by academic literature; no citations are given in the manual, but it seems such papers exist (https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/ANSSI.20and.20experimental.20SProp/near/247459612) and might be somewhat relevant to the current system.

@Blaisorblade Blaisorblade added the kind: documentation Additions or improvement to documentation. label Jul 28, 2021
@herbelin
Copy link
Member

The docs on the module system were first written by Jacek Chrząszcz iirc. That would indeed be good to add a reference to his papers, as well as a reference to Judicaël Courant and Élie Soubiran's PhD theses. Do you think you'd be willing to propose a PR?

@Zimmi48 Zimmi48 added this to Fixing in User documentation Sep 7, 2021
@Zimmi48 Zimmi48 moved this from Fixing to Writing in User documentation Sep 7, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: documentation Additions or improvement to documentation.
Projects
Status: Writing
Development

No branches or pull requests

2 participants