Mechanization of the Ravenscar Profile in Coq

The Ravenscar profile has been added to the Ada language as part of the 2005 revision. It is a pragmatic definition of concurrency patterns for real-time systems for mono-core processor. In this paper, we report on an ongoing effort to mechanize a toy language derived from IMP that embeds the Ravenscar profile constructs as they are specified in the Ada Reference Manual. We define the denotational semantics of the language and derive two interpreters for the language.