916 papers · page 34 of 46
In higher-order abstract syntax, the variables and bindings of an object language are represented by variables and bindings of a meta-language. Let us consider the simply typed λ-calculus as object language and Haskell as meta-language. For concreteness, we also throw in integers…
We propose a new style of writing graph algorithms in functional languages which is based on an alternative view of graphs as inductively defined data types. We show how this graph model can be implemented efficiently, and then we demonstrate how graph algorithms can be succinctl…
This article describes a general framework for designing purely functional datatypes that automatically satisfy given size or structural constraints. Using the framework we develop implementations of different matrix types (for example, square matrices) and implementations of sev…
Suppose, you want to implement a structured editor for some term type, so that the user can navigate through a given term and perform edit actions on subterms. In this case you are immediately faced with the problem of how to keep track of the cursor movements and the user's edit…
We introduce a typed programming formalism, type-2 inflationary tiered loop programs or ITLP 2 , that characterizes the type-2 basic feasible functionals. ITLP 2 is based on Bellantoni and Cook's (1992) and Leivant's (1995) type-theoretic characterization of polynomial-time, and …
Compare first-order functional programs with higher-order programs allowing functions as function parameters. Can the the first program class solve fewer problems than the second? The answer is no: both classes are Turing complete , meaning that they can compute all partial recur…
Chris Okasaki showed how to implement red-black trees in a functional programming language. Ralf Hinze incorporated even the invariants of such data structures into their types, using higher-order nested datatypes. We show how one can achieve something very similar without the us…
First-order languages based on rewrite rules share many features with functional languages, but one difference is that matching and rewriting can be made much more expressive and powerful by incorporating some built-in equational theories. To provide reasonable programming enviro…
Launchbury and Peyton Jones came up with an ingenious idea for embedding regions of imperative programming in a pure functional language like Haskell. The key idea was based on a simple modification of Hindley-Milner's type system. Our first contribution is to propose a more natu…
Every designer of a new data structure wants to know how well it performs in comparison with others. But finding, coding and testing applications as benchmarks can be tedious and time-consuming. Besides, how a benchmark uses a data structure may considerably affect its apparent e…
This article describes the implementation of a debugger for lazy functional languages like Haskell. The key idea is to construct a declarative trace which hides the operational details of lazy evaluation. However, to avoid excessive memory consumption, the trace is constructed on…
We describe a unified, lazy, declarative framework for solving constraint satisfaction problems, an important subclass of combinatorial search problems. These problems are both practically significant and computationally hard. Finding solutions involves combining good general-pur…
Many polyvariant program analyses have been studied in the 1990s, including k -CFA, polymorphic splitting, and the cartesian product algorithm. The idea of polyvariance is to analyze functions more than once and thereby obtain better precision for each call site. In this paper we…
Destructive array update optimization is critical for writing scientific codes in functional languages. We present set constraints for an interprocedural update optimization that runs in polynomial time. This is a multi-pass optimization, involving interprocedural flow analyses f…
It is well known that there is an isomorphism between natural deduction derivations and typed lambda terms. Moreover, normalising these terms corresponds to eliminating cuts in the equivalent sequent calculus derivations. Several papers have been written on this topic. The corres…
Pure type systems make use of domain-full λ-abstractions λx:D.M. We present a variant of pure type systems, which we call domain-free pure type systems, with domain-free λ-abstractions λx.M. Domain-free pure type systems have a number of advantages over both pure type systems and…
In this work we put forward an algorithm for the mechanical verification of an extension of Martin-Löf's theory of types with dependent record types and subtyping. We first give a concise description of that theory and motivate its use for the formalization of algebraic construct…
Researchers have recently proposed that for certain applications it is advantageous to use functional languages whose type systems are based upon linear logic: so-called linear functional languages. In this paper we develop reasoning techniques for programs in a linear functional…
In this paper we present two type inference systems for detecting useless-code in higher-order typed functional programs. Type inference can be performed in an efficient and complete way, by reducing it to the solution of a system of constraints. We also give a useless-code elimi…
We propose a parallel specialized language that ensures portable and cost-predictable implementations on parallel computers. The language is basically a first-order, recursion-less, strict functional language equipped with a collection of higher-order functions or skeletons. Thes…