In this thesis, we study the notions of determinism and confluence in the context of concurrent and sycnrhnous systems. The latter are variants of the pi-calculus and have been extended with a notion of time. The first model is the S-pi-calculus, an extenstion of the SL model where reaction to absence of a signal happens at the end of the instant and where signals are first class values. This model uses signals as a communication mechanism. In this context, we present and characterise a compositional semantics of the S-pi-calculus based on suitable notions of labelled transition system and bisimulation. Based on this semantic framework, we explore the notion of determinacy and the related one of (local) confluence. The second model, TAPIS, is another variant of the pi-calculus where channels are used for communication. We adapted the type theory developed for the S-pi-calculus to TAPIS and show that typable programs are confluent. The typing system developed in this section, and accompagning proofs, has been entirely formalized in Coq.
