Skip to content

Commit

Permalink
Added the link to CEP to the extended abstract for CoqWorkshopITP24
Browse files Browse the repository at this point in the history
  • Loading branch information
thomas-lamiaux committed Aug 1, 2024
1 parent fa4c2d6 commit d0e4d8a
Showing 1 changed file with 5 additions and 5 deletions.
10 changes: 5 additions & 5 deletions ressources/extended_abstract_ITP24_CoqWorkshop.tex
Original file line number Diff line number Diff line change
Expand Up @@ -48,9 +48,9 @@ \section{Motivation}
Having a proper, clean and accessible documentation is one of the keys to the
success of software.
There are different forms of documentation: abstract and detailed documentation
like the reference manual~(\cite{Link_Coq_Ref}), course-shaped documentation like
Coq'Art~(\cite{bertot2013interactive}) or
Software Foundations~(\cite{Pierce:SF1}), or short action-oriented
like the reference manual~\cite{Link_Coq_Ref}, course-shaped documentation like
Coq'Art~\cite{bertot2013interactive} or
Software Foundations~\cite{Pierce:SF1}, or short action-oriented
documentation. We focus on the latter.
Short action-oriented documentation provides users with practical information on
specific features of Coq, so that users can learn and discover new
Expand All @@ -63,7 +63,7 @@ \section{Motivation}
Books like Coq'Art or Software Foundations provide nice pedagogical explanations
but target specific audiences, and are rather meant to be read from cover to
cover.
Moreover, they are not well suited to learn about specific features, to discover
Moreover, they are not well suited for learning about specific features, to discover
horizontally, and are not easy to keep updated.

Yet, short action-oriented documentation has many interests:
Expand Down Expand Up @@ -157,7 +157,7 @@ \section{Description of the project}
In the future, we hope to support a more standard and expressive format,
possibly using Alectryon~\cite{pit2020untangling}.

We are also writing a Coq Enhancement Proposal to discuss the project further with the community.
To further discuss the project, we have written a \href{https://github.com/coq/ceps/pull/91}{Coq Enhancement Proposal}.
We hope that, eventually, this documentation will become part of the website that will be created when renaming Coq to \emph{the Rocq Prover}.

\label{sect:bib}
Expand Down

0 comments on commit d0e4d8a

Please sign in to comment.