We express reactive programs in COQ using data-flow synchronous operators. Following LUID-SYNCHROME approach, synchronous static constraints are here expressed using dependent types. Hence, our analysis of synchrony is here
directly performed by COQtypechecker.