<p>Shared programming systems typically fall into one of two categories: systems to distribute code between users, and systems to allow shared access to editing or debugging facilities. Version-control systems allow distribution of code and are often more than adequate for large-scale software development occurring over a long period of time, but they can become unwieldy for fast iterative or exploratory development in which multiple users wish to participate. In these situations, shared editors or pair programming tools may suffice,with the caveat that any user of the system can typically modify any of the code at will. Rather than connecting several users to the same editor session, it would be more effective to allow users to maintain separate sessions while quickly sharing selected chunks of code at will.</p> <p>To enable this paradigm, we have designed a new interpreter to allow distributed users to selectively share code and data at run-time. Our solution consists of a bytecode virtual machine <em>back-end </em>with access to a shared environment and a management mechanism to control creation and usage of these resources. By providing access to interpreter sessions overa network connection, we do not tie our interpreter to executing code from any one particular programming language, allowing any conforming <em>front-end</em> compiler and user interface to be used. This solution allows the development burden of shared programs to be distributed dynamically between users at run-time through the shared environment while still affording control over what and when to share, thereby facilitating more effective incremental or experimental multi-user programming.</p>

The purpose of this research was to investigate the generation of machine code from high-level programming language. The following steps were undertaken: 1) Choose a high-level programming language as the source language and a computer as the target computer. 2) Examine all stages during the compiling of a high-level programming language and all data sets involved in the compilation. 3) Discover the mechanism for generating machine code and the mechanism to generate more efficient machine code from the language. 3) Construct an algorithm for generating machine code for the target computer. The results suggest that compiler is best implemented in a high-level programming language, and that SCANNER and PARSER should be independent of target representations, if possible.

We live in a time where computing devices power essential systems of our society: our automobiles, our airplanes and even our medical services. In these safety-critical systems, bugs do not just cost money to fix; they have a potential to cause harm, even death. Therefore, software correctness is of paramount importance. Existing mainstream programming languages do not support software verification as part of their design, but rely on testing, and thus cannot completely rule out the possibility of bugs during software development. To fix this problem we must reshape the very foundation on which programming languages are based. Programming languages must support the ability to verify the correctness of the software developed in them, and this software verification must be possible using the same language the software is developed in. In the first half of this dissertation we introduce three new programming languages: Freedom of Speech, Separation of Proof from Program, and Dualized Type Theory. The Freedom of Speech language separates a logical fragment from of a general recursive programming language, but still allowing for the types of the logical fragment to depend on general recursive programs while maintaining logical consistency. Thus, obtaining the ability to verify properties of general recursion programs. Separation of Proof from Program builds on the Freedom of Speech languageby relieving several restrictions, and adding a number of extensions. Finally, Dualized Type Theory is a terminating functional programming language rich in constructive duality, and shows promise of being a logical foundation of induction and coninduction. These languages have the ability to verify properties of software, but how can we trust this verification? To be able to put our trust in these languages requires that the language be rigorously and mathematically defined so that the programming language itself can be studied as a mathematical object. Then we must show one very important property, logical consistency of the fragment of the programming language used to verify mathematical properties of the software. In the second half of this dissertation we introduce a well-known proof technique for showing logical consistency called hereditary substitution. Hereditary substitution shows promise of being less complex than existing proof techniques like the Tait-Girard Reducibility method. However, we are unsure which programming languages can be proved terminating using hereditary substitution. Our contribution to this line of work is the application of the hereditary substitution technique to predicative polymorphic programming languages, and the first proof of termination using hereditary substitution for a classical type theory.

Abstract not available

Partial programming is a field of study where users specify an outline or skeleton of a program, but leave various parts undefined. The undefined parts are then completed by an external mechanism to form a complete program. Adaptation-Based Programming (ABP) is a method of partial programming that utilizes techniques from the field of reinforcement learning (RL), a subfield of machine learning, to find good completions of those partial programs. An ABP user writes a partial program in some host programming language. At various points where the programmer is uncertain of the best course of action, they include choices that non-deterministically select amongst several options. Additionally, users indicate program success through a reward construct somewhere in their program. The resulting non-deterministic program is completed by treating it as an equivalent RL problem and solving the problem with techniques from that field. Over repeated executions, the RL algorithms within the ABP system will learn to select choices at various points that maximize the reward received. This thesis explores various aspects of ABP such as the semantics of different implementations, including different design trade-offs encountered with each approach. The goal of all approaches is to present a model for programs that adapt to their environment based on the points of uncertainty within the program that the programmer has indicated. The first approach presented in this work is an implementation of ABP as a domain-specific language embedded within a functional language. This language provides constructs for common patterns and situations that arise in adaptive programs. This language proves to be compositional and to foster rapid experimentation with different adaptation methods (e.g. learning algorithms). A second approach presents an implementation of ABP as an object-oriented library that models adaptive programs as formal systems from the field of RL called Markov Decision Processes (MDPs). This approach abstracts away many of the details of the learning algorithm from the casual user and uses a fixed learning algorithm to control the program adaptation rather than allowing it to vary. This abstraction results in an easier-to-use library, but limits the scenarios that ABP can effectively be used in. Moreover, treating adaptive programs as MDPs leads to some unintuitive situations where seemingly reasonably programs fail to adapt efficiently. This work addresses this problem with algorithms that analyze the adaptive program's structure and data flow to boost the rate at which these problematic adaptive programs learn thus increasing the number of problems that ABP can effectively be used to solve. / Graduation date: 2013

