title: Editorial - Special issue dedicated to ICFP 2010

authors:
Umut A. Acar
James Cheney
Stephanie Weirich

abstract: The 15th ACM SIGPLAN International Conference on Functional Programming (ICFP) took place on September 27–29, 2010 in Baltimore, Maryland. After the conference, the programme committee, chaired by Stephanie Weirich, selected several outstanding papers and invited their authors to submit to this special issue of Journal of Functional Programming . Umut A. Acar and James Cheney acted as editors for these submissions. This issue includes the seven accepted papers, each of which provides substantial new material beyond the original conference version. The selected papers reflect a consensus by the program committee that ICFP 2010 had a number of strong papers that link core functional programming ideas with other areas, such as multicore, embedded systems, and data compression.


venue: jfp

title: A compiled implementation of normalisation by evaluation

authors:
Klaus Aehlig
Florian Haftmann
Tobias Nipkow

abstract: Abstract We present a novel compiled approach to Normalisation by Evaluation (NBE) for ML-like languages. It supports efficient normalisation of open λ-terms with respect to β-reduction and rewrite rules. We have implemented NBE and show both a detailed formal model of our implementation and its verification in Isabelle. Finally we discuss how NBE is turned into a proof rule in Isabelle.


title: Lazy tree splitting

authors:
Lars Bergstrom
Matthew Fluet
Mike Rainey
John H. Reppy
Adam Shaw

abstract: Abstract Nested data-parallelism (NDP) is a language mechanism that supports programming irregular parallel applications in a declarative style. In this paper, we describe the implementation of NDP in Parallel ML (PML), which is a part of the Manticore system. One of the main challenges of implementing NDP is managing the parallel decomposition of work. If we have too many small chunks of work, the overhead will be too high, but if we do not have enough chunks of work, processors will be idle. Recently, the technique of Lazy Binary Splitting was proposed to address this problem for nested parallel loops over flat arrays. We have adapted this technique to our implementation of NDP, which uses binary trees to represent parallel arrays. This new technique, which we call Lazy Tree Splitting (LTS), has the key advantage of performance robustness , i.e., it does not require tuning to get the best performance for each program. We describe the implementation of the standard NDP operations using LTS and present experimental data that demonstrate the scalability of LTS across a range of benchmarks.


title: Proofs for free - Parametricity for dependent types

authors:
Jean-Philippe Bernardy
Patrik Jansson
Ross Paterson

abstract: Abstract Reynolds' abstraction theorem (Reynolds, J. C. (1983) Types, abstraction and parametric polymorphism, Inf. Process. 83 (1), 513–523) shows how a typing judgement in System F can be translated into a relational statement (in second-order predicate logic) about inhabitants of the type. We obtain a similar result for pure type systems (PTSs): for any PTS used as a programming language, there is a PTS that can be used as a logic for parametricity. Types in the source PTS are translated to relations (expressed as types) in the target. Similarly, values of a given type are translated to proofs that the values satisfy the relational interpretation. We extend the result to inductive families. We also show that the assumption that every term satisfies the parametricity condition generated by its type is consistent with the generated logic.


title: Semantic subtyping with an SMT solver

authors:
Gavin M. Bierman
Andrew D. Gordon
Catalin Hritcu
David E. Langworthy

abstract: Abstract We study a first-order functional language with the novel combination of the ideas of refinement type (the subset of a type to satisfy a Boolean expression) and type-test (a Boolean expression testing whether a value belongs to a type). Our core calculus can express a rich variety of typing idioms; for example, intersection, union, negation, singleton, nullable, variant, and algebraic types are all derivable. We formulate a semantics in which expressions denote terms, and types are interpreted as first-order logic formulas. Subtyping is defined as valid implication between the semantics of types. The formulas are interpreted in a specific model that we axiomatize using standard first-order theories. On this basis, we present a novel type-checking algorithm able to eliminate many dynamic tests and to detect many errors statically. The key idea is to rely on a Satisfiability Modulo Theories solver to compute subtyping efficiently. Moreover, using a satisfiability modulo theories solver allows us to show the uniqueness of normal forms for non-deterministic expressions, provide precise counterexamples when type-checking fails, detect empty types, and compute instances of types statically and at run-time.


title: Modeling in Event-B - System and Software Engineering Jean-Raymond Abrial Cambridge University Press, May 2010 ISBN-10: 0521895561


title: Functional Programming for Java Developers - Tools for Better Concurrency, Abstraction, and Agility, By Wampler, Media, July 2011, ISBN-13: 978-1449311032, 90pp


title: Steps in Scala: An introduction to Object-Functional Programming By Loverdos, Apostolos Syropoulos, Cambridge University Press, 2010, 504 pp, ISBN 0521747589


title: Fortifying macros

abstract: Abstract Existing macro systems force programmers to make a choice between clarity of specification and robustness. If they choose clarity, they must forgo validating significant parts of the specification and thus produce low-quality language extensions. If they choose robustness, they must write in a style that mingles the implementation with the specification and therefore obscures the latter. This paper introduces a new language for writing macros. With the new macro system, programmers naturally write robust language extensions using easy-to-understand specifications. The system translates these specifications into validators that detect misuses—including violations of context-sensitive constraints—and automatically synthesize appropriate feedback, eliminating the need for ad hoc validation code.


title: Finally tagless observable recursion for an abstract grammar model

authors:
Dominique Devriese
Frank Piessens

abstract: Abstract We define a finally tagless, shallow embedding of a typed grammar language. In order to avoid the limitations of traditional parser combinator libraries (no bottom-up parsing, no full grammar analysis or transformation), we require object-language recursion to be observable in the meta-language. Since existing proposals for recursive constructs are not fully satisfactory, we propose new finally tagless primitive recursive constructs to solve the problem. To do this in a well-typed way, we require considerable infrastructure, for which we reuse techniques from the multirec generic programming library. Our infrastructure allows a precise model of the complex interaction between a grammar, a parsing algorithm and a set of semantic actions. On the flip side, our approach requires the grammar author to provide a type- and value-level encoding of the grammar's domain and we can provide only a limited form of constructs like many . We demonstrate five meta-language grammar algorithms exploiting our model, including a grammar pretty-printer, a reachability analysis, a translation of quantified recursive constructs to the standard one and an implementation of the left-corner grammar transform. The work we present forms the basis of the grammar-combinators parsing library 1 , which is the first to work with a precise, shallow model of abstract context-free grammars in a classical (not dependently typed) functional language and which supports a wide range of grammar manipulation primitives. From a more general point of view, our work shows a solution to the well-studied problem of observable sharing in shallowly embedded domain-specific languages and specifically in finally tagless domain-specific languages.


title: The impact of higher-order state and control effects on local relational reasoning

authors:
Derek Dreyer
Georg Neis
Lars Birkedal

abstract: Abstract Reasoning about program equivalence is one of the oldest problems in semantics. In recent years, useful techniques have been developed, based on bisimulations and logical relations, for reasoning about equivalence in the setting of increasingly realistic languages—languages nearly as complex as ML or Haskell. Much of the recent work in this direction has considered the interesting representation independence principles enabled by the use of local state, but it is also important to understand the principles that powerful features like higher-order state and control effects disable . This latter topic has been broached extensively within the framework of game semantics, resulting in what Abramsky dubbed the “semantic cube”: fully abstract game-semantic characterizations of various axes in the design space of ML-like languages. But when it comes to reasoning about many actual examples, game semantics does not yet supply a useful technique for proving equivalences. In this paper, we marry the aspirations of the semantic cube to the powerful proof method of step-indexed Kripke logical relations . Building on recent work of Ahmed et al . (2009), we define the first fully abstract logical relation for an ML-like language with recursive types, abstract types, general references and call/cc. We then show how, under orthogonal restrictions to the expressive power of our language—namely, the restriction to first-order state and/or the removal of call/cc—we can enhance the proving power of our possible-worlds model in correspondingly orthogonal ways, and we demonstrate this proving power on a range of interesting examples. Central to our story is the use of state transition systems to model the way in which properties of local state evolve over time.


title: Editorial

abstract: With this issue of the Journal of Functional Programming , we transition to a new leadership. Xavier Leroy, who has faithfully served as co-Editor in Chief since 2007, is stepping down. After a short apprenticeship over the past year, Benjamin Pierce is taking his place.


title: Macros that Work Together - Compile-time bindings, partial expansion, and definition contexts

authors:
Matthew Flatt
Ryan Culpepper
David Darais
Robert Bruce Findler

abstract: Abstract Racket is a large language that is built mostly within itself. Unlike the usual approach taken by non-Lisp languages, the self-hosting of Racket is not a matter of bootstrapping one implementation through a previous implementation, but instead a matter of building a tower of languages and libraries via macros. The upper layers of the tower include a class system, a component system, pedagogic variants of Scheme, a statically typed dialect of Scheme, and more. The demands of this language-construction effort require a macro system that is substantially more expressive than previous macro systems. In particular, while conventional Scheme macro systems handle stand-alone syntactic forms adequately, they provide weak support for macros that share information or macros that use existing syntactic forms in new contexts. This paper describes and models features of the Racket macro system, including support for general compile-time bindings, sub-form expansion and analysis, and environment management. The presentation assumes a basic familiarity with Lisp-style macros, and it takes for granted the need for macros that respect lexical scope. The model, however, strips away the pattern and template system that is normally associated with Scheme macros, isolating a core that is simpler, can support pattern and template forms themselves as macros, and generalizes naturally to Racket's other extensions.


