Abstract Structural induction is pervasively used by functional programmers and researchers for both informal reasoning as well as formal methods for program verification and semantics. In this paper, we promote its dual—structural coinduction—as a technique for understanding corecursive programs only in terms of the logical structure of their context. We illustrate this technique as an informal method of proofs which closely match the style of informal inductive proofs, where it is straightforward to check that all cases are covered and the coinductive hypotheses are used correctly. This intuitive idea is then formalized through a syntactic theory for deriving program equalities, which is justified purely in terms of the computational behavior of abstract machines and proved sound with respect to observational equivalence.

Call-By-Push-Value has famously subsumed both call-by-name and call-by-value by decomposing programs along the axis of “values” versus “computations.” Here, we introduce Call-By-Unboxed-Value which further decomposes programs along an orthogonal axis separating “atomic” versus “complex.” As the name suggests, these two dimensions make it possible to express the representations of values as boxed or unboxed, so that functions pass unboxed values as inputs and outputs. More importantly, Call-By-Unboxed-Value allows for an unrestricted mixture of polymorphism and unboxed types, giving a foundation for studying compilation techniques for polymorphism based on representation irrelevance . In this regard, we use Call-By-UnboxedValue to formalize representation polymorphism independently of types; for the first time compiling untyped representation-polymorphic code, while nonetheless preserving types all the way to the machine.

Closure conversion, an essential step in compiling functional programs, is traditionally presented as a global transformation from a language with higher-order functions to one without. Optimizing this transformation can be done at any of its three stages with various tradeoffs. After conversion, optimizations will be in the target language at the cost of a weaker equational theory. During conversion, optimizations may be embedded into the transformation itself at the cost of increasing its complexity and correctness. And before conversion, optimizations may be planned and anticipated in a specialized intermediate language (IL) where all the properties of the source program are still known, with the hope that they will survive the rest of the compilation process.

Abstract Recursion is a mature, well-understood topic in the theory and practice of programming. Yet its dual, corecursion is underappreciated and still seen as exotic. We aim to put them both on equal footing by giving a foundation for primitive corecursion based on computation, giving a terminating calculus analogous to the original computational foundation of recursion. We show how the implementation details in an abstract machine strengthens their connection, syntactically deriving corecursion from recursion via logical duality. We also observe the impact of evaluation strategy on the computational complexity of primitive (co)recursive combinators: call-by-name allows for more efficient recursion, but call-by-value allows for more efficient corecursion.

Functional programming language design has been shaped by the framework of natural deduction, in which language constructs are divided into introduction and elimination rules for producers of values. In sequent calculus-based languages, left introduction rules replace (right) elimination rules and provide a dedicated sublanguage for consumers of values. In this paper, we present and analyze a wider design space of programming languages which encompasses four kinds of rules: Introduction and elimination, both left and right. We analyze the influence of rule choice on program structure and argue that having all kinds of rules enriches a programmer’s modularity arsenal. In particular, we identify four ways of adhering to the principle that ”the structure of the program follows the structure of the data“ and show that they correspond to the four possible choices of rules. We also propose the principle of bi-expressibility to guide and validate the design of rules for a connective. Finally, we deepen the well-known dualities between different connectives by means of the proof/refutation duality.

The duality between "true" and "false" is a hallmark feature of logic. We show how this duality can be put to use in the theory and practice of programming languages and their implementations, too. Starting from a foundation of constructive logic as dialogues, we illustrate how it describes a symmetric language for computation, and survey several applications of the dualities found therein.

Recursion and induction are mature, well-understood topics in programming. Yet their duals, corecursion and coinduction, are still exotic and underdeveloped programming features. We aim to put them on equal footing by giving a foundation for corecursion based on computation, analogous to the original computational foundation of recursion. At the lower level, we show how the connection between the two can be strengthened through their implementation details in an abstract machine. At the higher level, we develop a syntactic equational theory for inductive and coinductive reasoning based on control flow. We also observe the impact of evaluation strategy: call-by-name has efficient recursion and strong coinductive reasoning, but call-by-value has efficient corecursion and strong inductive reasoning.

A language supporting polymorphism is a boon to programmers: they can express complex ideas once and reuse functions in a variety of situations. However, polymorphism is pain for compilers tasked with producing efficient code that manipulates concrete values. This paper presents a new intermediate language that allows for efficient static compilation, while still supporting flexible polymorphism. Specifically, it permits polymorphism over not only the types of values, but also the representation of values, the arity of primitive machine functions, and the evaluation order of arguments---all three of which are useful in practice. The key insight is to encode information about a value's calling convention in the kind of its type, rather than in the type itself.

Computer scientists are well-versed in dealing with data structures. The same cannot be said about their dual: codata. Even though codata is pervasive in category theory, universal algebra, and logic, the use of codata for programming has been mainly relegated to representing infinite objects and processes. Our goal is to demonstrate the benefits of codata as a general-purpose programming abstraction independent of any specific language: eager or lazy, statically or dynamically typed, and functional or object-oriented. While codata is not featured in many programming languages today, we show how codata can be easily adopted and implemented by offering simple inter-compilation techniques between data and codata. We believe codata is a common ground between the functional and object-oriented paradigms; ultimately, we hope to utilize the Curry-Howard isomorphism to further bridge the gap.

