Key points are not available for this paper at this time.
This session was devoted to consideration of the potential value of ideas in formal semantics for application to the specification and implementation of operating systems, and the benefits and issues that would arise from such use. Jack Dennis introduced the session by noting that formal definitions of programming languages, such as the definition of PL/I in the Vienna Definition Language, are intended to serve two major practical objectives: 1) to ensure consistent interpretation of language constructs between computer systems so programs may be readily transferred; 2) to provide a standard with respect to which the correctness of implementations may be tested and verified. In contemporary systems user or application programs usually depend, for correct operation, on system facilities for file manipulation, communication, concurrent processing, and controlled access to data and procedures, as well as the linguistic constructs of conventional programming languages. Thus the same practical objectives for application of formal definition techniques hold for operating systems as for programming languages.
Jack B. Dennis (1973) studied this question.