title: Contracts made manifest

authors:
Michael Greenberg
Benjamin C. Pierce
Stephanie Weirich

abstract: Abstract Since Findler and Felleisen (Findler, R. B. & Felleisen, M. 2002) introduced higher-order contracts , many variants have been proposed. Broadly, these fall into two groups: some follow Findler and Felleisen (2002) in using latent contracts, purely dynamic checks that are transparent to the type system; others use manifest contracts, where refinement types record the most recent check that has been applied to each value. These two approaches are commonly assumed to be equivalent—different ways of implementing the same idea, one retaining a simple type system, and the other providing more static information. Our goal is to formalize and clarify this folklore understanding. Our work extends that of Gronski and Flanagan (Gronski, J. & Flanagan, C. 2007), who defined a latent calculus λ C and a manifest calculus λ H , gave a translation φ from λ C to λ H , and proved that if a λ C term reduces to a constant, so does its φ-image. We enrich their account with a translation ψ from λ H to λ C and prove an analogous theorem. We then generalize the whole framework to dependent contracts , whose predicates can mention free variables. This extension is both pragmatically crucial, supporting a much more interesting range of contracts, and theoretically challenging. We define dependent versions of λ H and two dialects (“lax” and “picky”) of λ C , establish type soundness—a substantial result in itself, for λ H — and extend φ and ψ accordingly. Surprisingly, the intuition that the latent and manifest systems are equivalent now breaks down: the extended translations preserve behavior in one direction, but in the other, sometimes yield terms that blame more.


title: Bookreview JFP: Domain-Specific Languages by Martin Fowler The Addison Wesley Signature Series

abstract: My main reason for wanting to read this book was to find out what a well-known publicist from the world of OO would have to say about the state of the art of domain specific languages (DSLs), in particular when it comes to type error feedback, functional programming, and the combination. As most readers will be aware, languages like Scheme and Haskell are very well suited to embed DSLs in: Scheme can be considered a core language to which new language facilities can be easily added by means of hygienic syntax macro's (Abelson et al . 1998), and there are so many papers on embedded DSLs in Haskell (Hudak, 1998), that any realistic selection would aggravate more people than I would please. Great was my disappointment when I read on page XXV that these topics were not discussed at all in the book. Although I can imagine that Fowler does not feel comfortable writing about subjects he is not sufficiently at home with, the question does arise whether the title of this book is sufficiently covered by its contents.


title: Generic top-down discrimination for sorting and partitioning in linear time

abstract: Abstract We introduce the notion of discrimination as a generalization of both sorting and partitioning, and show that discriminators (discrimination functions) can be defined generically , by structural recursion on representations of ordering and equivalence relations . Discriminators improve the asymptotic performance of generic comparison-based sorting and partitioning, and can be implemented not to expose more information than the underlying ordering, respectively equivalence relation. For a large class of order and equivalence representations, including all standard orders for regular recursive first-order types, the discriminators execute in the worst-case linear time. The generic discriminators can be coded compactly using list comprehensions, with order and equivalence representations specified using Generalized Algebraic Data Types. We give some examples of the uses of discriminators, including the most-significant digit lexicographic sorting, type isomorphism with an associative-commutative operator, and database joins. Source code of discriminators and their applications in Haskell is included. We argue that built-in primitive types, notably pointers (references), should come with efficient discriminators, not just equality tests, since they facilitate the construction of discriminators for abstract types that are both highly efficient and representation-independent.


title: Systematic abstraction of abstract machines

authors:
David Van Horn
Matthew Might

abstract: Abstract We describe a derivational approach to abstract interpretation that yields novel and transparently sound static analyses when applied to well-established abstract machines for higher-order and imperative programming languages. To demonstrate the technique and support our claim, we transform the CEK machine of Felleisen and Friedman ( Proc. of the 14th ACM SIGACT-SIGPLAN Symp. Prin. Program. Langs , 1987, pp. 314–325), a lazy variant of Krivine's machine ( Higher-Order Symb. Comput. Vol 20, 2007, pp. 199–207), and the stack-inspecting CM machine of Clements and Felleisen ( ACM Trans. Program. Lang. Syst. Vol 26, 2004, pp. 1029–1052) into abstract interpretations of themselves. The resulting analyses bound temporal ordering of program events; predict return-flow and stack-inspection behavior; and approximate the flow and evaluation of by-need parameters. For all of these machines, we find that a series of well-known concrete machine refactorings, plus a technique of store-allocated continuations, leads to machines that abstract into static analyses simply by bounding their stores. These machines are parameterized by allocation functions that tune performance and precision and substantially expand the space of analyses that this framework can represent. We demonstrate that the technique scales up uniformly to allow static analysis of realistic language features, including tail calls, conditionals, mutation, exceptions, first-class continuations, and even garbage collection. In order to close the gap between formalism and implementation, we provide translations of the mathematics as running Haskell code for the initial development of our method.


title: Every bit counts: The binary representation of typed data and programs

authors:
Andrew J. Kennedy
Dimitrios Vytiniotis

abstract: Abstract We show how the binary encoding and decoding of typed data and typed programs can be understood, programmed and verified with the help of question–answer games. The encoding of a value is determined by the yes/no answers to a sequence of questions about that value; conversely, decoding is the interpretation of binary data as answers to the same question scheme. We introduce a general framework for writing and verifying game-based codecs. We present games in Haskell for structured, recursive, polymorphic and indexed types, building up to a representation of well-typed terms in the simply-typed λ-calculus with polymorphic constants. The framework makes novel use of isomorphisms between types in the definition of games. The definition of isomorphisms together with additional simple properties make it easy to prove that codecs derived from games never encode two distinct values using the same code, never decode two codes to the same value and interpret any bit sequence as a valid code for a value or as a prefix of a valid code. Formal properties of the framework have been proved using the Coq proof assistant.


title: Drawing Programs: The Theory and Practice of Schematic Functional Programming, by Tom Addis and Jan Addis Springer, 2010, ISBN 978-1-84882-617-5, 379pp

abstract: Overall, this book contains a lot of valuable material, and due to the simplicity of the Event-B notation it should be a seriously considered for introductory courses on formal modelling with associated proof.As a basis for advanced study and research, it would be significantly better if it contained more conceptual clarity and methodological guidance on refinement, as well as a much more extensive index and bibliographic information.The case studies, however, still provide a rich source of example material for researchers.


title: CUFP 2011 Workshop Report

authors:
Anil Madhavapeddy
Yaron Minsky
Marius Eriksen

abstract: Commercial Users of Functional Programming (CUFP) is a yearly workshop that is aimed at the community of software developers who use functional programming in real-world settings. This scribe report covers the talks that were delivered at the 2011 workshop, which was held in association with ICFP in Tokyo. The goal of the report is to give the reader a sense of what went on, rather than to reproduce the full details of the talks. Videos and slides from all the talks are available online at http://cufp.org .


title: Manipulating accumulative functions by swapping call-time and return-time computations

authors:
Akimasa Morihata
Kazuhiko Kakehi
Zhenjiang Hu
Masato Takeichi

abstract: Abstract Functional languages are suitable for transformational developments of programs. However, accumulative functions, or in particular tail-recursive functions, are known to be less suitable for manipulation. In this paper, we propose a program transformation named “IO swapping” that swaps call-time and return-time computations. It moves computations in accumulative parameters to results and thereby enables interesting transformations. We demonstrate effectiveness of IO swapping by several applications: deforestation, higher order removal, program inversion, and manipulation of circular programs.


title: The Reduceron reconfigured and re-evaluated

authors:
Matthew Naylor
Colin Runciman

abstract: Abstract A new version of a special-purpose processor for running lazy functional programs is presented. This processor – the Reduceron – exploits parallel memories and dynamic analyses to increase evaluation speed, and is implemented using reconfigurable hardware. Compared to a more conventional functional language implementation targeting a standard RISC processor running on the same reconfigurable hardware, the Reduceron offers a significant improvement in run-time performance.


title: MRI: Modular reasoning about interference in incremental programming

authors:
Bruno C. d. S. Oliveira
Tom Schrijvers
William R. Cook

abstract: Abstract Incremental Programming (IP) is a programming style in which new program components are defined as increments of other components. Examples of IP mechanisms include Object-oriented programming inheritance, aspect-oriented programming advice, and feature-oriented programming . A characteristic of IP mechanisms is that, while individual components can be independently defined, the composition of components makes those components become tightly coupled, sharing both control and data flows. This makes reasoning about IP mechanisms a notoriously hard problem: modular reasoning about a component becomes very difficult; and it is very hard to tell if two tightly coupled components interfere with each other's control and data flows. This paper presents modular reasoning about interference (MRI), a purely functional model of IP embedded in Haskell. MRI models inheritance with mixins and side effects with monads. It comes with a range of powerful reasoning techniques: equational reasoning, parametricity, and reasoning with algebraic laws about effectful operations. These techniques enable MRI in the presence of side effects. MRI formally captures harmlessness , a hard-to-formalize notion in the interference literature, in two theorems. We prove these theorems with a non-trivial combination of all three reasoning techniques.


