Full syntax of λλ (from the paper):

   e ::= v | x | input(p) 
   | let x = e1 in e2
   | (e1, e2)
   | unpack e1 as (x1, x2) in e2
   | phase(θ, e)
   | split(r, e)
   | unitary(U, (e1, e2))
   | output(p) <- e1; e2
   v ::= r ↓ ℝ | p ↓ Port | U ↓ Unitary | ()
   τ ::= ℝ | Port | Opt | Unitary | Unit |(τ1 * τ2)

The second λ is subscripted. As footnote 1 in the paper says:

> Pronounced “lambda lambda”. One λ refers to the λ-calculus and the other refers to an optical wavelength.