Formalisation of C Language Interfaces

In practical computing, implementations of programming languages provide an interface that allow programs written in a language to call code written in another programming language, most often C. Usually, those language interfaces are left out of the formal definition of the language, and reasoning about multi-language programs is very difficult due to the lack of precise specifications for the language interfaces. In this paper, we present an application of a framework for the interoperability of programming languages, in which we specified in a systematic way the C interface of a real, rule-based programming language. Our framework is based on simple combinations of the small-step operational semantics of programming languages. We give the main elements of a small-step semantics for the C programming language that can be used to specify the same kind of interfaces for other programming languages implemented in C.