Accession Number : ADA570656


Title :   Substructural Logical Specifications


Descriptive Note : Doctoral thesis


Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE


Personal Author(s) : Simmons, Robert J


Full Text : https://apps.dtic.mil/dtic/tr/fulltext/u2/a570656.pdf


Report Date : 14 Nov 2012


Pagination or Media Count : 318


Abstract : A logical framework and its implementation should serve as a flexible tool for specifying, simulating, and reasoning about formal systems. When the formal systems we are interested in exhibit state and concurrency, however, existing logical frameworks fall short of this goal. Logical frameworks based on a rewriting interpretation of substructural logics, ordered and linear logic in particular, can help. To this end, this dissertation introduces and demonstrates four methodologies for developing and using substructural logical frameworks for specifying and reasoning about stateful and concurrent systems. Structural focalization is a synthesis of ideas from Andreoli's focused sequent calculi and Watkins's hereditary substitution. We can use structural focalization to take a logic and define a restricted form of derivations, the focused derivations, that form the basis of a logical framework. We apply this methodology to define SLS, a logical framework for substructural logical specifications, as a fragment of ordered linear lax logic. Logical correspondence is a methodology for relating and inter-deriving different styles of programming language specification in SLS. The styles we connect range from very high-level specification styles like natural semantics, which do not fully specify the control structure of programs, to low-level specification styles like destination-passing, which provide detailed control over concurrency and control flow. We apply this methodology to systematically synthesize a low-level destination-passing semantics for a Mini-ML language extended with stateful and concurrent primitives. The specification is mostly high-level except for the relatively few rules that actually deal with concurrency. Linear logical approximation is a methodology for deriving program analyses by performing abstract analysis on the SLS encoding of the language's operational semantics.


Descriptors :   *PROGRAMMING LANGUAGES , COMPUTER LOGIC , COMPUTER SCIENCE , THESES


Subject Categories : Computer Programming and Software


Distribution Statement : APPROVED FOR PUBLIC RELEASE