diff --git a/iris_heap_lang/lib/logatom_lock.v b/iris_heap_lang/lib/logatom_lock.v
index 40dbfa74e2089a722d5875b4dd78f487ee1a51f1..d9556ceb3c910956276ba07ef751f4d263962163 100644
--- a/iris_heap_lang/lib/logatom_lock.v
+++ b/iris_heap_lang/lib/logatom_lock.v
@@ -1,5 +1,5 @@
 (** A TaDA-style logically atomic specification for a lock, derived for an
-    arbitrary implementation of the lock interfacne. The opposite direction
+    arbitrary implementation of the lock interface. The opposite direction
     could also be derived rather easily (modulo a later in the [acquire] postcondition
     or a restriction to timeless lock invariants), as shown in the TaDA paper.