We realize a simple approach employing a logical type theory for the specification and verification of concurrent programs and systems. Type theories have been sucessfully applied in the field of functional programming to ensure partial or even total correctness. Here we present an embedding of a notion of concurrent programs and systems into the Calculus of Inductive Constructions. The embedding is not only simple and natural but also allows us to take full advantage of the underlying type theory. As a basis we use the idea of the UNITY method developed by Chandy and Misra to represent programs and systems as unbounded nondeterministic iterative transformations. As a specification and verification language we employ a variant of UNITY temporal logic in the expressive higher order logic framework which is provided by the propositions-as-types interpretation. As a first step and a starting point for applications we have developed a verified, general-purpose temporal logic library for the COQ proof assistant which can be used to specify and verify concurrent programs and systems. The concrete application of the library is demonstrated by a small example. Actually, the library is open for extensions and will be further developed in the future guided by the experience obtained from case studies.