  We propose a process calculus for modelling systems in the Internet of Things
paradigm. Our systems interact both with the physical environment, via sensors
and actuators, and with smart devices, via short-range and Internet channels.
The calculus is equipped with a standard notion of bisimilarity which is a
fully abstract characterisation of a well-known contextual equivalence. We use
our semantic proof-methods to prove run-time properties as well as system
equalities of non-trivial IoT systems.
