In ProCoS I, it was demonstrated, how a compiler for a very simple language could be specified and implemented in a provably correct manner. In ProCoS II we concentrate on compiler development for more powerful languages, including real-time and parallelism. The work centered on program compilation is essentially done at Kiel University. It is divided into the following parts: