This project develops new foundations for machine-verified proof in programming languages and mathematics. Formalized libraries of mathematics enable increased confidence in the correctness of proven results, large-scale collaboration on future results, and a database of relevant facts for automated reasoning. However, reuse of formalized proofs and proof components is made difficult by language limitations within theorem provers and incompatible choices between theorem provers. The project’s novelty is a new foundational technique based on type theory, with formal tools for proof modularity and reuse at its core. The project’s impacts are increased sharing among formalization efforts and a basis for more effectively exploring new proof theoretic foundations for mechanized theorem proving.

The project’s core contribution is a new impredicative dependent row type theory. Impredicativity captures expressive features of modern dependently typed languages, like induction-recursion, without further extension. Proof reuse is enabled by row types, used to describe extensible variants and extensible dependent records. Both object logics and constructs within them will be expressed extensible, automatically extending proof terms over simpler objects in smaller logics to apply to more complex terms in larger logics. For example, constructive proofs on groups can automatically be used as classical proofs on fields.

Mathematics and computer science are inextricably linked. However, it is well-known among educators and education researchers that undergraduate computer scientists often do not appreciate the relevance of mathematics to their discipline. This disconnect adversely affects students, especially as they progress from concrete, practical introductory courses centered on programming to theoretical upper-level courses rooted in abstract mathematics. Researchers have observed that student performance in the classroom and retention within the major falter when these connections are not established. This project’s impact is to address these concerns by developing pedagogy that (a) unites the mathematical foundations and practice of computer science together in a way that all undergraduates can appreciate and directly apply in their future endeavors and (b) is adoptable by as many institutions as possible, especially those with limited room to expand their curriculum.

To accomplish these goals, the investigators develop, deploy, and evaluate new pedagogy that integrates formal methods techniques within the existing undergraduate computer science curriculum. Specifically, this pedagogy introduces program reasoning, an activity all computer scientists perform, as the primary vehicle for studying the mathematical foundations of computing in the contexts of introductory programming, discrete mathematics, and algorithms courses. Such pedagogy bridges the gap between mathematics and computer science for all undergraduate computer scientists and makes relevant formal methods for a new generation of programmers. Additionally, the project promotes the relevance of formal methods to undergraduate computer science educators, as exemplified by this pedagogy, through a series of workshops at the regional and national levels.

The project sits at the intersection of two important goals in practical and correct software development. The first is precisely and formally capturing the requirements of programs and program components: we do not want a program to rely on comparing functions for equality, or adding arbitrary integers to pointers. The second is modular and extensible program construction: program components must be developed independently, and changes internal to one component should not cause cascading changes to other components. This project’s novelties are: a new foundation for extensible descriptions of program properties and invariants, subsuming multiple competing and complementary features used in current languages; its impementation; and its metatheory. The project’s impacts are: regularizing and extending features for specifying program properties in existing languages; simplifying their implementation; and making these features practical for adoption in other languages.

The primary focus of this project is the programming language Haskell. Haskell has an advanced type system with several features for modular and extensible specification of program properties, most prominently type classes and type families. These features have evolved mostly independently, with different approaches to their specification and implementation. The result, for both programmers and implementers, is a constellation of features with frequently surprising interactions and limitations. This project develops a new core language for Haskell, with a single feature that captures both type classes and type families. It will simplify Haskell implementations and make the existing features of Haskell more regular and more expressive. It will enable new features of Haskell, closing the gaps between type families and type classes. And, it will make it easier for other languages to adopt features from Haskell, by giving them a simpler underlying semantics.

Modern software engineering relies on large ecosystems of independent software components and libraries. This poses two challenges for the design of programming languages and language tooling, both of which are addressed by this project. First, languages must support developing independent components, including identifying and abstracting reusable components from existing applications. Second, languages must provide expressive specification mechanisms to ensure that components are used correctly and that components do not have unintended interactions. The project’s novelties are new programming language features for modular specification and implementation of program data and behavior, at all level of the software stack from user-facing applications to operating system components and hardware support. The project’s impacts are improvements in both software reliability and programmer productivity, as the project enables language tooling to automatically help programmers identify and correctly use software components and libraries.

