The growing success of wireless ad hoc networks and portable hardware devices presents many interesting problems to software engineers. Particular, coordination is a challenging task, since ad hoc networks are characterized by very opportunistic connections and rapidly changing topologies. This paper presents the formal semantics of a coordination model, called PeerSpaces, designed to overcome the shortcomings of traditional coordination models when used in ad hoc networks. The PeerSpaces model does not assume any centralized structure. Instead, it fosters a peer to peer style of computation, where any connected node has the same capabilities. Mobile devices can discover each other using a decentralized lookup service and then communicate using remote primitives. The paper presents the PeerSpaces model and gives its operational semantics in terms of a process calculus. Besides a formal specification of the model, the semantics presented in the paper supports formal reasoning about ap...