916 papers · page 12 of 46
Abstract Dependent pattern matching is an intuitive way to write programs and proofs in dependently typed languages. It is reminiscent of both pattern matching in functional languages and case analysis in on-paper mathematics. However, in general, it is incompatible with new type…
The 12th International Symposium on Functional and Logic Programming was held in Kanazawa, Japan, June 4–6, 2014. The aim of the Functional and Logic Programming series of conferences is to bring together researchers interested in declarative programming including functional prog…
Abstract We compare two inherently different approaches to implement complex process systems in Eden: stable process systems and a compositional approach. A stable process system is characterised by handling several computation stages in each of the participating processes. Often…
The 19th ACM SIGPLAN International Conference on Functional Programming (ICFP) took place on September 1–3, 2014 in Gothenburg, Sweden. After the conference, the programme committee, chaired by Manuel Chakravarty, selected several outstanding papers and invited their authors to s…
Abstract Folds and unfolds have been understood as fundamental building blocks for total programming, and have been extended to form an entire zoo of specialised structured recursion schemes. A great number of these schemes were unified by the introduction of adjoint folds, but m…
Abstract Information-flow control mechanisms are difficult both to design and to prove correct. To reduce the time wasted on doomed proof attempts due to broken definitions, we advocate modern random-testing techniques for finding counterexamples during the design process. We sho…
Many students complete PhDs in functional programming each year. As a service to the community, the Journal of Functional Programming publishes the abstracts from PhD dissertations completed during the previous year.
Many students complete PhDs in functional programming each year. As a service to the community, the Journal of Functional Programming publishes the abstracts from PhD dissertations completed during the previous year.
Abstract We settle three basic questions that naturally arise when verifying code generators written in multi-stage functional programming languages. First, does adding staging to a language compromise any equalities that hold in the base language? Unfortunately it does, and more…
Abstract It is well known that simply typed λ-terms can be used to represent numbers, as well as some other data types. We show that λ-terms of each fixed (but possibly very complicated) type can be described by a finite piece of information (a set of appropriately defined inters…
Abstract Effect systems have the potential to help software developers, but their practical adoption has been very limited. We conjecture that this limited adoption is due in part to the difficulty of transitioning from a system where effects are implicit and unrestricted to a sy…
Abstract The runtime for a modern, concurrent, garbage collected language like Java or Haskell is like an operating system: sophisticated, complex, performant, but alas very hard to change. If more of the runtime system were in the high-level language, it would be far more modula…
Abstract Current systems for safely manipulating values containing names only support simple binding structures for those names. As a result, few tools exist to safely manipulate code in those languages for which name problems are the most challenging. We address this problem wit…
Abstract Reliability is set to become a major concern on emergent large-scale architectures. While there are many parallel languages, and indeed many parallel functional languages, very few address reliability. The notable exception is the widely emulated Erlang distributed actor…
Abstract This paper proposes a new typed lambda-encoding for inductive types which, for Peano numerals, has the expected time complexities for basic operations like addition and multiplication, has a constant-time predecessor function, and requires only quadratic space to encode …
Abstract Graphics Processing Units (GPUs) offer potential for very high performance; they are also rapidly evolving. Obsidian is an embedded language (in Haskell) for implementing high performance kernels to be run on GPUs. We would like to have our cake and eat it too; we want t…
Abstract The main aim of the paper is to give a simple and conceptual account for the correspondence (originally described by Bodini, Gardy, and Jacquot) between α-equivalence classes of closed linear lambda terms and isomorphism classes of rooted trivalent maps on compact-orient…
Abstract Proving bounds on the resource consumption of a program by statically analyzing its source code is an important and well-studied problem. Automatic approaches for numeric programs with side effects usually apply abstract interpretation-based invariant generation to deriv…
Abstract We show that the syntactically rich notion of strictly positive families can be reduced to a core type theory with a fixed number of type constructors exploiting the novel notion of indexed containers. As a result, we show indexed containers provide normal forms for stri…