A Framework for the Denotational Semantics of Multi-Composition

ABSTRACT

Given a meta-language that can meaningfully compose highlevel abstractions of DSLs, what is a possible framework for the denotational semantics of such a programming language? Such denotational semantics provide a means for formalization of a given meta-language that offer high levels of assurance for compositional correctness. Within the DARPA V-SPELLS program, teams are tasked with understanding how to unwind the intricacies of legacy code so that it can be patched. This legacy code may be written in multiple languages, have several dependencies, or have portions whose use may be unclear. In particular, this code will require extensive maintenance, and users will want a high level of assurance that any required patches integrate properly with the system and do not introduce potentially critical failures. To guarantee such compositional correctness, our solution with the Johns Hopkins Applied Physics Laboratory (JHU APL) is to create a metalanguage that can read, write, and meaningfully compose high-level abstractions of DSLs. We desire that any composition taking place in our meta-language be provably correct. To accomplish this, we construct an algebraic framework for the denotational semantics of this meta-language whose backbone is created from an objects known as operads. In summary, we provide a strong guarantee for compositional correctness by creating a formal environment through which all patching operations must pass.

BIOS

Zachary Flores is a research scientist on the High Assurance Solutions team at Two Six Technologies interested in denotational semantics and cryptography.  

Eric Bond is a research scientist on the High Assurance Solutions team at Two Six Technologies interested in interactive theorem proving and denotational semantics.

Angelo Taranto is a research scientist on the High Assurance Solutions team at Two Six Technologies interested in formal methods, applied category theory, and machine learning.