Runtime Abstract Interpretation for Numerical Accuracy and Robustness
Abstract elided by the publisher.
26,098 papers · page 311 of 1,305
Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking
Abstract elided by the publisher.
Netter: Probabilistic, Stateful Network Models
Abstract elided by the publisher.
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.
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. The abstracts are made freely available on the J…
Not by equations alone: Reasoning with extensible effects
Abstract The challenge of reasoning about programs with (multiple) effects such as mutation, jumps, or IO dates back to the inception of program semantics in the works of Strachey and Landin. Using monads to represent individual effects and the associated equational laws to reaso…
What is an education paper?
We recently renamed our “education” track’s papers from Education Pearl to Education Matters. This would be a good time to explain our vision for the track as a whole, as well as this specific renaming.