title: A unified treatment of syntax with binders

authors:
Nicolas Pouillard
François Pottier

abstract: Abstract Atoms and de Bruijn indices are two well-known representation techniques for data structures that involve names and binders. However, using either technique, it is all too easy to make a programming error that causes one name to be used where another was intended. We propose an abstract interface to names and binders that rules out many of these errors. This interface is implemented as a library in Agda . It allows defining and manipulating term representations in nominal style and in de Bruijn style. The programmer is not forced to choose between these styles: on the contrary, the library allows using both styles in the same program, if desired. Whereas indexing the types of names and terms with a natural number is a well-known technique to better control the use of de Bruijn indices, we index types with worlds. Worlds are at the same time more precise and more abstract than natural numbers. Via logical relations and parametricity, we are able to demonstrate in what sense our library is safe, and to obtain theorems for free about world-polymorphic functions. For instance, we prove that a world-polymorphic term transformation function must commute with any renaming of the free variables. The proof is entirely carried out in Agda .


title: Pure Type System conversion is always typable

authors:
Vincent Siles
Hugo Herbelin

abstract: Abstract Pure Type Systems are usually described in two different ways, one that uses an external notion of computation like beta-reduction, and one that relies on a typed judgment of equality, directly in the typing system. For a long time, the question was open to know whether both presentations described the same theory. A first step towards this equivalence has been made by Adams for a particular class of Pure Type Systems (PTS) called functional. Then, his result has been relaxed to all semi-full PTSs in previous work. In this paper, we finally give a positive answer to the general question, and prove that equivalence holds for any Pure Type System.


title: When Maybe is not good enough

abstract: Many variations upon the theme of parser combinators have been proposed, too many to list here, but the main idea is simple: A parser for phrases of type α is a function that takes an input string and produces results ( x, rest ), where x is a value of type α, and rest is the remainder of the input after the phrase with value x has been consumed. The results are often arranged into a list, because this allows a parser to signal failure with the empty list of results, an unambiguous success with one result, or multiple possibilities with a longer ‘list of successes’.


title: A consistent semantics of self-adjusting computation

authors:
Umut A. Acar
Matthias Blume
Jacob Donham

abstract: Abstract This paper presents a semantics of self-adjusting computation and proves that the semantics is correct and consistent. The semantics introduces memoizing change propagation, which enhances change propagation with the classic idea of memoization to enable reuse of computations even when memory is mutated via side effects. During evaluation, computation reuse via memoization triggers a change-propagation algorithm that adapts the reused computation to the memory mutations (side effects) that took place since the creation of the computation. Since the semantics includes both memoization and change propagation, it involves both non-determinism (due to memoization) and mutation (due to change propagation). Our consistency theorem states that the non-determinism is not harmful: any two evaluations of the same program starting at the same state yield the same result. Our correctness theorem states that mutation is not harmful: Self-adjusting programs are compatible with purely functional programming. We formalize the semantics and its meta-theory in the LF logical framework and machine check our proofs using Twelf.


title: EditorArrow: An arrow-based model for editor-based programming

authors:
Peter Achten
Marko C. J. D. van Eekelen
Maarten de Mol
Rinus Plasmeijer

abstract: Abstract State-based interactive applications, whether they run on the desktop or as a web application, can be considered as collections of interconnected editors of structured values that allow users to manipulate data. This is the view that is advocated by the GEC and iData toolkits, which offer a high level of abstraction to programming desktop and web GUI applications respectively. Special features of these toolkits are that editors have shared , persistent state, and that they handle events individually. In this paper we cast these toolkits within the Arrow framework and present EditorArrow : a single, unified semantic model that defines shared state and event handling. We study the properties of EditorArrow , and of editors in particular. Furthermore, we present the definedness properties of the combinators. A reference implementation of the EditorArrow model is given with some small program examples. We discuss formal reasoning about the model using the proof assistant Sparkle . The availability of this tool has proved to be indispensable in this endeavor.


title: Special Issue Dedicated to ICFP 2011 Editorial

authors:
Kenichi Asai
Benjamin C. Pierce

abstract: The 16th ACM SIGPLAN International Conference on Functional Programming (ICFP) took place on September 19–21, 2011 in Tokyo, Japan. After the conference, the programme committee, chaired by Olivier Danvy, selected several outstanding papers and invited their authors to submit to this special issue of the Journal of Functional Programming . Kenichi Asai and Benjamin C. Pierce acted as editors for these submissions. This issue includes the three accepted articles, each of which provides substantial new material beyond the original conference version. The selected papers represent the importance of various aspects of proof techniques, from theory to practice, all of which aim at verifying realistic programs.


title: An in-situ algorithm for expanding a graph

abstract: This pearl is devoted to a problem posed by Don Knuth about how to justify a certain array-based algorithm for changing the way an undirected graph is represented. In order to set the scene, we delay describing the precise problem until Section 4. Knuth (2011) recorded three different solutions, though no proofs of correctness were provided, nor even much explanation of why they worked. Recently, he asked various computer scientists interested in formal program development whether any of the proposed solutions “could have been discovered in a disciplined manner.” In what follows we respond by developing a purely functional solution. The solution makes heavy use of the operations in the Haskell library Data . Array , and the whole exercise turns out to be a fascinating study of the arithmetic of graphs and arrays. One of the conditions of the problem is that the final algorithm has to be in situ , but we will get to that in due course.


title: Idris, a general-purpose dependently typed programming language: Design and implementation

abstract: Abstract Many components of a dependently typed programming language are by now well understood, for example, the underlying type theory, type checking, unification and evaluation. How to combine these components into a realistic and usable high-level language is, however, folklore, discovered anew by successive language implementors. In this paper, I describe the implementation of Idris , a new dependently typed functional programming language. Idris is intended to be a general-purpose programming language and as such provides high-level concepts such as implicit syntax, type classes and do notation. I describe the high-level language and the underlying type theory, and present a tactic-based method for elaborating concrete high-level syntax with implicit arguments and type classes into a fully explicit type theory. Furthermore, I show how this method facilitates the implementation of new high-level language constructs.


title: Building Web Applications with Erlang, by Zachary Kessin, O'Reilly Media, Inc., 2012, ISBN 97-81-4493-20652


title: How to make ad hoc proof automation less ad hoc

authors:
Georges Gonthier
Beta Ziliani
Aleksandar Nanevski
Derek Dreyer

abstract: Abstract Most interactive theorem provers provide support for some form of user-customizable proof automation. In a number of popular systems, such as Coq and Isabelle, this automation is achieved primarily through tactics , which are programmed in a separate language from that of the prover's base logic. While tactics are clearly useful in practice, they can be difficult to maintain and compose because, unlike lemmas, their behavior cannot be specified within the expressive type system of the prover itself. We propose a novel approach to proof automation in Coq that allows the user to specify the behavior of custom automated routines in terms of Coq's own type system. Our approach involves a sophisticated application of Coq's canonical structures , which generalize Haskell type classes and facilitate a flexible style of dependently-typed logic programming. Specifically, just as Haskell type classes are used to infer the canonical implementation of an overloaded term at a given type, canonical structures can be used to infer the canonical proof of an overloaded lemma for a given instantiation of its parameters. We present a series of design patterns for canonical structure programming that enable one to carefully and predictably coax Coq's type inference engine into triggering the execution of user-supplied algorithms during unification, and we illustrate these patterns through several realistic examples drawn from Hoare Type Theory. We assume no prior knowledge of Coq and describe the relevant aspects of Coq type inference from first principles.


title: Modular verification of preemptive OS kernels

authors:
Alexey Gotsman
Hongseok Yang

abstract: Abstract Most major OS kernels today run on multiprocessor systems and are preemptive: it is possible for a process running in the kernel mode to get descheduled. Existing modular techniques for verifying concurrent code are not directly applicable in this setting: they rely on scheduling being implemented correctly, and in a preemptive kernel, the correctness of the scheduler is interdependent with the correctness of the code it schedules. This interdependency is even stronger in mainstream kernels, such as those of Linux, FreeBSD or Mac OS X, where the scheduler and processes interact in complex ways. We propose the first logic that is able to decompose the verification of preemptive multiprocessor kernel code into verifying the scheduler and the rest of the kernel separately, even in the presence of complex interdependencies between the two components. The logic hides the manipulation of control by the scheduler when reasoning about preemptable code and soundly inherits proof rules from concurrent separation logic to verify it thread-modularly. We illustrate the power of our logic by verifying an example scheduler, which includes some of the key features of the scheduler from Linux 2.6.11 challenging for verification.


title: Counting and generating lambda terms

