916 papers · page 44 of 46
Abstract We extend the definition of natural semantics to include simply typed λ-terms, instead of first-order terms, for representing programs, and to include inference rules for the introduction and discharge of hypotheses and eigenvariables. This extension, which we call exten…
Abstract An extension of ML with continuation primitives similar to those found in Scheme is considered. A number of alternative type systems are discussed, and several programming examples are given. A continuation-based operational semantics is defined for a small, purely funct…
Abstract This survey presents information concerning the use of functional languages (both strict and non-strict) for teaching in higher education. It lists the languages used by over 70 different institutions, the years in which the courses are given, and the recommended textboo…
Abstract We show how improving values (Burton, 1991) can be extended to handle both upper and lower bounds. The result is a new data type, called improving intervals . We give a simple implementation of improving intervals that uses a list of successively tighter bounds to repres…
Abstract In the period 1986–1991, experiments have been carried out with an introductory course in computer programming, based on functional programming. Due to thorough educational design and evaluation, a successful course has been developed. This has led to a revision of the c…
Abstract The functional programming language Miranda has been used as a first programming language at the University of NSW since the beginning of 1989, when a new computer engineering course and a revised computer science course were introduced. This paper explains the reasons f…
Abstract Objects with dynamic types allow the integration of operations that essentially require runtime type-checking into statically-typed languages. This paper presents two extensions of the ML language with dynamics, based on our work on the CAML implementation of ML, and dis…
Abstract A functional language, Miranda, is being used on an introductory programming course for business students. This paper describes the rationale for such a course and choice of language. An application in the area of operations management, which is used in teaching, is give…
Abstract Values belonging to lazy data types have the advantage that sub-components can be accessed without evaluating the values as a whole: unneeded components remain unevaluated. A disadvantage is that often a large amount of space and time is required to handle lazy data type…
Abstract A binding-time analysis is correct if it always produces consistent binding-time information. Consistency prevents partial evaluators from ‘going wrong’. A sufficient and decidable condition for consistency, called well-annotatedness, was first presented by Gomard and Jo…
Abstract List terminators are discussed as a new form of qualifier in list comprehensions for early termination of a list. The semantics of list terminators is expressed in terms of an optimal translation of list comprehensions (cf. Wadler, 1987) because it makes direct use of a …
Abstract A common technique for improving the speed of program specialization is to specialize the program specializer itself on the program to be specialized, creating a custom program generator . Much research has been devoted to the problem of generating efficient program gene…
Abstract Most programming environments for functional languages offer a single tool used to evaluate programs – either a batch compiler or an interpreter with a read-eval-print loop. This paper presents a programming environment that supports not only evaluation, but also a range…
Abstract We describe the design, implementation and use of a new kind of profiling tool that yields valuable information about the memory use of lazy functional programs. The tool has two parts: a modified functional language implementation which generates profiling information d…
Abstract A new program transformation method is presented. It is a further refinement of supercompilation where the supercompiler is not applied directly to the function to be transformed, but to a metafunction, namely an interpreter which computes this function using its definit…
Abstract Mogensen has exhibited a very compact partial evaluator for the pure lambda calculus, using binding-time analysis followed by specialization. We give a correctness criterion for this partial evaluator and prove its correctness relative to this specification. We show that…
Abstract We present an on-line (run-time) algorithm that manages the granularity of parallel functional programs. The algorithm exploits useful parallelism when it exists, and ignores ineffective parallelism in programs that produce many small tasks. The idea is to balance the am…
Abstract In the last two decades, category theory has become one of the main tools for the denotational investigation of programming languages. Taking advantage of the algebraic nature of the categorical semantics, and of the rewriting systems it suggests, it is possible to use t…
Abstract A closed λ-term E is called an enumerator if Here ⋀ 0 is the set of closed λ-terms,. is the set of natural numbers and the ⌜ n ⌝ are the Church's numerals λ fx . f n x . Such an E is called reducing if, moreover An ingenious recursion theoretic proof by Statman will be p…