26,098 papers · page 262 of 1,305
Debugging is an essential part of software development. Numerous tools and techniques to improve debugging have been proposed in research or developed in the industry. However, only a few of those see widespread use, and debugging only rarely is a primary teaching subject. To pr…
Computer programming typically requires people to describe operations in a formally specified textual language. Unfortunately, working with syntax is a significant cognitive load, making programming difficult for beginners and time-consuming for professional developers. In respon…
We must retain liveness and exploratory practices within the programming systems that make us feel most productive. However, the temptation to just reuse black boxes through limited interfaces is pervasive. We expect time savings and better performance at the cost of poor repaira…
What is a conference for? What are its design considerations? What are the trade-offs between virtual and terrestrial meetings? Within these larger frame questions, this essay looks only at the following argument: The first critical step in research is the hypothesis—the novel i…
Object-oriented programming has been around for more than 50 years and is now the most dominant style of programming. In recent years there has been an increasing criticism of object-oriented programming. Some people argue that the mainstream object-oriented languages do not capt…
Programming is usually based on an inconvenient separation between an implementation level and a user level. Self-sustaining systems expose their implementation at their user level so that they can be modified and improved from within. However, the few examples that exist are tig…
Configurable software makes up most of the software in use today. Configurability, i.e., the ability of software to be customized without additional programming, is pervasive, and due to the criticality of problems caused by misconfiguration, it has been an active topic researche…
Abstract We implement extraction of Coq programs to functional languages based on MetaCoq’s certified erasure. We extend the MetaCoq erasure output language with typing information and use it as an intermediate representation, which we call ${\lambda^T_\square}$ . We complement t…
Abstract Functional reactive programming (FRP) provides a high-level interface for implementing reactive systems in a declarative manner. However, this high-level interface has to be carefully reigned in to ensure that programs can in fact be executed in practice. Specifically, o…
Abstract Gradual typing allows programs to enjoy the benefits of both static typing and dynamic typing. While it is often desirable to migrate a program from more dynamically typed to more statically typed or vice versa, gradual typing itself does not provide a way to facilitate …
Abstract In this paper, we introduce a tiered-priority scheme for a synchronous message-passing language with support for selective communication and first-class communication protocols. Crucially, our scheme allows higher priority threads to communicate with lower priority threa…
Abstract A standard informal method for analyzing the asymptotic complexity of a program is to extract a recurrence that describes its cost in terms of the size of its input and then to compute a closed-form upper bound on that recurrence. We give a formal account of that method …
Abstract Fold–unfold lemmas complement the rewrite tactic in the Coq Proof Assistant to reason about recursive functions, be they defined locally or globally. Each of the structural cases gives rise to a fold–unfold lemma that equates a call to this function in that case with the…
Abstract The Robert Harper Festschrift includes articles by three of Bob’s students and colleagues—Karl Crary, Andrzej Filinski, and Jonathan Sterling. Each of these articles touches on themes that are central to Bob’s research: module system design, proof-directed program develo…
The name has also been used for Steinitz numbers, or for numbers of the form 10 4n , both otherwise unconnected with the super-naturals described here.2 Defined in Numeric.Natural, a basic Haskell library. 3 In Haskell, symbolic data constructors, which are infix by default, must…
Many students complete PhDs in functional programming each year. As a service to the community, twice per year the Journal of Functional Programming publishes the abstracts from PhD dissertations completed during the previous year. The abstracts are made freely available on the J…
A dissertation is eligible for inclusion if parts of it have or could have appeared in JFP, that is, if it is in the general area of functional programming.The abstracts are not reviewed.
A dissertation is eligible for inclusion if parts of it have or could have appeared in JFP, that is, if it is in the general area of functional programming.The abstracts are not reviewed.
Abstract The vertex-centric programming model is now widely used for processing large graphs. User-defined vertex programs are executed in parallel over every vertex of a graph, but the imperative and explicit message-passing style of existing systems makes defining a vertex prog…