authors:
Katarzyna Grygiel
Pierre Lescanne

abstract: Abstract Lambda calculus is the basis of functional programming and higher order proof assistants. However, little is known about combinatorial properties of lambda terms, in particular, about their asymptotic distribution and random generation. This paper tries to answer questions like: How many terms of a given size are there? What is a ‘typical’ structure of a simply typable term? Despite their ostensible simplicity, these questions still remain unanswered, whereas solutions to such problems are essential for testing compilers and optimizing programs whose expected efficiency depends on the size of terms. Our approach toward the aforementioned problems may be later extended to any language with bound variables, i.e., with scopes and declarations. This paper presents two complementary approaches: one, theoretical, uses complex analysis and generating functions, the other, experimental, is based on a generator of lambda terms. Thanks to de Bruijn indices (de Bruijn, N. (1972) Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagat. Math. 34 (5), 381–392), we provide three families of formulas for the number of closed lambda terms of a given size and we give four relations between these numbers which have interesting combinatorial interpretations. As a by-product of the counting formulas, we design an algorithm for generating λ-terms. Performed tests provide us with experimental data, like the average depth of bound variables and the average number of head lambdas. We also create random generators for various sorts of terms. Thereafter, we conduct experiments that answer questions like: What is the ratio of simply typable terms among all terms? ( Very small! ) How are simply typable lambda terms distributed among all lambda terms? ( A typable term almost always starts with an abstraction .) In this paper, abstractions and applications have size 1 and variables have size 0.


title: Solving the snake cube puzzle in Haskell

abstract: Abstract We describe a concise and elegant functional program, written in Haskell, that computes solutions for a classic puzzle known as the “snake cube.” The program reflects some of the fundamental characteristics of the functional style, identifying key abstractions, and defining a small collection of operators for manipulating and working with the associated values. Well-suited for an introductory course on functional programming, this example highlights the use of visualization tools to explain and demonstrate the choices of data structures and algorithms that are used in the development.


title: Contextual equivalence for inductive definitions with binders in higher order typed functional programming

authors:
Matthew R. Lakin
Andrew M. Pitts

abstract: Abstract Correct handling of names and binders is an important issue in meta-programming. This paper presents an embedding of constraint logic programming into the αML functional programming language, which provides a provably correct means of implementing proof search computations over inductive definitions involving names and binders modulo α-equivalence. We show that the execution of proof search in the αML operational semantics is sound and complete with regard to the model-theoretic semantics of formulae, and develop a theory of contextual equivalence for the subclass of αML expressions which correspond to inductive definitions and formulae. In particular, we prove that αML expressions, which denote inductive definitions, are contextually equivalent precisely when those inductive definitions have the same model-theoretic semantics. This paper is a revised and extended version of the conference paper (Lakin, M. R. & Pitts, A. M. (2009) Resolving inductive definitions with binders in higher-order typed functional programming. In Proceedings of the 18th European Symposium on Programming (ESOP 2009) , Castagna, G. (ed), Lecture Notes in Computer Science, vol. 5502. Berlin, Germany: Springer-Verlag, pp. 47–61) and draws on material from the first author's PhD thesis (Lakin, M. R. (2010) An Executable Meta-Language for Inductive Definitions with Binders . University of Cambridge, UK).


title: Fractal image compression

authors:
C. E. Martin
S. A. Curtis

abstract: Abstract This paper describes some experiences of using fractal image compression as the subject of an assignment for a functional programming course using Haskell. The students were fascinated by the reproduction of images from their encodings and engaged well with the exercise which involved only elementary functional programming techniques.


title: Learn You a Haskell for Great Good! A Beginner's Guide, by Miran Lipovaca, No Starch Press, April 2011, ISBN-10: 1593272839; ISBN-13: 978-1593272838, 376 pp

abstract: The first thing that you will notice about this book is the clunky how-foreigners-speak-English title.And the second is the clunky illustration style.Of course, the word "clunky" demonstrates either my high-mindedness or my pomposity.Either way, these tropes really got in the way of my taking this book as seriously as it deserved."Comic" books on programming languages actually have a long pedigree.Kaufman's A FORTRAN Coloring Book has a Dr Seuss-ish feel.I used Alcock's Illustrating Basic (1977) for many years to teach non-specialists with the BBC Microcomputer.In our own noble discipline, Friedman's The Little LISPer (1974) predates both.In turn, this has spawned Friedman and Felleisen's The Little Schemer (1998) and Little MLer (1998).These older books have a gently whimsical feel.In contrast, I found Learn You a Haskell. . .considerably more abrasive in tone.Weak puns abound, as do geek culture references, for example to Mission Impossible and Star Trek and Terry Pratchett and spaghetti westerns."Stuff" is "cool."The "maximum" function is "awesome."We take a journey to "the top of Monad Mountain."Perhaps, the target readership will warm to this. 1 Luckily, for me at any rate, the author does not maintain this style throughout: most of the book is thoughtful and well-written.I think the illustrations also lack the charm of those in the earlier books.At best, they are mildly cute.At worst, they are offensive, in particular the scantily clad, curvaceous woman on p. 102 accompanying a phone book example, which only contains female names.Indeed, one of the few other representations of women, among a plethora of men and animals, is the "old lady" on p. 95.Really, sexism is not funny.This is 21st century: gender neutrality should be taken for granted in academic computing.Now, there is a generic problem with books about specific programming languages, or perhaps a family of problems.Do they assume that the reader already knows how to program in some other language?If so, which language?If not, then do they seek to teach some pedagogy of programming?If so, then which pedagogy?Learn You a Haskell. . . is aimed at readers with imperative programming experience in, say C++, Java, or Python.At the start, there is a very brief summary of key functional programming concepts from an imperative perspective.Thereafter, the book dives straight into interactive GHCi use and is driven by Haskell constructs.Thus, no clear discipline is offered to marshal an initial myriad of techniques to solve substantial problems.Of course, this is a fault of many functional programming texts, my own included.Overall, though, I think this book might prove hard going for self-study except for experienced programmers.Nonetheless, the book is well suited to accompany a taught course on Haskell, offering a strong and systematic emphasis throughout on the central notions of types and higher order constructs.Topics in functional programming, such as recursion, type polymorphism,


title: Pearls of Functional Algorithm Design, by Richard Bird, Cambridge University Press, September 2010, £35.00, US $ 60.00. ISBN: 978052151338 (hardback), 286pp


title: Metamorphism in jigsaw

abstract: Abstract A metamorphism is an unfold after a fold, consuming an input by the fold then generating an output by the unfold. It is typically useful for converting data representations, e.g., radix conversion of numbers. (Bird and Gibbons, Lecture Notes in Computer Science, vol. 2638, 2003, pp. 1–26) have shown that metamorphisms can be incrementally processed in streaming style when a certain condition holds because part of the output can be determined before the whole input is given. However, whereas radix conversion of fractions is amenable to streaming, radix conversion of natural numbers cannot satisfy the condition because it is impossible to determine part of the output before the whole input is completed. In this paper, we present a jigsaw model in which metamorphisms can be partially processed for outputs even when the streaming condition does not hold. We start with how to describe the 3-to-2 radix conversion of natural numbers using our model. The jigsaw model allows us to process metamorphisms in a flexible way that includes parallel computation. We also apply our model to other examples of metamorphisms.


title: An insider's look at LF type reconstruction: everything you (n)ever wanted to know

abstract: Abstract Although type reconstruction for dependently typed languages is common in practical systems, it is still ill-understood. Detailed descriptions of the issues around it are hard to find and formal descriptions together with correctness proofs are non-existing. In this paper, we discuss a one-pass type reconstruction for objects in the logical framework LF, describe formally the type reconstruction process using the framework of contextual modal types, and prove correctness of type reconstruction. Since type reconstruction will find most general types and may leave free variables, we in addition describe abstraction which will return a closed object where all free variables are bound at the outside. We also implemented our algorithms as part of the Beluga language, and the performance of our type reconstruction algorithm is comparable to type reconstruction in existing systems such as the logical framework Twelf.


title: Syntactic soundness proof of a type-and-capability system with hidden state

abstract: Abstract This paper presents a formal definition and machine-checked soundness proof for a very expressive type-and-capability system, that is, a low-level type system that keeps precise track of ownership and side effects. The programming language has first-class functions and references. The type system's features include the following: universal, existential, and recursive types; subtyping; a distinction between affine and unrestricted data; support for strong updates; support for naming values and heap fragments via singleton and group regions; a distinction between ordinary values (which exist at runtime) and capabilities (which do not); support for dynamic reorganizations of the ownership hierarchy by disassembling and reassembling capabilities; and support for temporarily or permanently hiding a capability via frame and anti-frame rules. One contribution of the paper is the definition of the type-and-capability system itself. We present the system as modularly as possible. In particular, at the core of the system, the treatment of affinity, in the style of dual intuitionistic linear logic, is formulated in terms of an arbitrary monotonic separation algebra , a novel axiomatization of resources, ownership, and the manner in which they evolve with time. Only the peripheral layers of the system are aware that we are dealing with a specific monotonic separation algebra, whose resources are references and regions. This semi-abstract organization should facilitate further extensions of the system with new forms of resources. The other main contribution is a machine-checked proof of type soundness. The proof is carried out in the Wright and Felleisen's syntactic style. This offers an evidence that this relatively simple-minded proof technique can scale up to systems of this complexity, and constitutes a viable alternative to more sophisticated semantic proof techniques. We do not claim that the syntactic technique is superior: We simply illustrate how it is used and highlight its strengths and shortcomings.


