916 papers · page 14 of 46
Abstract Monadic second-order logic on finite words is a decidable yet expressive logic into which many decision problems can be encoded. Since MSO formulas correspond to regular languages, equivalence of MSO formulas can be reduced to the equivalence of some regular structures (…
Abstract Effective support for custom proof automation is essential for large-scale interactive proof development. However, existing languages for automation via tactics either (a) provide no way to specify the behavior of tactics within the base logic of the accompanying theorem…
Abstract Computational problems that involve dynamic data, such as physics simulations and program development environments, have been an important subject of study in programming languages. Building on this work, recent advances in self-adjusting computation have developed techn…
Abstract Programming with dependent types is a blessing and a curse. It is a blessing to be able to bake invariants into the definition of datatypes: We can finally write correct-by-construction software. However, this extreme accuracy is also a curse: A datatype is the combinati…
Abstract We give a framework for delimited control with multiple prompts, in the style of Parigot's λμ-calculus, through a series of incremental extensions by starting with the pure λ-calculus. Each language inherits the semantics and reduction theory of its parent, giving a syst…
Abstract Designing and implementing typed programming languages is hard. Every new type system feature requires extending the metatheory and implementation, which are often complicated and fragile. To ease this process, we would like to provide general mechanisms that subsume man…
Abstract We study the complexity of deciding the equality of streams specified by systems of equations. There are several notions of stream models in the literature, each generating a different semantics of stream equality. We pinpoint the complexity of each of these notions in t…
Over the past six months, we have transitioned to a new leadership team. We are now saying goodbye to Benjamin Pierce, who faithfully served as co-Editor in Chief since 2012, and welcome Jeremy Gibbons from the University of Oxford as new co-Editor in Chief.
Abstract Okasaki introduced the canonical formulation of functional red-black trees when he gave a concise, elegant method of persistent element insertion. Persistent element deletion, on the other hand, has not enjoyed the same treatment. For this reason, many functional impleme…
Many students complete PhDs in functional programming each year, but there is currently no common location in which to promote and advertise the resulting work. The Journal of Functional Programming would like to change that!
Realm of Racket, by Forrest Bice, Rose DeMaio, Spencer Florence, Feng-Yun Mimi Lin, Scott Lindeman, Nicole Nussbaum, Eric Peterson, Ryan Plessner, David Van Horn, Matthias Felleisen and Conrad Barski, MD, No Starch Press, San Franscisco, CA, 2013, £27.49. ISBN-10:1-59327-491-2. -…
Abstract In the static analysis of functional programs, pushdown flow analysis and abstract garbage collection push the boundaries of what we can learn about programs statically. This work illuminates and poses solutions to theoretical and practical challenges that stand in the w…
Abstract The Revised 6 Report on the Algorithmic Language Scheme added a mechanism to the Scheme programming language for creating new record types procedurally. While many programming languages support user defined, structured data types, these are usually handled syntactically,…
Abstract The higher-order logic found in proof assistants such as Coq and various HOL systems provides a convenient setting for the development and verification of functional programs. However, to efficiently run these programs, they must be converted (or ‘extracted’) to function…
One of the fundamental tasks of science is to find explainable relationships between observed phenomena. One approach to this task that has received attention in recent years is based on probabilistic graphical modelling with sparsity constraints on model structures. In this pape…
Abstract ML modules are a powerful language mechanism for decomposing programs into reusable components. Unfortunately, they also have a reputation for being “complex” and requiring fancy type theory that is mostly opaque to non-experts. While this reputation is certainly underst…
Abstract When writing transformation systems, a significant amount of engineering effort goes into setting up the infrastructure needed to direct individual transformations to specific targets in the data being transformed. Strategic programming languages provide general-purpose …
Abstract The worker/wrapper transformation is a general-purpose technique for refactoring recursive programs to improve their performance. The two previous approaches to formalising the technique were based upon different recursion operators and different correctness conditions. …