The project has two primary themes. The first is modularity and reuse in high-level functional programs. The project develops extensible types for data and computational effects, supporting high-level abstractions including overloading, generic programming, and extensible effect handlers. The second is modularity and reuse in low-level and systems programs. The project develops extensible bit-level specifications of data structures and their layout, targeting applications including operating system kernels and hardware interfaces. Each of these themes will only have impact if the resulting language features have comparable performance with existing approaches. The project uses linear typing and compile-type specialization to offset runtime costs traditionally associated with generic and extensible programming techniques.

We propose a novel approach to soundly combining linear types with multi-shot effect handlers. Linear type systems statically ensure that resources such as file handles and communication channels are used exactly once. Effect handlers provide a rich modular programming abstraction for implementing features ranging from exceptions to concurrency to backtracking. Whereas conventional linear type systems bake in the assumption that continuations are invoked exactly once, effect handlers allow continuations to be discarded (e.g. for exceptions) or invoked more than once (e.g. for backtracking). This mismatch leads to soundness bugs in existing systems such as the programming language Links, which combines linearity (for session types) with effect handlers. We introduce control-flow linearity as a means to ensure that continuations are used in accordance with the linearity of any resources they capture, ruling out such soundness bugs.

We formalise the notion of control-flow linearity in a System F-style core calculus F_eff^∘ equipped with linear types, an effect type system, and effect handlers. We define a linearity-aware semantics in order to formally prove that F_eff^∘ preserves the integrity of linear values in the sense that no linear value is discarded or duplicated. In order to show that control-flow linearity can be made practical, we adapt Links based on the design of F_eff^∘, in doing so fixing a long-standing soundness bug.

Finally, to better expose the potential of control-flow linearity, we define an ML-style core calculus Q_eff^∘, based on qualified types, which requires no programmer provided annotations, and instead relies entirely on type inference to infer control-flow linearity. Both linearity and effects are captured by qualified types. Q_eff^∘ overcomes a number of practical limitations of F_eff^∘, supporting abstraction over linearity, linearity dependencies between type variables, and a much more fine-grained notion of control-flow linearity.

We present a novel approach to generic programming over extensible data types. Row types capture the structure of records and variants, and can be used to express record and variant subtyping, record extension, and modular composition of case branches. We extend row typing to capture generic programming over rows themselves, capturing patterns including lifting operations to records and variations from their component types, and the duality between cases blocks over variants and records of labeled functions, without placing specific requirements on the fields or constructors present in the records and variants. We formalize our approach in System R𝜔, an extension of F𝜔 with row types, and give a denotational semantics for (stratified) R𝜔 in Agda.

This paper proposes a new approach to writing and verifying divide-and-conquer programs in Coq. Extending the rich line of previous work on algebraic approaches to recursion schemes, we present an algebraic approach to divide-and-conquer recursion: recursions are represented as a form of algebra, and from outer recursions, one may initiate inner recursions that can construct data upon which the outer recursions may legally recurse. Termination is enforced entirely by the typing discipline of our recursion schemes. Despite this, our approach requires little from the underlying type system, and can be implemented in System Fω plus a limited form of positive-recursive types. Our implementation of the method in Coq does not rely on structural recursion or on dependent types. The method is demonstrated on several examples, including mergesort, quicksort, Harper’s regular-expression matcher, and others. An indexed version is also derived, implementing a form of divide-and-conquer induction that can be used to reason about functions defined via our method.

Type constructors in functional programming languages are total: a Haskell programmer can equally readily construct lists of any element type. In practice, however, not all applications of type constructors are equally sensible: collections may only make sense for orderable elements, or embedded DSLs might only make sense for serializable return types. Jones et al. proposed a theory of partial type constructors, which guarantees that type applications are sensible, and extends higher-order abstractions to apply equally well to partial and total type constructors. This paper evaluates the practicality of partial type constructors, in terms of both language design and implementation. We extend GHC, the most widely used Haskell compiler, with support for partial type constructors, and test our extension on the compiler itself and its libraries. We show that introducing partial type constructors has a minimal impact on most code, but raises important questions in language and library design

This paper introduces Hypersequent GV (HGV), a modular and extensible core calculus for functional programming with session types that enjoys deadlock freedom, confluence, and strong normalisation. HGV exploits hyper-environments, which are collections of type environments, to ensure that structural congruence is type preserving. As a consequence we obtain a tight operational correspondence between HGV and HCP, a hypersequent-based process-calculus interpretation of classical linear logic. Our translations from HGV to HCP and vice-versa both preserve and reflect reduction. HGV scales smoothly to support Girard’s Mix rule, a crucial ingredient for channel forwarding and exceptions.

Functional programming languages assume that type constructors are total. Yet functional programmers know better: counterexamples range from container types that make limiting assumptions about their contents (e.g., requiring computable equality or ordering functions) to type families with defining equations only over certain choices of arguments. We present a language design and formal theory of partial type constructors, capturing the domains of type constructors using qualified types. Our design is both simple and expressive: we support partial datatypes as first-class citizens (including as instances of parametric abstractions, such as the Haskell Functor and Monad classes), and show a simple type elaboration algorithm that avoids placing undue annotation burden on programmers. We show that our type system rejects ill-defined types and can be compiled to a semantic model based on System F. Finally, we have conducted an experimental analysis of a body of Haskell code, using a proof-of-concept implementation of our system; while there are cases where our system requires additional annotations, these cases are rarely encountered in practical Haskell code.

Process calculi based in logic, such as πDILL and CP, provide a foundation for deadlock-free concurrent programming, but exclude non- determinism and races. HCP is a reformulation of CP which addresses a fundamental shortcoming: the fundamental operator for parallel com- position from the π-calculus does not correspond to any rule of linear logic, and therefore not to any term construct in CP. We introduce HCP^–_ND , which extends HCP with a novel account of non- determinism. Our approach draws on bounded linear logic to provide a strongly-typed account of standard process calculus expressions of non-determinism. We show that our extension is expressive enough to capture many uses of non-determinism in untyped calculi, such as non- deterministic choice, while preserving HCP’s meta-theoretic properties, including deadlock freedom.

We present a novel typed language for extensible data types, generalizing and abstracting existing systems of row types and row polymorphism. Extensible data types are a powerful addition to traditional functional programming languages, capturing ideas from OOP-like record extension and polymorphism to modular compositional interpreters. We introduce row theories, a monoidal generalization of row types, giving a general account of record concatenation and projection (dually, variant injection and branching). We realize them via qualified types, abstracting the interpretation of records and variants over different row theories. Our approach naturally types terms untypable in other systems of extensible data types, while maintaining strong metatheoretic properties, such as coherence and principal types. Evidence for type qualifiers has computational content, determining the implementation of record and variant operations; we demonstrate this in giving a modular translation from our calculus, instantiated with various row theories, to polymorphic λ-calculus.

Session types statically guarantee that communication complies with a protocol. However, most accounts of session typing do not account for failure, which means they are of limited use in real applications—especially distributed applications—where failure is pervasive.

We present the first formal integration of asynchronous session types with exception handling in a functional programming language. We define a core calculus which satisfies preservation and progress properties, is deadlock free, confluent, and terminating.

We provide the first implementation of session types with exception handling for a fully-fledged functional programming language, by extending the Links web programming language; our implementation draws on existing work on effect handlers. We illustrate our approach through a running example of two-factor authentication, and a larger example of a session-based chat application where communication occurs over session-typed channels and disconnections are handled gracefully.

Gradual typing has emerged as the tonic for programmers wanting a mixture of static and dynamic typing, hoping to achieve the best of both. Sound gradual typing is the most potent brew, providing static type- checking and dynamic assertions. Contracts provide a lightweight form of gradual typing as they do not provide static checking but can be implemented as a library, rather than demanding language level support.

Intersection and union types are well suited to dynamic languages: intersection encodes overloaded functions; union encodes uncertain data arising from branching code. We extend the untyped lambda calculus with contracts for monitoring higher-order intersection and union types, giving a uniform treatment to both. Each operator requires a single reduction rule that does not depend on the constituent types, or the context of the operator, unlike existing work.

We present a new method for defining contract satisfaction based on blame behaviour. A value positively satisfies a type if, when monitored against that type in any context, never elicits positive blame. A continuation negatively satisfies a type if, when monitored against that type using any value, never elicits negative blame.

We supplement our definition of satisfaction with a serious of monitoring properties that satisfying values and continuations should have. Each type has a positive property for values and a negative property for continuations, ensuring that contracts reflect the types they represent.

We present an approach to support partiality in type-level computation without compromising expressiveness or type safety. Existing frameworks for type-level computation either require totality or implicitly assume it. For example, type families in Haskell provide a powerful, modular means of defining type-level computation. However, their current design implicitly assumes that type families are total, introducing nonsensical types and significantly complicating the metatheory of type families and their extensions. We propose an alternative design, using qualified types to pair type-level computations with predicates that capture their domains. Our approach naturally captures the intuitive partiality of type families, simplifying their metatheory. As evidence, we present the first complete proof of consistency for a language with closed type families.

TypeScript participates in the recent trend among programming languages to support gradual typing. The DefinitelyTyped Repository for TypeScript supplies type definitions for over 2000 popular JavaScript libraries. However, there is no guarantee that implementations conform to their corresponding declarations.

We present a practical evaluation of gradual typing for TypeScript. We have developed a tool, based on the polymorphic blame calculus, for monitoring JavaScript libraries and TypeScript clients against the TypeScript definition. We apply our tool, TypeScript TNG, to those libraries in the DefinitelyTyped Repository which had adequate test code to use. Of the 122 libraries we checked, 59 had cases where either the library or its tests failed to conform to the declaration.

Gradual typing should satisfy non-interference. Monitoring a program should never change its behaviour except, to raise a type error should a value not conform to its declared type. However, our experience also suggests serious technical concerns with the use of the JavaScript proxy mechanism for enforcing contracts. Of the 122 libraries we checked, 22 had cases where the library or its tests violated non-interference.

We present a linear functional calculus with both the safety guarantees expressible with linear types and the rich language of combinators and composition provided by functional programming. Unlike previous combinations of linear typing and functional programming, we compromise neither the linear side (for example, our linear values are first-class citizens of the language) nor the functional side (for example, we do not require duplicate definitions of compositions for linear and unrestricted functions). To do so, we must generalize abstraction and application to encompass both linear and unrestricted functions. We capture the typing of the generalized constructs with a novel use of qualified types. Our system maintains the metatheoretic properties of the theory of qualified types, including principal types and decidable type inference. Finally, we give a formal basis for our claims of expressiveness, by showing that evaluation respects linearity, and that our language is a conservative extension of existing functional calculi.

Session types provide static guarantees that concurrent programs respect communication protocols. We give a novel account of recursive session types in the context of GV, a small concurrent extension of the linear λ-calculus. We extend GV with recursive types and catamorphisms, following the initial algebra semantics of recursion, and show that doing so naturally gives rise to recursive session types. We show that this principled approach to recursion resolves long-standing problems in the treatment of duality for recursive session types.

We characterize the expressiveness of GV concurrency by giving a CPS translation to (non-concurrent) λ-calculus and proving that reduction in GV is simulated by full reduction in λ-calculus. This shows that GV remains terminating in the presence of positive recursive types, and that such arguments extend to other extensions of GV, such as polymorphism or non-linear types, by appeal to normalization results for sequential λ-calculi. We also show that GV remains deadlock free and deterministic in the presence of recursive types.

Finally, we extend CP, a session-typed process calculus based on linear logic, with recursive types, and show that doing so preserves the connection between reduction in GV and cut elimination in CP.

We present a novel embedding of session-typed concurrency in Haskell.

We extend an existing HOAS embedding of the linear λ-calculus with a set of core session-typed primitives, using indexed type families to express the constraints of the session typing discipline.

We give two interpretations of our embedding, one in terms of GHC’s built-in concurrency and another in terms of purely functional continuations.

Our safety guarantees, including deadlock freedom, are assured statically and introduce no additional runtime overhead.

Session types provide a static guarantee that concurrent programs respect communication protocols. Recent work has explored a correspondence between proof rules and cut reduction in linear logic and typing and evaluation of process calculi. This paper considers two approaches to extend logically-founded process calculi. First, we consider extensions of the process calculus to more closely resemble π-calculus. Second, inspired by denotational models of process calculi, we consider conflating dual types. Most interestingly, we observe that these approaches coincide: conflating the multiplicatives (⊗ and ⅋) allows processes to share multiple channels; conflating the additives (⊕ and &) provides nondeterminism; and conflating the exponentials (! and ?) yields access points, a rendezvous mechanism for initiating session typed communication. Access points are particularly expressive: for example, they are sufficient to encode concurrent state and general recursion.

Extensible variants improve the modularity and expressiveness of programming languages: they allow program functionality to be decomposed into independent blocks, and allow seamless extension of existing code with both new cases of existing data types and new operations over those data types.

This paper considers three approaches to providing extensible variants in Haskell. Row typing is a long understood mechanism for typing extensible records and variants, but its adoption would require extension of Haskell’s core type system. Alternatively, we might hope to encode extensible variants in terms of existing mechanisms, such as type classes. We describe an encoding of extensible variants using instance chains, a proposed extension of the class system. Unlike many previous encodings of extensible variants, ours does not require the definition of a new type class for each function that consumes variants. Finally, we translate our encoding to use closed type families, an existing feature of GHC. Doing so demonstrates the interpretation of instances chains and functional dependencies in closed type families.

One concern with encodings like ours is how completely they match the encoded system. We compare the expressiveness of our encodings with each other and with systems based on row types. We find that, while equivalent terms are typable in each system, both encodings require explicit type annotations to resolve ambiguities in typing not present in row type systems, and the type family implementation retains more constraints in principal types than does the instance chain implementation. We propose a general mechanism to guide the instantiation of ambiguous type variables, show that it eliminates the need for type annotations in our encodings, and discuss conditions under which it preserves coherence.

Session types provide a static guarantee that concurrent programs respect communication protocols. Recently, Caires, Pfenning, and Toninho, and Wadler, have developed a correspondence between propositions of linear logic and session typed π-calculus processes.

We relate the cut-elimination semantics of this approach to an operational semantics for session-typed concurrency in a functional language.

We begin by presenting a variant of Wadler’s session-typed core functional language, GV. We give a small-step operational semantics for GV. We develop a suitable notion of deadlock, based on existing approaches for capturing deadlock in π-calculus, and show that all well-typed GV programs are deadlock-free, deterministic, and terminating.

We relate GV to linear logic by giving translations between GV and CP, a process calculus with a type system and semantics based on classical linear logic. We prove that both directions of our translation preserve reduction; previous translations from GV to CP, in contrast, failed to preserve β-reduction.

Furthermore, to demonstrate the modularity of our approach, we define two extensions of GV which preserve deadlock-freedom, determinism, and termination.

As originally proposed, type classes provide overloading and ad-hoc definition, but can still be understood (and implemented) in terms of strictly parametric calculi. This is not true of subsequent extensions of type classes. Functional dependencies and equality constraints allow the satisfiability of predicates to refine typing; this means that the interpretations of equivalent qualified types may not be interconvertible. Overlapping instances and instance chains allow predicates to be satisfied without determining the implementations of their associated class methods, introducing truly non-parametric behavior. We propose a new approach to the semantics of type classes, interpreting polymorphic expressions by the behavior of each of their ground instances, but without requiring that those behaviors be parametrically determined. We argue that this approach both matches the intuitive meanings of qualified types and accurately models the behavior of programs.

Recently, Wadler presented a continuation-passing translation from a session-typed functional language, GV, to a process calculus based on classical linear logic, CP. However, this translation is one-way: CP is more expressive than GV. We propose an extension of GV, called HGV, and give translations showing that it is as expressive as CP. The new translations shed light both on the original translation from GV to CP, and on the limitations in expressiveness of GV.

Type classes have found a wide variety of uses in Haskell programs, from simple overloading of operators (such as equality or ordering) to complex invariants used to implement type-safe heterogeneous lists or limited subtyping. Unfortunately, many of the richer uses of type classes require extensions to the class system that have been incompletely described in the research literature and are not universally accepted within the Haskell community.

This paper describes a new type class system, implemented in a prototype tool called ilab, that simplifies and enhances Haskell-style type-class programming. In ilab, we replace overlapping instances with a new feature, instance chains, allowing explicit alternation and failure in instance declarations. We describe a technique for ascribing semantics to type class systems, relating classes, instances, and class constraints (such as kind signatures or functional dependencies) directly to a set-theoretic model of relations on types. Finally, we give a semantics for ilab and describe its implementation.

Hackage, an online repository of Haskell applications and libraries, provides a hub for programmers to both release code to and use code from the larger Haskell community. We suggest that Hackage can also serve as a valuable resource for language designers: by providing a large collection of code written by different programmers and in different styles, it allows language designers to see not just how features could be used theoretically, but how they are (and are not) used in practice.

We were able to make such a use of Hackage during the design of the class system for a new Haskell-like programming language. In this paper, we sketch our language design problem, and how we used Hackage to help answer it. We describe our methodology in some detail, including both ways that it was and was not effective, and summarize our results.