916 papers · page 46 of 46
Programming languages which are capable of interpreting themselves have been fascinating computer scientists. Indeed, if this is possible then a ‘strange loop’ (in the sense of Hofstadter, 1979) is involved. Nevertheless, the phenomenon is a direct consequence of the existence of…
Abstract For numeral systems in untyped λ-calculus the definability of a successor, a predecessor and a test for zero implies the definability of all recursive functions on that system. Towards a disproof of the converse statement, H. P. Barendregt and the author constructed a nu…
The problem of computing the smallest natural number not contained in a given set of natural numbers has a number of practical applications. Typically, the given set represents the indices of a class of objects ‘in use’ and it is required to find a ‘free’ object with smallest ind…
The function remdup (also called mkset in some functional languages) removes duplicates from a given list. The following definition of remdup is standard and leads to a quadratic time algorithm The operator (—) used in the last expression subtracts one list from another; its defi…
Abstract The evaluation transformer model of reduction generalizes lazy evaluation in two ways: it can start the evaluation of expressions before their first use, and it can evaluate expressions further than weak head normal form. Moreover, the amount of evaluation required of an…
Abstract A parallel program may be indeterminate so that it can adapt its behavior to the number of processors available. Indeterminate programs are hard to write, understand, modify or verify. They are impossible to debug, since they may not behave the same from one run to the n…
Abstract Quest is a programming language based on impredicative type quantifiers and subtyping within a three-level structure of kinds, types and type operators, and values. The semantics of Quest is rather challenging. In particular, difficulties arise when we try to model simul…
Abstract We present a modular proof of strong normalization for the Calculus of Constructions of Coquand and Huet (1985, 1988). This result was first proved by Coquand (1986), but our proof is more perspicious. The method consists of a little juggling with some systems in the cub…
Abstract This article describes theoretical and practical aspects of an implemented self-applicable partial evaluator for the untyped lambda-calculus with constants and a fixed point operator. To the best of our knowledge, it is the first partial evaluator that is simultaneously …
Abstract Abstract interpretation is the collective name for a family of semantics-based techniques for compile-time analysis of programs. One of the most costly operations in automating such analyses is the computation of fixed points. The frontiers algorithm is an elegant method…
Abstract This paper presents an application of functional programming: searching a domain for elements which satisfy certain constraints. We give a very general formulation of the problem and describe ‘generate and test’, ‘backtracking’ and ‘forward checking’ algorithms. We then …
Abstract Traditionally the view has been that direct expression of control and store mechanisms and clear mathematical semantics are incompatible requirements. This paper shows that adding objects with memory to the call-by-value lambda calculus results in a language with a rich …
Abstract Subtyping appears in a variety of programming languages, in the form of the ‘automatic coercion’ of integers to reals, Pascal subranges, and subtypes arising from class hierarchies in languages with inheritance. A general framework based on untyped lambda calculus provid…
Abstract Traditional functional languages do not have an explicit distinction between binding times. It arises implicitly, however, as one typically instantiates a higher-order function with the arguments that are known, whereas the unknown arguments remain to be taken as paramet…
Abstract A method is proposed to search for an identifier in a functional program library by using its Hindley–Milner type as a key. This can be seen as an approximation of using the specification as a key. Functions that only differ in their argument order or currying are essent…
Abstract Polymorphic types are labels classifying both ( a ) defined components in a library and ( b ) contexts of free variables in partially written programs. It is proposed to help programmers make better use of software libraries by providing a system that, given ( b ), ident…