For a long time, intersection types have been admired for their surprising ability to complete the simply typed lambda calculus. Intersection types are an example of an implicit typing feature which can describe program behavior without manifesting itself within the syntax of a program. Dual to int ersections, union types are another implicit typing feature which extends the completeness property of intersection types in the lambda calculus to full-fledged programming languages. However, the formalization of union types can easily break other desirable meta-theoretical properties of the type system. But why should unions be troublesome when their dual, intersections, are not? We look at the issues surrounding the design of type systems for both intersection and union types through the lens of duality by formalizing them within the symmetric language of the classical sequent calculus. In order to formulate type systems which have all of our properties of interest—soundness, completeness, and type safety—we also look at the impact of evaluation strategy on typing. As a result, we present two dual type systems—one for call-by-value and one for call-by-name evaluation—which have all three properties. We also consider the possibility of classical non-deterministic evaluation, for which there is a choice between two different systems depending on which properties are desired: a full type system which is complete, and a simplified type system which is sound and type safe.

The study of polarity in computation has revealed that an "ideal" programming language combines both call-by-value and call-by-name evaluation; the two calling conventions are each ideal for half the types in a programming language. But this binary choice leaves out call-by-need which is used in practice to implement lazy-by-default languages like Haskell. We show how the notion of polarity can be extended beyond the value/name dichotomy to include call-by-need by only adding a mechanism for sharing and the extra polarity shifts to connect them, which is enough to compile a Haskell-like functional language with user-defined types.

Abstract We present a model of computation that heavily emphasizes the concept of duality and the interaction between opposites–production interacts with consumption. The symmetry of this framework naturally explains more complicated features of programming languages through relatively familiar concepts. For example, binding a value to a variable is dual to manipulating the flow of control in a program. By looking at the computational interpretation of the sequent calculus, we find a language that lets us speak about duality, control flow, and evaluation order in programs as first-class concepts. We begin by reviewing Gentzen's LK sequent calculus and show how the Curry–Howard isomorphism still applies to give us a different basis for expressing computation. We then illustrate how the fundamental dilemma of computation in the sequent calculus gives rise to a duality between evaluation strategies : strict languages are dual to lazy languages. Finally, we discuss how the concept of focusing , developed in the setting of proof search, is related to the idea of type safety for computation expressed in the sequent calculus. In this regard, we compare and contrast two different methods of focusing that have appeared in the literature, static and dynamic focusing, and illustrate how they are two means to the same end.

Many fields of study in compilers give rise to the concept of a join point—a place where different execution paths come together. Join points are often treated as functions or continuations, but we believe it is time to study them in their own right. We show that adding join points to a direct-style functional intermediate language is a simple but powerful change that allows new optimizations to be performed, including a significant improvement to list fusion. Finally, we report on recent work on adding join points to the intermediate language of the Glasgow Haskell Compiler.

Abstract Designing rewriting systems that respect functional extensionality for call-by-name languages with effects turns out to be surprisingly challenging. Simply interpreting extensional laws like η as reduction rules easily breaks confluence. We explore these issues in the setting of a sequent calculus. Building on an insight that appears in different aspects of the theory of call-by-name functional languages—confluent rewriting for two independent control calculi and sound continuation-passing style transformations—we give a confluent reduction system for lazy extensional functions. Finally, we consider limitations to this approach when used for strict evaluation and types beyond functions.

The λ-calculus is popular as an intermediate language for practical compilers. But in the world of logic it has a lesser-known twin, born at the same time, called the sequent calculus. Perhaps that would make for a good intermediate language, too? To explore this question we designed Sequent Core, a practically-oriented core calculus based on the sequent calculus, and used it to re-implement a substantial chunk of the Glasgow Haskell Compiler.

Our goal is to develop co-induction from our understanding of induction, putting them on level ground as equal partners for reasoning about programs. We investigate several structures which represent well-founded forms of recursion in programs. These simple structures encapsulate reasoning by primitive and noetherian induction principles, and can be composed together to form complex recursion schemes for programs operating over a wide class of data and co-data types. At its heart, this study is guided by duality: each structure for recursion has a dual form, giving perfectly symmetric pairs of equal and opposite data and co-data types for representing recursion in programs. Duality is brought out through a framework presented in sequent style, which inherently includes control effects that are interpreted logically as classical reasoning principles. To accommodate the presence of effects, we give a calculus parameterized by a notion of strategy, which is strongly normalizing for a wide range of strategies. We also present a more traditional calculus for representing effect-free functional programs, but at the cost of losing some of the founding dualities.

Parigot's λμ-calculus, a system for computational reasoning about classical proofs, serves as a foundation for control operations embodied by operators like Scheme's callcc. We demonstrate that the call-by-value theory of the λμ-calculus contains a latent theory of delimited control, and that a known variant of λμ which unshackles the syntax yields a calculus of composable continuations from the existing constructs and rules for classical control. To relate to the various formulations of control effects, and to continuation-passing style, we use a form of compositional program transformations which preserves the underlying structure of equational theories, contexts, and substitution. Finally, we generalize the call-by-name and call-by-value theories of the λμ-calculus by giving a single parametric theory that encompasses both, allowing us to generate a call-by-need instance that defines a calculus of classical and delimited control with lazy evaluation and sharing.

Continuation-passing style (CPS) transforms have long been important tools in the study of programming. They have been shown to correspond to abstract machines and, when combined with a naming transform that expresses shared values, they enjoy a direct correspondence with encodings into process calculi such as the π-calculus. We present our notion of correctness and discuss the sufficient conditions that guarantee the correctness of transforms. We then consider the call-by-value, call-by-name and call-by-need evaluation strategies for the λ-calculus and present their CPS transforms, abstract machines, π-encodings, and proofs of correctness. Our analysis covers a uniform CPS transform, which differentiates the three evaluation strategies only by the treatment of function calls. This leads to a new CPS transform for call-by-need requiring a less expressive form of side effect, which we call constructive update.

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.