This thesis presents a critical analysis of normalisation by evaluation as a technique for speeding up compilation of typed functional programming languages. Our investigation focuses on the SML.NET compiler and its typed intermediate language MIL. We implement and measure the performance of normalisation by evaluation for MIL across a range of benchmarks. Taking a different approach, we also implement and measure the performance of a graph-based shrinking reductions algorithm for SML.NET. MIL is based on Moggi’s computational metalanguage. As a stepping stone to normalisation by evaluation, we investigate strong normalisation of the computational metalanguage by introducing an extension of Girard-Tait reducibility. Inspired by previous work on local state and parametric polymorphism, we define reducibility for continuations and more generally reducibility for frame stacks. First we prove strong normalistion for the computational metalanguage. Then we extend that proof to include features of MIL such as sums and exceptions. Taking an incremental approach, we construct a collection of increasingly sophisticated normalisation by evaluation algorithms, culminating in a range of normalisation algorithms for MIL. Congruence rules and alpha-rules are captured by a compositional parameterised semantics. Defunctionalisation is used to eliminate eta-rules. Normalisation by evaluation for the computational metalanguage is introduced using a monadic semantics. Variants in which the monadic effects are made explicit, using either state or control operators, are also considered. Previous implementations of normalisation by evaluation with sums have relied on continuation-passing-syle or control operators. We present a new algorithm which instead uses a single reference cell and a zipper structure. This suggests a possible alternative way of implementing Filinski’s monadic reflection operations. In order to obtain benchmark results without having to take into account all of the features of MIL, we implement two different techniques for eliding language constructs. The first is not semantics-preserving, but is effective for assessing the efficiency of normalisation by evaluation algorithms. The second is semantics-preserving, but less flexible. In common with many intermediate languages, but unlike the computational metalanguage, MIL requires all non-atomic values to be named. We use either control operators or state to ensure each non-atomic value is named. We assess our normalisation by evaluation algorithms by comparing them with a spectrum of progressively more optimised, rewriting-based normalisation algorithms. The SML.NET front-end is used to generate MIL code from ML programs, including the SML.NET compiler itself. Each algorithm is then applied to the generated MIL code. Normalisation by evaluation always performs faster than the most naıve algorithms— often by orders of magnitude. Some of the algorithms are slightly faster than normalisation by evaluation. Closer inspection reveals that these algorithms are in fact defunctionalised versions of normalisation by evaluation algorithms. Our normalisation by evaluation algorithms perform unrestricted inlining of functions. Unrestricted inlining can lead to a super-exponential blow-up in the size of target code with respect to the source. Furthermore, the worst-case complexity of compilation with unrestricted inlining is non-elementary in the size of the source code. SML.NET alleviates both problems by using a restricted form of normalisation based on Appel and Jim’s shrinking reductions. The original algorithm is quadratic in the worst case. Using a graph-based representation for terms we implement a compositional linear algorithm. This speeds up the time taken to perform shrinking reductions by up to a factor of fourteen, which leads to an improvement of up to forty percent in total compile time.

Functional reactive programming (FRP) is a paradigm extending functional languages with primitives which operate on state. Typical FRP systems contain many dozens of such primitives. This thesis aims to identify a minimal subset of primitives which captures the same set of behavior as these systems, and to provide an axiomatic semantics for them using first-order linear temporal logic, with the aim of utilizing these semantics in formal verification of FRP programs. Furthermore, we identify several important properties of these primitives and prove that they are satisfied using the Coq proof assistant.

This thesis describes TeaBag, which is a debugger for functional logic computations. TeaBag is an accessory of a virtual machine currently under development. A distinctive feature of this machine is its operational completeness of computations, which places novel demands on a debugger. This thesis describes the features of TeaBag, in particular the handling of non-determinism, the ability to control nondeterministic steps, to remove context information, to toggle eager evaluation, and to set breakpoints on both functions and terms. This thesis also describes TeaBag's architecture and its interaction with the associated virtual machine. Finally, some debugging sessions of defective programs are presented to demonstrate TeaBag's ability to locate bugs. A distinctive feature of TeaBag is how it presents non-deterministic trace steps of an expression evaluation trace to the user. In the past expression evaluation traces were linearized via backtracking. However, the presence of backtracking makes linear traces difficult to follow. TeaBag does not present backtracking to the user. Rather TeaBag presents the trace in two parts. One part is the search space which has a tree structure and the other part is a linear sequence of steps for one path through the search space.

