A Scott/Strachey style denotational semantics intended to describe pure LISP is examined. I present evidence that it is an accurate rendering of the language described in chapter 1 of the LISP 1.5 Programmer's, Manual, in particular I show that call-by-value and fluid variables are correctly handled. To do this I have: (1) written an operational 'semantics' of pure LISP and shown it equivalent to the denotational one (2) Proved that, relative to the denotational semantics, the LISP functions apply,eval,...,etc. correctly compute meanings. The proof techniques used are derived from the work of Wadsworth; roughly one first proves the results for a class of 'finite' programs and then extends them to all programs by a limiting argument. Conceptually these arguments are inductions on length of computation and to bring this out I've formulated a rule of inference which enables such operational reasoning to be applied to the denotational semantics.

No description available.

No description available.

Typescript (photocopy) / xii, 241 leaves : ill. ; 30 cm. / Title page, contents and abstract only. The complete thesis in print form is available from the University Library. / Thesis (Ph.D.)--University of Adelaide, Dept. of Computing Science, 1980

Extensible programming languages allow users to create fundamentally new syntax and translate this syntax into language primitives. The concept of compile-time meta-programming has been around for decades, but systems that provide such abilities generally disallow the creation of new syntactic forms, or have heavy restrictions on how, or where, this may be done. Genesis is an extension to Java that supports compile-time meta-programming by allowing users to create their own arbitrary syntax. This is achieved through macros that operate on a mix of both concrete and abstract syntax, and produce abstract syntax. Genesis attempts to provide a minimal design whilst maintaining, and extending, the expressive power of other similar macro systems. The core Genesis language definition lacks many of the desirable features found in other systems, such as quasi-quote, hygiene, and static expression-type dispatch, but is expressive enough to define these as syntax extensions. User-defined macros produce only well-formed syntactic structures via the use of a predefined set of classes that define a Java abstract syntax. At the heart of Genesis is a flexible parser that is capable of parsing any context-free grammars - even ambiguous ones. The parser is capable of arbitrary speculation and will consider all possible parses. The parser constructs a graph of possible paths, and is capable of dynamically pruning this graph, or combining nodes, based on precedence or associativity rules. This general parser allows macro programmers to forget about parsing, and concentrate on defining new syntax. One key goal of this system was to address the programmer's learning curve by providing as simple a system as possible. This was achieved by the use of the flexible parser, the introduction of only one new construct to standard Java, and extensions to make programming macros more user friendly. The expressiveness of Genesis is wide ranging; it is capable of providing small scale limited use macros, large scale semantic modifications, through to complete language replacements. To demonstrate this expressiveness, we implement many of the simple test cases found in other systems, such as a type-safe printf, assertions, and iteration statements. These test cases require an ability to perform static type-checking and to manipulate compile-time values and abstract syntax trees. As additional examples of Genesis' expressive power we also provide implementations of embedded subsets of SQL and Haskell. As a final proof of power, the Haskell subset can operate as a stand-alone extension independent of any recognisable Java code.

Thesis (Ph.D.)--University of Texas at Dallas, 2007. / Includes vita. Includes bibliographical references (leaves 137-146)

Thesis (M.S.)--Worcester Polytechnic Institute. / Keywords: Coq; monads; functional reactive programming; formal verification. Includes bibliographical references (leaves 31-32).

Thesis (Ph.D.) -- University of Adelaide, Dept. of Computing Science, 1980. / Typescript (photocopy).

Thesis (M.Sc.) -- University of Adelaide, 1958. / Typewritten copy.

Thesis (M.S.)--Virginia Polytechnic Institute and State University, 1992. / Vita. Abstract. Includes bibliographical references (leaves 92-94). Also available via the Internet.