The general area of developing, applying and studying new and parallel models of computation is motivated by a need to overcome the limits of current Von Neumann based architectures. A key area of research in understanding how new technology can be applied to Al problem solving is through using logic languages. Logic programming languages provide a procedural interpretation for sentences of first order logic, mainly using a class of sentence called Horn clauses. Horn clauses are open to a wide variety of parallel evaluation models, giving possible speed-ups and alternative parallel models of execution. The research in this thesis is concerned with investigating one class of parallel logic language known as Committed Choice Non-Deterministic languages. The investigation considers the inherent parallel behaviour of Al programs implemented in the CCND languages and the effect of various alternatives open to language implementors and designers. This is achieved by considering how various Al programming techniques map to alternative language designs and the behaviour of these Al programs on alternative implementations of these languages. The aim of this work is to investigate how Al programming techniques are affected (qualitatively and quantitatively) by particular language features. The qualitative evaluation is a consideration of how Al programs can be mapped to the various CCND languages. The applications considered are general search algorithms (which focuses on the committed choice nature of the languages); chart parsing (which focuses on the differences between safe and unsafe languages); and meta-level inference (which focuses on the difference between deep and flat languages). The quantitative evaluation considers the inherent parallel behaviour of the resulting programs and the effect of possible implementation alternatives on this inherent behaviour. To carry out this quantitative evaluation we have implemented a system which improves on the current interpreter based evaluation systems. The new system has an improved model of execution and allows several

Swift is a new programming language developed by Apple for creating iOS and Mac OS X applications. Intended to eventually replace Objective-C as Apple’s language of choice, Swift needs to convince developers to switch over to the new language. Apple has promised that Swift will be faster than Objective-C, as well as offer more modern language features, be very safe, and be easy to learn and use. In this thesis I test these claims by creating an iOS application entirely in Swift as well as benchmarking two different algorithms. I find that while Swift is faster than Objective-C, it does not see the speedup projected by Apple. I also conclude that Swift offers many advantages over Objective-C, and is easy for developers to learn and use. However there are some weak areas of Swift involving interactions with Objective-C and the strictness of the compiler that can make the language difficult to work with. Despite these difficulties Swift is overall a successful project for Apple and should attract new developers to their platform.

Thesis (Ph. D.)--College of Computing, Georgia Institute of Technology, 2005. Directed by Yannis Smaragdakis. / Spencer Rugaber, Committee Member ; Olin Shivers, Committee Member ; Mary Jean Harrold, Committee Member ; Yannis Smaragdakis, Committee Chair ; Philip Wadler, Committee Member. Includes bibliographical references.

Thesis (M. S.)--Mechanical Engineering, Georgia Institute of Technology, 2009. / Committee Chair: Paredis, Chris; Committee Member: McGinnis, Leon; Committee Member: Schaefer, Dirk.

Two major applications of lambda calculi in computer science are functional programming languages and mechanized reasoning systems (or, proof assistants). According to the Curry--Howard correspondence, it is possible, in principle, to design a unified language based on a typed lambda calculus for both logical reasoning and programming. However, the different requirements of programming languages and reasoning systems make it difficult to design such a unified language that provides both. Programming languages usually extend lambda calculi with programming-friendly features (e.g., recursive datatypes, general recursion) for supporting the flexibility to model various computations, while sacrificing logical consistency. Logical reasoning systems usually extend lambda calculi with logic-friendly features (e.g., induction principles, dependent types) for paradox-free inference over fine-grained properties, while being more restrictive in modeling computations. In this dissertation, we design and implement a language called Nax that embraces benefits of both. Nax accepts all recursive datatypes, thus, allowing the same flexibility of defining recursive datatypes as in functional languages. Nax supports a number of Mendler-style recursion schemes that can express various kinds of recursive computations and also guarantee termination. Nax supports term-indexed types to support specifications of fine-grained properties. In addition, Nax supports a conservative extension of Hindley--Milner type inference. The theoretical contributions of this dissertation include theories for Mendler-style recursion schemes and term-indexed types, which we developed to establish strong normalization and logical consistency of Nax.