diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 38ad33dc6008a9b944c4cbde62ae79efa1be00d9..930c7dec4b29a630829fb1d12d46371188b873de 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -1,3 +1,8 @@
+(** This file contains the examples from the paper:
+
+Interactive Proofs in Higher-Order Concurrent Separation Logic
+Robbert Krebbers, Amin Timany and Lars Birkedal
+POPL 2017 *)
 From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export hoare.