title: OCaml from the Very Beginning, by John Whitington, Coherent Press, 2013, £ 25.99, US $37.99. ISBN-10: 0957671105 (paperback), 204 pp


title: Commercial users of functional programming workshop report

authors:
Michael Sperber
Anil Madhavapeddy

abstract: Commercial Users of Functional Programming (CUFP) is an annual workshop that is aimed at the community of software developers who use functional programming in real-world settings. This scribe report covers the talks that were delivered at the 2012 workshop, which was held in association with International Conference on Functional Programming (ICFP) in Copenhagen, Denmark. The goal of the report is to give the reader a sense of what went on, rather than to reproduce the full details of the talks. Videos and slides from all the talks are available online at http://cufp.org.


title: Secure distributed programming with value-dependent types

authors:
Nikhil Swamy
Juan Chen
Cédric Fournet
Pierre-Yves Strub
Karthikeyan Bhargavan
Jean Yang

abstract: Abstract Distributed applications are difficult to program reliably and securely. Dependently typed functional languages promise to prevent broad classes of errors and vulnerabilities, and to enable program verification to proceed side-by-side with development. However, as recursion, effects, and rich libraries are added, using types to reason about programs, specifications, and proofs becomes challenging. We present F*, a full-fledged design and implementation of a new dependently typed language for secure distributed programming. Our language provides arbitrary recursion while maintaining a logically consistent core; it enables modular reasoning about state and other effects using affine types; and it supports proofs of refinement properties using a mixture of cryptographic evidence and logical proof terms. The key mechanism is a new kind system that tracks several sub-languages within F* and controls their interaction. F* subsumes two previous languages, F7 and Fine. We prove type soundness (with proofs mechanized in Coq) and logical consistency for F*. We have implemented a compiler that translates F* to .NET bytecode, based on a prototype for Fine. F* provides access to libraries for concurrency, networking, cryptography, and interoperability with C#, F#, and the other .NET languages. The compiler produces verifiable binaries with 60% code size overhead for proofs and types, as much as a 45x improvement over the Fine compiler, while still enabling efficient bytecode verification. We have programmed and verified nearly 50,000 lines of F* including new schemes for multi-party sessions; a zero-knowledge privacy-preserving payment protocol; a provenance-aware curated database; a suite of web-browser extensions verified for authorization properties; a cloud-hosted multi-tier web application with a verified reference monitor; the core F* typechecker itself; and programs translated to F* from other languages such as F7 and JavaScript.


title: A library for polymorphic dynamic typing

authors:
Wouter Swierstra
Thomas van Noort

abstract: Abstract This paper presents a library for programming with polymorphic dynamic types in the dependently typed programming language Agda. The resulting library allows dynamically typed values with a polymorphic type to be instantiated to a less general (possibly monomorphic) type without compromising type soundness.


title: Refactoring tools for functional languages

authors:
Simon J. Thompson
Huiqing Li

abstract: Abstract Refactoring is the process of changing the design of a program without changing what it does. Typical refactorings, such as function extraction and generalisation, are intended to make a program more amenable to extension, more comprehensible and so on. Refactorings differ from other sorts of program transformation in being applied to source code, rather than to a ‘core’ language within a compiler, and also in having an effect across a code base, rather than to a single function definition, say. Because of this, there is a need to give automated support to the process. This paper reflects on our experience of building tools to refactor functional programs written in Haskell (HaRe) and Erlang (Wrangler). We begin by discussing what refactoring means for functional programming languages, first in theory, and then in the context of a larger example. Next, we address system design and details of system implementation as well as contrasting the style of refactoring and tooling for Haskell and Erlang. Building both tools led to reflections about what particular refactorings mean, as well as requiring analyses of various kinds, and we discuss both of these. We also discuss various extensions to the core tools, including integrating the tools with test frameworks; facilities for detecting and eliminating code clones; and facilities to make the systems extensible by users. We then reflect on our work by drawing some general conclusions, some of which apply particularly to functional languages, while many others are of general value.


title: Enhancing semantic bidirectionalization via shape bidirectionalizer plug-ins

authors:
Janis Voigtländer
Zhenjiang Hu
Kazutaka Matsuda
Meng Wang

abstract: Abstract Matsuda et al . (Matsuda, K., Hu, Z., Nakano, K., Hamana, M. & Takeichi, M. (2007) Bidirectionalization transformation based on automatic derivation of view complement functions. In Proceedings of the International Conference on Functional Programming . ACM Press, pp. 47–58) and Voigtländer (Voigtländer, J. (2009) Bidirectionalization for free! In Proceedings of Principles of Programming Languages . ACM Press, pp. 165–176) have introduced two techniques that given a source-to-view function provide an update propagation function mapping an original source and an updated view back to an updated source, subject to standard consistency conditions. Previously, we developed a synthesis of the two techniques, based on a separation of shape and content aspects (Voigtländer, J., Hu, Z., Matsuda, K. & Wang, M. (2010) Combining syntactic and semantic bidirectionalization. In Proceedings of the International Conference on Functional Programming . ACM Press, pp. 181–192). Here we carry that idea further, reworking the technique of Voigtländer such that any shape bidirectionalizer (based on the work of Matsuda et al . (2007) or not) can be used as a plug-in, to good effect. We also provide a data-type-generic account, enabling wider reuse, including the use of pluggable bidirectionalization itself as a plug-in.


title: Implicit self-adjusting computation for purely functional programs

authors:
Yan Chen
Jana Dunfield
Matthew A. Hammer
Umut A. Acar

abstract: 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 techniques that enable programs to respond automatically and efficiently to dynamic changes in their inputs. Self-adjusting programs have been shown to be efficient for a reasonably broad range of problems, but the approach still requires an explicit programming style, where the programmer must use specific monadic types and primitives to identify, create, and operate on data that can change over time. We describe techniques for automatically translating purely functional programs into self-adjusting programs. In this implicit approach, the programmer need only annotate the (top-level) input types of the programs to be translated. Type inference finds all other types, and a type-directed translation rewrites the source program into an explicitly self-adjusting target program. The type system is related to information-flow type systems and enjoys decidable type inference via constraint solving. We prove that the translation outputs well- typed self-adjusting programs and preserves the source program's input–output behavior, guaranteeing that translated programs respond correctly to all changes to their data. Using a cost semantics, we also prove that the translation preserves the asymptotic complexity of the source program.


title: Transporting functions across ornaments

authors:
Pierre-Évariste Dagand
Conor McBride

abstract: 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 combination of a structuring medium together with a special purpose logic. These domain-specific logics hamper any attempt to reuse code across similarly structured data. In this paper, we capitalise on the structural invariants of datatypes. To do so, we first adapt the notion of ornament to our universe of inductive families. We then show how code reuse can be achieved by ornamenting functions. Using these functional ornaments, we capture the relationship between functions such as the addition of natural numbers and the concatenation of lists. With this knowledge, we demonstrate how the implementation of the former informs the implementation of the latter: The users can ask the definition of addition to be lifted to lists and they will only be asked the details necessary to carry on adding lists rather than numbers. Our presentation is formalised in the type theory with a universe of datatypes and all our constructions have been implemented as generic programs, requiring no extension to the type theory.


title: Delimited control and computational effects

authors:
Paul Downen
Zena M. Ariola

abstract: 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 systematic way to describe each level of control. For each language of interest, we fully characterize its semantics in terms of a reduction semantics, operational semantics, continuation-passing style transform, and abstract machine. Furthermore, the control operations are expressed in terms of fine-grained primitives that can be used to build well-known, higher-level control operators. In order to illustrate the expressive power provided by various languages, we show how other computational effects can be encoded in terms of these control operators.


title: Elaborating intersection and union types

abstract: 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 many different features. In modern type systems, parametric polymorphism is fundamental, but intersection polymorphism has gained little traction in programming languages. Most practical intersection type systems have supported only refinement intersections , which increase the expressiveness of types (more precise properties can be checked) without altering the expressiveness of terms; refinement intersections can simply be erased during compilation. In contrast, unrestricted intersections increase the expressiveness of terms, and can be used to encode diverse language features, promising an economy of both theory and implementation. We describe a foundation for compiling unrestricted intersection and union types: an elaboration type system that generates ordinary λ-calculus terms. The key feature is a Forsythe-like merge construct. With this construct, not all reductions of the source program preserve types; however, we prove that ordinary call-by-value evaluation of the elaborated program corresponds to a type-preserving evaluation of the source program. We also describe a prototype implementation and applications of unrestricted intersections and unions: records, operator overloading, and simulating dynamic typing.


