If we classify variables in a program into various security levels, then a secure information flow analysis aims to verify statically that information in a program can flow only in ways consistent with the specified security levels. One well-studied approach is to formulate the rules of the secure information flow analysis as a type system. A major trend of recent research focuses on how to accommodate various sophisticated modern language features. However, this approach often leads to overly complicated and restrictive type systems, . making them unfit for practical use. Also, problems essential to practical use, such as type inference and error reporting, have received little attention. This dissertation identified and solved major theoretical and practical hurdles to the application of secure information flow. We adopted a minimalist approach to designing our language to ensure a simple lenient type system. We started out with a small simple imperative language and only added features that we deemed most important for practical use. One language feature we addressed is arrays. Due to the various leaking channels associated with array operations, arrays have received complicated and restrictive typing rules in other secure languages. We presented a novel approach for lenient array operations, which lead to simple and lenient typing of arrays. Type inference is necessary because usually a user is only concerned with the security types for input/output variables of a program and would like to have all types for auxiliary variables inferred automatically. We presented a type inference algorithm B and proved its soundness and completeness. Moreover, algorithm B stays close to the program and the type system and therefore facilitates informative error reporting that is generated in a cascading fashion. Algorithm Band error reporting have been implemented and tested. Lastly, we presented a novel framework for developing applications that ensure user information privacy. In this framework, core computations are defined as code modules that involve input/output data from multiple parties. Incrementally, secure flow policies are refined based on feedback from the type checking/inference. Core computations only interact with code modules from involved parties through well-defined interfaces. All code modules are digitally signed to ensure their authenticity and integrity.

This thesis is mainly concerned with semantic data modelling related to database design. The domain of this research is restricted to general data modelling and the discussion is carried out at the conceptual level. The thesis assesses a number of serious modelling shortcomings of the conventional data models and reviews several basic principles and mechanisms developed in current semantic data modelling research. Based on these findings, the thesis identifies the inadequacy of the conceptualization of data modelling and develops the two-view conceptualization of data modelling. The basic idea behind the two-view conceptualization is that the conceptual structure of the applications being modelled should be separated from its external data representation. A new semantic database model, SDBM, is designed based on the conceptualization. The model makes a clear separation between the conceptual structure and its external data representation. It offers a data type mechanism to deal with the data representation, a window mechanism to model the conceptual structure, and a transaction mechanism to provide database operations. One of the major extensions of the current semantic data models is that with SDBM the specialization relationship is just a special case of constraints that can be specified among SDBM windows. A formal syntax and informal semantics of SDBM are given in the thesis along with comparisons between SDBM and a closely-related semantic data model, Taxis. / Business, Sauder School of / Graduate

This thesis examines the semantic definition of a programming language by a form of attribute grammar for ease of understanding. The attributes are expressed in a simple macro language and when evaluated produce code for an abstract machine. Part of an actual definition is looked at and found to be too obscure to be useful. The reasons for the obscurity are identified and suggestions are made for eliminating them. / Science, Faculty of / Computer Science, Department of / Graduate

Abstract Not Provided. / Thesis / Master of Engineering (MEngr)

No description available.

Object-oriented programming has gained significant traction in the software development community and is now the common approach for developing large, commercial applications. Many of these applications require the behaviour of objects to be modified at run-time. Contemporary class-based, statically-typed languages such as C++ and Java require collaboration with external objects to modify an object’s behaviour. Furthermore, such an object must be designed to order to support such collaborations. Dynamic languages such as Python which natively support object extension do not guarantee type safety. In this work, using dynamic mixins with static typing is proposed as a means of providing type-safe, object extension. A new language called mix is introduced that allows a compiler to syntactically check the type-safety of an object extension. A model to support object-oriented development is extended to support dynamic mixins. The utility of the approach is illustrated using sample use cases. Finally, a compiler was implemented to validate the practicality of the model proposed. / Thesis / Doctor of Philosophy (PhD)

Answer set programming (ASP) is a form of declarative programming oriented towards difficult combinatorial search problems. It has been applied, for instance, to plan generation and product configuration problems in artificial intelligence and to graph-theoretic problems arising in VLSI design and in historical linguistics. Syntactically, ASP programs look like Prolog programs, but the computational mechanisms used in ASP are different: they are based on the ideas that have led to the development of fast satisfiability solvers for propositional logic. ASP is based on the answer set/stable model semantics for logic problems, originally intended as a specification for query answering in Prolog. From the original definition of 1988, the semantics was independently extended by different research groups to more expressive kinds of programs, with syntax and semantics that are incompatible with each other. In this thesis we study how the various extensions are related to each other. In order to do that, we propose another definition of an answer set. This definition has three main characteristics: (i) it is very simple, (ii) its syntax is more general than the usual concept of a logic program, and (iii) strong theoretical tools can be used to reason on it. About (ii), we show that our syntax allows constructs defined in many other extensions of the answer sets semantics. This fact, together with (iii), allows us to study the expressiveness of those constructs. We also compare the answer set semantics with another important formalism developed by Norm McCain and Hudson Turner, called logic. / text

Thesis (Ph. D.)--University of Texas at Austin, 2007. / Vita. Includes bibliographical references.

Thesis (Ph. D.)--University of Alabama at Birmingham, 2007. / Additional advisors: Marjan Mernik, Jeffrey G. Gray, Alan P. Sprague, Elliot J. Lefkowitz. Description based on contents viewed May 29, 2008; title from title screen. Includes bibliographical references (p. 140-152).

The programs that are easiest to write and understand are often not the most efficient. This thesis gives methods of converting programs of the former type to those of the latter type; this involves converting definitions of algorithms given as recursion equations using high level primitives into lower level flow chart programs. The main activities involved are recursion removal (c.f. Strong), loop elimination, and the overwriting of shared structures. We have concentrated on the semantics, rather than the syntax, of the programs we are transforming and we have used techniques developed in work done on proving the correctness of programs. The transformations are done in a hierarchical manner and can be regarded as compiling a program defined in a structured manner (Dijkstra) to produce an efficient low level program that simulates it. We describe the implementation of a system that allows the user to specify algorithms in a simple set language and converts them to flow chart programs in either a bitstring or list processing language. Both of these lower languages allow the sharing of structures. The principles are applicable to other domains and we describe how our system can be applied more generally.