Cite POPL19 SProp paper

Close #10242

3 files changed, 26 insertions, 4 deletions

diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst
index 9a9ec78edc..9acdd18b89 100644
--- a/doc/sphinx/addendum/sprop.rst
+++ b/doc/sphinx/addendum/sprop.rst
@@ -9,9 +9,11 @@ SProp (proof irrelevant propositions)
 
 This section describes the extension of |Coq| with definitionally
 proof irrelevant propositions (types in the sort :math:`\SProp`, also
-known as strict propositions). Using :math:`\SProp` may be prevented
-by passing ``-disallow-sprop`` to the |Coq| program or using
-:flag:`Allow StrictProp`.
+known as strict propositions) as described in
+:cite:`Gilbert:POPL2019`.
+
+Using :math:`\SProp` may be prevented by passing ``-disallow-sprop``
+to the |Coq| program or using :flag:`Allow StrictProp`.
 
 .. flag:: Allow StrictProp
    :name: Allow StrictProp
diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib
index 6fec3ef00c..db089df395 100644
--- a/doc/sphinx/biblio.bib
+++ b/doc/sphinx/biblio.bib
@@ -222,6 +222,25 @@ s},
   year        = {1890}
 }
 
+@article{Gilbert:POPL2019,
+ author = {Gilbert, Ga\"{e}tan and Cockx, Jesper and Sozeau, Matthieu and Tabareau, Nicolas},
+ title = {{Definitional Proof Irrelevance Without K}},
+ journal = {Proc. ACM Program. Lang.},
+ issue_date = {January 2019},
+ volume = {3},
+ number = {POPL},
+ year = {2019},
+ issn = {2475-1421},
+ pages = {3:1--3:28},
+ articleno = {3},
+ numpages = {28},
+ url = {http://doi.acm.org/10.1145/3290316},
+ acmid = {3290316},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {proof assistants, proof irrelevance, type theory},
+}
+
 @InProceedings{Gim94,
   author      = {E. Gim\'enez},
   booktitle   = {Types'94 : Types for Proofs and Programs},
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 6410620b40..f659438674 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -49,7 +49,8 @@ The sort :math:`\SProp` is like :math:`\Prop` but the propositions in
 equal). Objects of type :math:`\SProp` are called strict propositions.
 :math:`\SProp` is rejected except when using the compiler option
 ``-allow-sprop``. See :ref:`sprop` for information about using
-:math:`\SProp`.
+:math:`\SProp`, and :cite:`Gilbert:POPL2019` for meta theoretical
+considerations.
 
 The sort :math:`\Set` intends to be the type of small sets. This includes data
 types such as booleans and naturals, but also products, subsets, and