title: On the complexity of stream equality

authors:
Jörg Endrullis
Dimitri Hendriks
Rena Bakhshi
Grigore Rosu

abstract: 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 the arithmetical or analytical hierarchy. Their complexity ranges from low levels of the arithmetical hierarchy such as Π 0 2 for the most relaxed stream models, to levels of the analytical hierarchy such as Π 1 1 and up to subsuming the entire analytical hierarchy for more restrictive but natural stream models. Since all these classes properly include both the semi-decidable and co-semi-decidable classes, it follows that regardless of the stream semantics employed, there is no complete proof system or algorithm for determining equality or inequality of streams. We also discuss several related problems, such as the existence and uniqueness of stream solutions for systems of equations, as well as the equality of such solutions.


title: Editorial

abstract: 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.


title: Deletion: The curse of the red-black tree

authors:
Kimball Germane
Matthew Might

abstract: 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 implementations simply omit persistent deletion. Those that include deletion typically take one of two approaches. The more-common approach is a superficial translation of the standard imperative algorithm. The resulting algorithm has functional airs but remains clumsy and verbose, characteristic of its imperative heritage. (Indeed, even the term insertion is a holdover from imperative origins, but is now established in functional contexts. Accordingly, we use the term deletion which has the same connotation.) The less-common approach leverages the features of advanced type systems, which obscures the essence of the algorithm. Nevertheless, foreign-language implementors reference such implementations and, apparently unable to tease apart the algorithm and its type specification, transliterate the entirety unnecessarily. Our goal is to provide for persistent deletion what Okasaki did for insertion: a succinct, comprehensible method that will liberate implementors. We conceptually simplify deletion by temporarily introducing a “double-black” color into Okasaki's tree type. This third color, with its natural interpretation, significantly simplifies the preservation of invariants during deletion.


title: Beginning Haskell, by Alejandro Serrano Mena, Apress, New York City, NY, 2014, ISBN-10: 1430262508, 428 pp


title: PhD Abstracts

abstract: 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!


title: 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: 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. - Volume 24 Issue 2-3


title: Pushdown flow analysis with abstract garbage collection

authors:
Dionna Amalie Glaze
Ilya Sergey
Christopher Earl
Matthew Might
David Van Horn

abstract: 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 way of combining the power of these techniques. Pushdown flow analysis grants unbounded yet computable polyvariance to the analysis of return-flow in higher-order programs. Abstract garbage collection grants unbounded polyvariance to abstract addresses which become unreachable between invocations of the abstract contexts in which they were created. Pushdown analysis solves the problem of precisely analyzing recursion in higher-order languages; abstract garbage collection is essential in solving the “stickiness” problem. Alone, our benchmarks demonstrate that each method can reduce analysis times and boost precision by orders of magnitude. We combine these methods. The challenge in marrying these techniques is not subtle: computing the reachable control states of a pushdown system relies on limiting access during transition to the top of the stack; abstract garbage collection, on the other hand, needs full access to the entire stack to compute a root set, just as concrete collection does. Conditional pushdown systems were developed for just such a conundrum, but existing methods are ill-suited for the dynamic nature of garbage collection. We show fully precise and approximate solutions to the feasible paths problem for pushdown garbage-collecting control-flow analysis. Experiments reveal synergistic interplay between garbage collection and pushdown techniques, and the fusion demonstrates “better-than-both-worlds” precision.


title: A run-time representation of scheme record types

authors:
Andrew W. Keep
R. Kent Dybvig

abstract: 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, so that the compiler can make choices at compile time about the memory layout of these data types. The procedural record types in Scheme, however, can be constructed at run time, making the efficient run-time representation of record types important to ensure good run-time performance. The run-time representation used in our implementation provides an extended model for record types allowing record types to represent foreign scalar data types, e.g., machine word integers, and allows the base record type to be extended to create non-R6RS record-type systems. This article describes our run-time representation for record types, how the garbage collector handles foreign scalar data types, and includes extended record type systems both for an object-oriented programming model and a representation of foreign structured data types.


title: Proof-producing translation of higher-order logic into pure and stateful ML

authors:
Magnus O. Myreen
Scott Owens

abstract: 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 functional programs in a programming language such as ML or Haskell. With current techniques, this step, which must be trusted, relates similar looking objects that have very different semantic definitions, such as the set-theoretic model of a logic and the operational semantics of a programming language. In this paper, we show how to increase the trustworthiness of this step with an automated technique. Given a functional program expressed in higher-order logic, our technique provides the corresponding program for a functional language defined with an operational semantics, and it provides a mechanically checked theorem relating the two. This theorem can then be used to transfer verified properties of the logical function to the program. We have implemented our technique in the HOL4 theorem prover, translating functions to a subset of Standard ML, and have applied the implementation to examples including functional data structures, a parser generator, cryptographic algorithms, a garbage collector and the 500-line kernel of the HOL light theorem prover. This paper extends our previous conference publication with new material that shows how functions defined in terms of a state-and-exception monad can be translated, with proofs, into stateful ML code. The HOL light example is also new.


title: Computational Semantics with Functional Programming, byJan van Eijck andChristina Unger

abstract: 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 paper, we describe two new approaches to Bayesian inference of sparse structures of Gaussian graphical models (GGMs). One is based on a simple modification of the cutting-edge block Gibbs sampler for sparse GGMs, which results in significant computational gains in high dimensions. The other method is based on a specific construction of the Hamiltonian Monte Carlo sampler, which results in further significant improvements. We compare our fully Bayesian approaches with the popular regularisation-based graphical LASSO, and demonstrate significant advantages of the Bayesian treatment under the same computing costs. We apply the methods to a broad range of simulated data sets, and a real-life financial data set.


title: Introduction to the art of programming using Scala, by Mark C. Lewis, Chapman and Hall/CRC Press, 2012, £ 46.99 (paperback) ISBN-10: 1439896666


title: F-ing modules

authors:
Andreas Rossberg
Claudio V. Russo
Derek Dreyer

abstract: 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 understandable, given the many non-standard methodologies that have been developed in the process of studying modules, we aim here to demonstrate that it is undeserved. To do so, we present a novel formalization of ML modules, which defines their semantics directly by a compositional “elaboration” translation into plain System F ω (the higher-order polymorphic λ-calculus). To demonstrate the scalability of our “F-ing” semantics, we use it to define a representative, higher-order ML-style module language, encompassing all the major features of existing ML module dialects (except for recursive modules). We thereby show that ML modules are merely a particular mode of use of System F ω . To streamline the exposition, we present the semantics of our module language in stages. We begin by defining a subset of the language supporting a Standard ML-like language with second-class modules and generative functors. We then extend this sublanguage with the ability to package modules as first-class values (a very simple extension, as it turns out) and OCaml-style applicative functors (somewhat harder). Unlike previous work combining both generative and applicative functors, we do not require two distinct forms of functor or signature sealing. Instead, whether a functor is applicative or not depends only on the computational purity of its body. In fact, we argue that applicative/generative is rather incidental terminology for pure versus impure functors. This approach results in a semantics that we feel is simpler and more natural than previous accounts, and moreover prohibits breaches of abstraction safety that were possible under them.


title: The Kansas University rewrite engine - A Haskell-Embedded Strategic Programming Language with Custom Closed Universes

authors:
Neil Sculthorpe
Nicolas Frisby
Andy Gill

abstract: 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 infrastructure for this task, which the author of a transformation system can use for any algebraic data structure. The Kansas University Rewrite Engine (KURE) is a typed strategic programming language, implemented as a Haskell-embedded domain-specific language. KURE is designed to support typed transformations over typed data, and the main challenge is how to make such transformations compatible with generic traversal strategies that should operate over any type. Strategic programming in a typed setting has much in common with datatype-generic programming . Compared to other approaches to datatype-generic programming, the distinguishing feature of KURE's solution is that the user can configure the behaviour of traversals based on the location of each datum in the tree, beyond their behaviour being determined by the type of each datum. This article describes KURE's approach to assigning types to generic traversals, and the implementation of that approach. We also compare KURE, its design choices, and their consequences, with other approaches to strategic and datatype-generic programming.


title: Work it, wrap it, fix it, fold it

authors:
Neil Sculthorpe
Graham Hutton

abstract: 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. In this paper we show how these two approaches can be generalised in a uniform manner by combining their correctness conditions, extend the theory with new conditions that are both necessary and sufficient to ensure the correctness of the worker/wrapper technique, and explore the benefits that result. All the proofs have been mechanically verified using the Agda system.


title: Special Issue Dedicated to ICFP 2012: Editorial

authors:
Satnam Singh
Robert Bruce Findler

abstract: The 17th ACM SIGPLAN International Conference on Functional Programming (ICFP) took place on September 10–12, 2012 in Copenhagen, Denmark. After the conference, the programme committee selected several outstanding papers and invited their authors to submit to this special issue of Journal of Functional Programming . Robby Findler and Satnam Singh acted as editors for these submissions. This issue includes the accepted papers, each of which provides substantial new material beyond the original conference version.


