Summary: ``New constructs for synchronization termed synchronization expressions (SEs) have been developed as high-level language constructs for parallel programming languages. Statements that are constrained by certain synchronization requirements are tagged, and synchronization requests are specified as expressions of statement tags. \par ``In this paper, we introduce a new family of languages named synchronization languages which we use to give a precise semantic description for SEs. Under this description, relations such as equivalence and inclusion between SEs can be easily understood and tested. In practice, it also provides us with a systematic way for the implementation as well as the simplification of SEs in parallel programming languages. \par ``We show that each synchronization language is closed under the following rewriting rules: (1) $a_sb_s\to b_sa_s$, (2) $a_tb_t\to b_ta_t$, (3) $a_sb_t\to b_ta_s$, (4) $a_ta_sb_tb_s\to b_tb_sa_ta_s$ and also $h(a_ta_sb_tb_s)\to h(b_tb_sa_ta_s)$ for any morphism $h$ that satisfies certain conditions which are specified in the paper. We conjecture that closure under the above rewriting rules is a sufficient condition for a regular start-termination language to be a synchronization language. Several other properties of synchronization languages are also studied.''