PhD Abstracts
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.
916 papers · page 5 of 46
Fregel: a functional domain-specific language for vertex-centric large-scale graph processing
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…
ANF preserves dependent types up to extensional equality
Abstract Many programmers use dependently typed languages such as Coq to machine-verify high-assurance software. However, existing compilers for these languages provide no guarantees after compiling, nor when linking after compilation. Type-preserving compilers preserve guarantee…
Iterating on multiple collections in synchrony
Abstract Modern programming languages typically provide some form of comprehension syntax which renders programs manipulating collection types more readable and understandable. However, comprehension syntax corresponds to nested loops in general. There is no simple way of using i…
Back to futures
Abstract Common approaches to concurrent programming begin with languages whose semantics are naturally sequential and add new constructs that provide limited access to concurrency, as exemplified by futures . This approach has been quite successful, but often does not provide a …
A well-known representation of monoids and its application to the function 'vector reverse'
Abstract Vectors—or length-indexed lists—are classic example of a dependent type. Yet, most tutorials stay clear of any function on vectors whose definition requires non-trivial equalities between natural numbers to type check. This pearl shows how to write functions, such as vec…
Segments: An alternative rainfall problem
Abstract Elliot Soloway’s Rainfall problem is a well-known and well-studied problem to investigate the problem-solving strategies of programmers. Kathi Fisler investigated this programming challenge from the point of view of functional programmers. She showed that this particular…
A trustful monad for axiomatic reasoning with probability and nondeterminism
The algebraic properties of the combination of probabilistic choice and nondeterministic choice have long been a research topic in program semantics. This paper explains a formalization in the Coq proof assistant of a monad equipped with both choices: the geometrically convex mon…
A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
Abstract The syntax of almost every programming language includes a notion of binder and corresponding bound occurrences, along with the accompanying notions of α-equivalence, capture-avoiding substitution, typing contexts, runtime environments, and so on. In the past, implementi…
Protocol combinators for modeling, testing, and execution of distributed systems
Abstract Distributed systems are hard to get right, model, test, debug, and teach. Their textbook definitions, typically given in a form of replicated state machines, are concise, yet prone to introducing programming errors if naïvely translated into runnable implementations. In …
A greedy algorithm for dropping digits
Abstract Consider the following puzzle: given a number, remove k digits such that the resulting number is as large as possible. Various techniques are employed to derive a linear-time solution to the puzzle: we justify the structure of a greedy algorithm by predicate logic, give …
Extensional equality preservation and verified generic programming
Abstract In verified generic programming, one cannot exploit the structure of concrete data types but has to rely on well chosen sets of specifications or abstract data types (ADTs). Functors and monads are at the core of many applications of functional programming. This raises t…
On the correctness of monadic backward induction
Abstract In control theory, to solve a finite-horizon sequential decision problem (SDP) commonly means to find a list of decision rules that result in an optimal expected total reward (or cost) when taking a given number of decision steps. SDPs are routinely solved using Bellman’…
Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code
Abstract Good tools can bring mechanical verification to programs written in mainstream functional languages. We use hs-to-coq to translate significant portions of Haskell’s containers library into Coq, and verify it against specifications that we derive from a variety of sources…
Integrating region memory management and tag-free generational garbage collection
Abstract We present a region-based memory management scheme with support for generational garbage collection. The scheme features a compile-time region inference algorithm, which associates values with logical regions, and builds on a region type system that deploys region types …
Explainable dynamic programming
Abstract In this paper, we present a method for explaining the results produced by dynamic programming (DP) algorithms. Our approach is based on retaining a granular representation of values that are aggregated during program execution. The explanations that are created from the …
Proof-directed program transformation: A functional account of efficient regular expression matching
Abstract We show how to systematically derive an efficient regular expression (regex) matcher using a variety of program transformation techniques, but very little specialized formal language and automata theory. Starting from the standard specification of the set-theoretic seman…
How to design co-programs
Abstract The observation that program structure follows data structure is a key lesson in introductory programming: good hints for possible program designs can be found by considering the structure of the data concerned. In particular, this lesson is a core message of the influen…
Taming the Merge Operator
Abstract Calculi with disjoint intersection types support a symmetric merge operator with subtyping. The merge operator generalizes record concatenation to any type, enabling expressive forms of object composition, and simple solutions to hard modularity problems. Unfortunately, …
PhD Abstracts
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.