title: MultiMLton: A multicore-aware runtime for standard ML

authors:
K. C. Sivaramakrishnan
Lukasz Ziarek
Suresh Jagannathan

abstract: Abstract MultiMLton is an extension of the MLton compiler and runtime system that targets scalable, multicore architectures. It provides specific support for ACML, a derivative of Concurrent ML that allows for the construction of composable asynchronous events. To effectively manage asynchrony, we require the runtime to efficiently handle potentially large numbers of lightweight, short-lived threads, many of which are created specifically to deal with the implicit concurrency introduced by asynchronous events. Scalability demands also dictate that the runtime minimize global coordination. MultiMLton therefore implements a split-heap memory manager that allows mutators and collectors running on different cores to operate mostly independently. More significantly, MultiMLton exploits the premise that there is a surfeit of available concurrency in ACML programs to realize a new collector design that completely eliminates the need for read barriers, a source of significant overhead in other managed runtimes. These two symbiotic features - a thread design specifically tailored to support asynchronous communication, and a memory manager that exploits lightweight concurrency to greatly reduce barrier overheads - are MultiMLton 's key novelties. In this article, we describe the rationale, design, and implementation of these features, and provide experimental results over a range of parallel benchmarks and different multicore architectures including an 864 core Azul Vega 3, and a 48 core non-coherent Intel SCC (Single-Cloud Computer), that justify our design decisions.


title: Systematic Program Design: From Clarity to Efficiency, by Yanhong Annie Liu, Cambridge University Press, 2013, ISBN: 978-1-107-03660-4


title: Special Issue on Run-Time Systems and Target Platforms for Functional Languages: Editorial

authors:
Michael Sperber
Lennart Augustsson

abstract: Compiling functional languages to the existing variety of platforms calls for sophisticated implementations of run-time systems. This special issue focuses on this often-neglected aspect. We volunteered to compile this special issue in 2012 and immediately started soliciting papers. The original call for papers covered native-code platforms as well as run-time systems originally designed for non-functional languages such as the Java Virtual Machine or the .NET Common Language Runtime.


title: Propositions as sessions

abstract: Abstract Continuing a line of work by Abramsky (1994), Bellin and Scott (1994), and Caires and Pfenning (2010), among others, this paper presents CP, a calculus, in which propositions of classical linear logic correspond to session types. Continuing a line of work by Honda (1993), Honda et al . (1998), and Gay & Vasconcelos (2010), among others, this paper presents GV, a linear functional language with session types, and a translation from GV into CP. The translation formalises for the first time a connection between a standard presentation of session types and linear logic, and shows how a modification to the standard presentation yields a language free from races and deadlock, where race and deadlock freedom follows from the correspondence to linear logic.


title: Review: Practical Foundations for Programming Languages, by Robert Harper, Cambridge University Press, New York, December2012, English, ISBN-10: 1107029570, Hardcover, 487 pp


title: Type-based amortized resource analysis with integers and arrays

authors:
Jan Hoffmann
Zhong Shao

abstract: 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 derive bounds on loops and recursion depths of function calls. This article presents an alternative approach to resource-bound analysis for numeric and heap-manipulating programs that uses type-based amortized resource analysis. As a first step towards the analysis of imperative code, the technique is developed for a first-order ML-like language with unsigned integers and arrays. The analysis automatically derives bounds that are multivariate polynomials in the numbers and the lengths of the arrays in the input. Experiments with example programs demonstrate two main advantages of amortized analysis over current abstract interpretation–based techniques. For one thing, amortized analysis can handle programs with non-linear intermediate values like f (( n + m ) 2 ). For another thing, amortized analysis is compositional and works naturally for compound programs like f ( g ( x )).


title: Indexed containers

authors:
Thorsten Altenkirch
Neil Ghani
Peter G. Hancock
Conor McBride
Peter Morris

abstract: 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 strictly positive families in much the same way that containers provide normal forms for strictly positive types. Interestingly, this step from containers to indexed containers is achieved without having to extend the core type theory. Most of the construction presented here has been formalized using the Agda system.


title: Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm

authors:
Jesús Aransay
Jose Divasón

abstract: Abstract In this paper, we present a formalisation in a proof assistant, Isabelle/HOL, of a naive version of the Gauss-Jordan algorithm, with explicit proofs of some of its applications; and, additionally, a process to obtain versions of this algorithm in two different functional languages (SML and Haskell) by means of code generation techniques from the verified algorithm. The aim of this research is not to compete with specialised numerical implementations of Gauss-like algorithms, but to show that formal proofs in this area can be used to generate usable functional programs. The obtained programs show compelling performance in comparison to some other verified and functional versions, and accomplish some challenging tasks, such as the computation of determinants of matrices of big integers and the computation of the homology of matrices representing digital images.


title: Interleaving data and effects

authors:
Robert Atkey
Patricia Johann

abstract: Abstract The study of programming with and reasoning about inductive datatypes such as lists and trees has benefited from the simple categorical principle of initial algebras. In initial algebra semantics, each inductive datatype is represented by an initial f -algebra for an appropriate functor f . The initial algebra principle then supports the straightforward derivation of definitional principles and proof principles for these datatypes. This technique has been expanded to a whole methodology of structured functional programming, often called origami programming. In this article we show how to extend initial algebra semantics from pure inductive datatypes to inductive datatypes interleaved with computational effects. Inductive datatypes interleaved with effects arise naturally in many computational settings. For example, incrementally reading characters from a file generates a list of characters interleaved with input/output actions, and lazily constructed infinite values can be represented by pure data interleaved with the possibility of non-terminating computation. Straightforward application of initial algebra techniques to effectful datatypes leads either to unsound conclusions if we ignore the possibility of effects, or to unnecessarily complicated reasoning because the pure and effectful concerns must be considered simultaneously. We show how pure and effectful concerns can be separated using the abstraction of initial f -and- m -algebras, where the functor f describes the pure part of a datatype and the monad m describes the interleaved effects. Because initial f -and- m -algebras are the analogue for the effectful setting of initial f -algebras, they support the extension of the standard definitional and proof principles to the effectful setting. Initial f -and- m -algebras are originally due to Filinski and Støvring, who studied them in the category Cpo. They were subsequently generalised to arbitrary categories by Atkey, Ghani, Jacobs, and Johann in a FoSSaCS 2012 paper. In this article we aim to introduce the general concept of initial f -and- m -algebras to a general functional programming audience.


title: Calculating correct compilers

authors:
Patrick Bahr
Graham Hutton

abstract: Abstract In this article, we present a new approach to the problem of calculating compilers. In particular, we develop a simple but general technique that allows us to derive correct compilers from high-level semantics by systematic calculation, with all details of the implementation of the compilers falling naturally out of the calculation process. Our approach is based upon the use of standard equational reasoning techniques, and has been applied to calculate compilers for a wide range of language features and their combination, including arithmetic expressions, exceptions, state, various forms of lambda calculi, bounded and unbounded loops, non-determinism and interrupts. All the calculations in the article have been formalised using the Coq proof assistant, which serves as a convenient interactive tool for developing and verifying the calculations.


title: Efficient parallel and incremental parsing of practical context-free languages

authors:
Jean-Philippe Bernardy
Koen Claessen

abstract: Abstract We present a divide-and-conquer algorithm for parsing context-free languages efficiently. Our algorithm is an instance of Valiant's (1975; General context-free recognition in less than cubic time. J. Comput. Syst. Sci. 10 (2), 308–314), who reduced the problem of parsing to matrix multiplications. We show that, while the conquer step of Valiant's is O ( n 3 ), it improves to O (log 2 n ) under certain conditions satisfied by many useful inputs that occur in practice, and if one uses a sparse representation of matrices. The improvement happens because the multiplications involve an overwhelming majority of empty matrices. This result is relevant to modern computing: divide-and-conquer algorithms with a polylogarithmic conquer step can be parallelized relatively easily.


title: How to mingle streams

abstract: The setting is a class on functional programming. There are four students: Anne, Jack, Mary and Theo.


title: Generating constrained random data with uniform distribution

authors:
Koen Claessen
Jonas Duregård
Michal H. Palka

abstract: Abstract We present a technique for automatically deriving test data generators from a given executable predicate representing the set of values we are interested in generating. The distribution of these generators is uniform over values of a given size. To make the generation efficient, we rely on laziness of the predicate, allowing us to prune the space of values quickly. In contrast, implementing test data generators by hand is labour intensive and error prone. Moreover, handwritten generators often have an unpredictable distribution of values, risking that some values are arbitrarily underrepresented. We also present a variation of the technique that has better performance, but where the distribution is skewed in a limited, albeit predictable way. Experimental evaluation of the techniques shows that the automatically derived generators are much easier to define than handwritten ones, and their performance, while lower, is adequate for some realistic applications.


title: Review of "A functional start to computing with Python", Ted Herman, CRC Press, 2014, ISBN 978-1-4665-0455-4


title: Calculating a linear-time solution to the densest-segment problem

authors:
Sharon A. Curtis
Shin-Cheng Mu

