An 'executable' impredicative semantics for Ada configuration

We present a translation of Ada configuration constructs, in a higher order, impredicatively typed,functional language (HOTFUL) with subtypes. Aim of this work is to provide an expressive executable semantics for Ada configuration constructs, and to verify the suitability of the chosen HOTFUL for such a task. We address, in particular, not only the description of single modular units, but the practicability of the approach when dealing with the development of a whole complex system. After giving the detailed rules for such a translation, we compare our approach with what could be obtained by choosing a different typed language as "target", namely the predicative type system of Standard ML.