Establishing the termination of programs is a fundamental problem in the field of software verification. For transformational programs, termination is used to extend partial correctness to total correctness. For reactive systems, termination reasoning is used to establish liveness properties. In the context of theorem proving, termination is used to establish the consistency of definitional axioms and to automate proofs by induction. Of course, termination is an undecidable problem, as Turing himself proved. However, the question remains: how automatic can a general termination analysis be in practice? In this dissertation, we develop two new general frameworks for reasoning about termination and demonstrate their effectiveness in automating the task of proving termination in the domain of applicative first-order functional languages. The foundation of the first framework is the development of the first known complete set of algorithms for ordinal arithmetic over an ordinal notation. We provide algorithms for ordinal ordering ($<$), addition, subtraction, multiplication, and exponentiation on the ordinals up to epsilon-naught. We prove correctness and complexity results for each algorithm. We also create a library for automating arithmetic reasoning over epsilon-naught in the ACL2 theorem proving system. This ordinal library enables new termination proofs that were previously not possible in previous versions of ACL2. The foundation of the second framework is an algorithm for fully automating termination reasoning with no user assistance. This algorithm uses a combination of theorem proving and static analysis to create a Calling Context Graph (CCG), a novel abstraction that captures the looping behavior of the program. Calling Context Measures (CCMs) are then used to prove that no infinite path through the CCG can be an actual computation of the program. We implement this algorithm in the ACL2, and empirically evaluate its effectiveness on the regression suite, a collection of over 11,000 user-defined functions from a wide variety of applications.

Thesis (M.S.)--University of North Texas, Dec., 2009. / Title from title page display. Includes bibliographical references.

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 (Ph. D.)--OGI School of Science & Engineering at OHSU, 2002.

Thesis (M. Sc.)--University of Canterbury, 2006. / Typescript (photocopy). Includes bibliographical references (leaves 101-107). Also available via the World Wide Web.

Non-strict pure functional programming often requires redesigning algorithms and data structures to work more effectively under new constraints of non-strict evaluation and immutable state. Graph drawing algorithms, while numerous and broadly studied, have no presence in the non-strict pure functional programming model. Additionally, there is currently no freely licensed standalone toolkit used to quantitatively analyze aesthetics of graph drawings. This thesis addresses two previously unexplored questions. Can a force-directed graph drawing algorithm be implemented in a non-strict functional language, such as Haskell, and still be practically usable? Can an easily extensible aesthetic measuring tool be implemented in a language such as Haskell and still be practically usable? The focus of the thesis is on implementing one of the simplest force-directed algorithms, that of Fruchterman and Reingold, and comparing its resulting aesthetics to those of a well-known C++ implementation of the same algorithm.

<p>Analizirani su važniji predstavnici čisto-funkcionalnih programskih jezika i važniji načini njihove implementacije . Na osnovu uočenih osobina, jezici su podeljeni na klase. Definisan je novi medjujezik za implementaciju čisto-funkcionalnih programskih jezika kojim je moguće predstaviti vi&scaron;e klasa funkcionalnih programskih jezika nego postojećim medjujezicima. Konstruisani su algoritmi translacije 4 vi&scaron;a funkcionalna jezika u medjujezik i algoritmi prevodjenja medjujezika u ma&scaron;inske jezike 5 apstraktnih ma&scaron;ina. Diskutovani su neki praktični aspekti implementacije nedjujezika i izvr&scaron;ene analize performansi nekoliko&nbsp; realizovanih prevodilaca.</p> / <p>Important purely functional languages and important ways of their implementation are analyzed. Based on observed characteristics, functional languages are divided into appropriate classes. A new specialized intermediate code for implementation of functional programming languages is defined, which enable a representation of more classes of high-level functional languages than existing intermediate codes. Algorithms for translation of four high-level functional languages into intermediate code are constructed, as well as algorithms for compilation of intermediate code into five abstract machine languages. Performance of several implemented compilers are analyzed.</p>