abstract: Abstract The problem of finding a densest segment of a list is similar to the well-known maximum segment sum problem, but its solution is surprisingly challenging. We give a general specification of such problems, and formally develop a linear-time online solution, using a sliding-window style algorithm. The development highlights some elegant properties of densities, involving partitions that are decreasing and all right-skew.


title: CUFP'13 scribe's report

authors:
Marius Eriksen
Michael Sperber
Anil Madhavapeddy

abstract: The Commercial Users of Functional Programming workshop (CUFP) is an annual workshop held in association with the International Conference on Functional Programming (ICFP). The aim of the CUFP workshops is to publicize the use of functional programming in commercial ventures. Its motto is “functional programming as a means, not an end.


title: Pure type systems with explicit substitutions

authors:
Daniel Fridlender
Miguel Pagano

abstract: Abstract We introduce a new formulation of pure type systems (PTSs) with explicit substitution and de Bruijn indices and formally prove some of its meta-theory. Using techniques based on Normalisation by Evaluation, we prove that untyped conversion can be typed for predicative PTSs. Although this equivalence was settled by Siles and Herbelin for the conventional presentation of PTSs, we strongly conjecture that our proof method can also be applied to PTSs with η.


title: Thinking Functionally with Haskell by Richard Bird, Cambridge University Press, 2014

abstract: With Thinking Functionally in Haskell Richard Bird steps up to continue a family of textbook classics.Bird and Wadler jointly started the series with two editions of Introduction to Functional Programming (in Haskell) in 1988 and 1998, respectively.Let me begin with the outright spoiler that I think that this third edition breathes new life into the series and indeed presents a worthy continuation.The 12 chapters of the 340-page volume contain more material than most layouts of a one-term introductory course on functional programming can accommodate.If the many exercises are considered in depth and a discussion of Haskell-specifics is added (more on both points below), we hold the syllabus of a two-term course in our hands.According to the blurb, the book addresses first-or second-year undergraduates.I agree, but gained the impression that true programming novices would probably struggle starting with the fifth chapter when concepts, scripts, and exercises become more complex.This is also where the exposition generally picks up speed.From the outset, Bird consistently adopts a style of programming in which complex functions are composed from simpler constituents that are useful on their own (". . .functions that seem to be basic in programming are often composed of even simpler functions.A bit like protons and quarks.")Already the earliest exercises in Chapter 1 adhere to this principle: an elaborate pipeline of function types has to be designed even before students can be expected to write the functions' bodies.Early on lazy evaluation is established as a principle that makes this rigorous compositional style viable.Here, and at many occasions later in the book, Bird relates the discussion to the research literature or blog posts. 1 This provides welcome entry points for deep dives into the subject.When Chapter 4 introduces lists it carefully distinguishes finite, infinite, and partial values, a discussion that has its dedicated Chapter 9 but permeates the entire book.Chapter 5 is entirely devoted to a Sudoku solver that readers of Bird's Pearls of Functional Algorithm Design (Cambridge University Press, 2010) will recognize.The present book significantly expands on the earlier treatment through an in-depth discussion of the many involved component functions.The derivation of an efficient solver from the "clearest specification" also marks the first larger showcase of equational reasoning.Bird consequently uses the "Wim Feijen style" e 1 = {justification} e 2 to simplify and optimize programs or to establish proofs of their properties.The rewriting of compositions of functions remains one of Bird's grand themes.Calculations pervade the entire book, from its preface(!) to the final Chapter 12 where a (semi-)automatic equational rewriter is developed.Lawful program construction encourages "wholemeal programming", 1 Regarding a discussion of strict vs. lazy evaluation, Bird points to a blog post by Robert Harper and the extensive thread of comments that followed (http://existentialtype.wordpress.


title: Counting and generating terms in the binary lambda calculus

authors:
Katarzyna Grygiel
Pierre Lescanne

abstract: Abstract In a paper, entitled Binary lambda calculus and combinatory logic , John Tromp presents a simple way of encoding lambda calculus terms as binary sequences. In what follows, we study the numbers of binary strings of a given size that represent lambda terms and derive results from their generating functions, especially that the number of terms of size n grows roughly like 1.963447954. . . n . In a second part we use this approach to generate random lambda terms using Boltzmann samplers.


title: Review of "Learn you some Erlang for great good! A beginner's guide", by Fred Hébert, No Starch Press, 2013, £26.80 (paperback), ISBN: 978-1-59327-435-1


title: PhD abstracts

abstract: 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.


title: PhD Abstracts


title: PhD Abstracts

abstract: 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!


title: A representation theorem for second-order functionals

authors:
Mauro Jaskelioff
Russell O'Connor

abstract: Abstract Representation theorems relate seemingly complex objects to concrete, more tractable ones. In this paper, we take advantage of the abstraction power of category theory and provide a datatype-generic representation theorem. More precisely, we prove a representation theorem for a wide class of second-order functionals which are polymorphic over a class of functors. Types polymorphic over a class of functors are easily representable in languages such as Haskell, but are difficult to analyse and reason about. The concrete representation provided by the theorem is easier to analyse, but it might not be as convenient to implement. Therefore, depending on the task at hand, the change of representation may prove valuable in one direction or the other. We showcase the usefulness of the representation theorem with a range of examples. Concretely, we show how the representation theorem can be used to prove that traversable functors are finitary containers, how coalgebras of a parameterised store comonad relate to very well-behaved lenses, and how algebraic effects might be implemented in a functional language.


title: Evaluation of splittable pseudo-random generators

abstract: Abstract Pseudo-random number generation is a fundamental problem in computer programming. In the case of sequential processing the problem is very well researched, but parallel processing raises new problems whereof far too little is currently understood. Splittable pseudo-random generators (S-PRNG) have been proposed to meet the challenges of parallelism. While applicable to any programming paradigm, they are designed to be particularly suitable for pure functional programming. In this paper, we review and evaluate known constructions of such generators, and we identify flaws in several large classes of generators, including Lehmer trees, the implementation in Haskell's standard library, leapfrog, and subsequencing (substreaming).


title: Teaching types with a cognitively effective worked example format

authors:
Ville Tirronen
Ville Isomöttönen

abstract: Abstract Teaching functional programming as a second programming paradigm is often difficult as students can have strong preconceptions about programming. When most of these preconceived ideas fail to be confirmed, functional programming may be seen as an unnecessarily difficult topic. A typical topic that causes such difficulties is the language of types employed by many modern functional languages. In this paper, we focus on addressing this difficulty through the use of step-by-step calculations of type expressions. The outcome of the study is an elaboration of a worked example format and a methodical approach for teaching types to beginner functional programmers.


title: Understanding beginners' mistakes with Haskell

authors:
Ville Tirronen
Samuel Uusi-Mäkelä
Ville Isomöttönen

abstract: Abstract This article presents an overview of student difficulties in an introductory functional programming (FP) course taught in Haskell. The motivation for this study stems from our belief that many student difficulties can be alleviated by understanding the underlying causes of errors and by modifying the educational approach and, possibly, the teaching language accordingly. We analyze students' exercise submissions and categorize student errors according to compiler error messages and then manually according to the observed underlying cause. Our study complements earlier studies on the topic by applying computer and manual analysis while focusing on providing descriptive statistics of difficulties specific to FP languages. We conclude that the majority of student errors, regardless of cause, are reported by three different compiler error messages that are not well understood by students. In addition, syntactic features, such as precedence, the syntax of function application, and deeply nested statements, cause difficulties throughout the course.


title: Verified decision procedures for MSO on words based on derivatives of regular expressions

authors:
Dmitriy Traytel
Tobias Nipkow

abstract: 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 (e.g., automata). This paper presents a verified functional decision procedure for MSO formulas that is not based on automata but on regular expressions. Functional languages are ideally suited for this task: regular expressions are data types and functions on them are defined by pattern matching and recursion and are verified by structural induction. Decision procedures for regular expression equivalence have been formalized before, usually based on Brzozowski derivatives. Yet, for a straightforward embedding of MSO formulas into regular expressions, an extension of regular expressions with a projection operation is required. We prove total correctness and completeness of an equivalence checker for regular expressions extended in that way. We also define a language-preserving translation of formulas into regular expressions with respect to two different semantics of MSO. Our results have been formalized and verified in the theorem prover Isabelle. Using Isabelle's code generation facility, this yields purely functional, formally verified programs that decide equivalence of MSO formulas.


title: Mtac: A monad for typed tactic programming in Coq

authors:
Beta Ziliani
Derek Dreyer
Neelakantan R. Krishnaswami
Aleksandar Nanevski
Viktor Vafeiadis

abstract: 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 prover, or (b) rely on advanced type-theoretic machinery that is not easily integrated into established theorem provers. We present Mtac, a lightweight but powerful extension to Coq that supports dependently typed tactic programming. Mtac tactics have access to all the features of ordinary Coq programming, as well as a new set of typed tactical primitives. We avoid the need to touch the trusted kernel typechecker of Coq by encapsulating uses of these new tactical primitives in a monad , and instrumenting Coq so that it executes monadic tactics during type inference.