Foundational research in programming language semantics has given us the ability to design languages for sequential programming with strong theoretical properties, which translate into run-time assurance for programs written in such languages. Recently, logical frameworks such as Twelf and Coq have been used to formally prove deep properties of full-scale practical programming languages, such as the safety of Standard ML or the correctness of a compiler for an expressive subset of C. In contrast, no overarching methodologies exist yet for languages for distributed computation, which are gaining prominence with the advent of web programming, security infrastructures, and cloud computing. This means that we cannot say as much about the properties of present languages in these domains as a whole, or behaviors of specific programs written in them. We propose to develop recent work on language specification with substructural operational semantics (SSOS) into methodologies for designing and reasoning about programming and specification languages for distributed computation. We further propose the use of the Concurrent Logical Framework (CLF) in order to elegantly implement SSOS specifications, and to develop and implement (co)inductive techniques to reason about such specification. Finally, we propose to carry out case studies with logically-based languages for distributed computation such as ML5 to demonstrate the practicality of our approach.