The Dependent Calculus of Indistinguishability (DCOI) uses dependency tracking to identify irrelevant arguments and uses indistinguishability during type conversion to enable proof irrelevance, supporting run-time and compile-time irrelevance with the same uniform mechanism. DCOI also internalizes reasoning about indistinguishability through the use of a propositional equality type indexed by an observer level.

As DCOI is a pure type system, prior work establishes only its syntactic type safety, justifying its use as the basis for a programming language with dependent types. However, it was not clear whether any instance of this system would be suitable for use as a type theory for theorem proving. Here, we identify a suitable instance DCOIω, which has an infinite predicative universe hierarchy. We show that DCOIω is logically consistent, normalizing, and that type conversion is decidable. We have mechanized all results using the Coq proof assistant.

Effect and coeffect tracking integrate many types of compile-time analysis, such as cost, liveness, or dataflow, directly into a language's type system. In this paper, we investigate the addition of effect and coeffect tracking to the type system of call-by-push-value (CBPV), a computational model useful in compilation for its isolation of effects and for its ability to cleanly express both call-by-name and call-by-value computations. Our main result is effect-and-coeffect soundness, which asserts that the type system accurately bounds the effects that the program may trigger during execution and accurately tracks the demands that the program may make on its environment. This result holds for two different dynamic semantics: a generic one that can be adapted for different coeffects and one that is adapted for reasoning about resource usage. In particular, the second semantics discards the evaluation of unused values and pure computations while ensuring that effectful computations are always evaluated, even if their results are not required. Our results have been mechanized using the Coq proof assistant.

Lazy evaluation is a powerful tool that enables better compositionality and potentially better performance in functional programming, but it is challenging to analyze its computation cost. Existing works either require manually annotating sharing, or rely on separation logic to reason about heaps of mutable cells. In this paper, we propose a bidirectional demand semantics that allows for extrinsic reasoning about the computation cost of lazy programs without relying on special program logics. To show the effectiveness of our approach, we apply the demand semantics to a variety of case studies including insertion sort, selection sort, Okasaki's banker's queue, and the implicit queue. We formally prove that the banker's queue and the implicit queue are both amortized and persistent using the Rocq Prover (formerly known as Coq). We also propose the reverse physicist's method, a novel variant of the classical physicist's method, which enables mechanized, modular and compositional reasoning about amortization and persistence with the demand semantics.

Keywords: formal verification, computation cost, lazy evaluation, amortized analysis

In type systems with dependency tracking, programmers can assign an ordered set of levels to computations and prevent information flow from high-level computations to the low-level ones. The key notion in such systems is indistinguishability: a definition of program equivalence that takes into account the parts of the program that an observer may depend on. In this paper, we investigate the use of dependency tracking in the context of dependently-typed languages. We present the Dependent Calculus of Indistinguishability (DCOI), a system that adopts indistinguishability as the definition of equality used by the type checker. DCOI also internalizes that relation as an observer-indexed propositional equality type, so that programmers may reason about indistinguishability within the language. Our design generalizes and extends prior systems that combine dependency tracking with dependent types and is the first to support conversion and propositional equality at arbitrary observer levels. We have proven type soundness and noninterference theorems for DCOI and have developed a prototype implementation of its type checker.

Keywords: Coq, Dependent Types, Formalization, Modes

In dependently-typed functional programming languages that allow general recursion, programs used as proofs must be evaluated to retain type soundness. As a result, programmers must make a trade-off between performance and safety. To address this problem, we propose System DE, an explicitly-typed, moded core calculus that supports termination tracking and equality reflection. Programmers can write inductive proofs about potentially diverging programs in a logical sublanguage and reflect those proofs to the type checker, while knowing that such proofs will be erased by the compiler before execution. A key feature of System DE is its use of modes for both termination and relevance tracking, which not only simplifies the design but also leaves it open for future extension. System DE is suitable for use in the Glasgow Haskell Compiler, but could serve as the basis for any general purpose dependently-typed language.

Keywords: Modes, Equality Reflection, Haskell, Dependent Types

Free monads (and their variants) have become a popular general-purpose tool for representing the semantics of effectful programs in proof assistants. These data structures support the compositional definition of semantics parameterized by uninterpreted events, while admitting a rich equational theory of equivalence. But monads are not the only way to structure effectful computation, why should we limit ourselves? In this paper, inspired by applicative functors, selective functors, and other structures, we define a collection of data structures and theories, which we call program adverbs, that capture a variety of computational patterns. Program adverbs are themselves composable, allowing them to be used to specify the semantics of languages with multiple computation patterns. We use program adverbs as the basis for a new class of semantic embeddings called Tlön embeddings. Compared with embeddings based on free monads, Tlön embeddings allow more flexibility in computational modeling of effects, while retaining more information about the program’s syntactic structure.

Over twenty years ago, Abadi et al. established the Dependency Core Calculus (DCC) as a general purpose framework for analyzing dependency in typed programming languages. Since then, dependency analysis has shown many practical benefits to language design: its results can help users and compilers enforce security constraints, eliminate dead code, among other applications. In this work, we present a Dependent Dependency Calculus (DDC), which extends this general idea to the setting of a dependently-typed language. We use this calculus to track both run-time and compile-time irrelevance, enabling faster type-checking and program execution.

Lazy evaluation is a powerful tool for functional programmers. It enables the concise expression of on-demand computation and a form of compositionality not available under other evaluation strategies. However, the stateful nature of lazy evaluation makes it hard to analyze a program’s computational cost, either informally or formally. In this work, we present a novel and simple framework for formally reasoning about lazy computation costs based on a recent model of lazy evaluation: clairvoyant call-by-value. The key feature of our framework is its simplicity, as expressed by our definition of the clairvoyance monad. This monad is both simple to define (around 20 lines of Coq) and simple to reason about. We show that this monad can be effectively used to mechanically reason about the computational cost of lazy functional programs written in Coq.

Despite the great success of inferring and programming with universal types, their dual—existential types—are much harder to work with. Existential types are useful in building abstract types, working with indexed types, and providing first-class support for refinement types. This paper, set in the context of Haskell, presents a bidirectional type-inference algorithm that infers where to introduce and eliminate existentials without any annotations in terms, along with an explicitly typed, type-safe core language usable as a compilation target. This approach is backward compatible. The key ingredient is to use strong existentials, which support (lazily) projecting out the encapsulated data, not weak existentials accessible only by pattern-matching.

Keywords: Coq, Haskell, verification

Keywords: Dependent Types, Haskell

We introduce our efforts within the project The science of deep specification to work out the key formal underpinnings of industrial-scale formal specifications of software and hardware components, anticipating a world where large verified systems are routinely built out of smaller verified components that are also used by many other projects. We identify an important class of specification that has already been used in a few experiments that connect strong component-correctness theorems across the work of different teams. To help popularize the unique advantages of that style, we dub it deep specification, and we say that it encompasses specifications that are rich, two-sided, formal and live (terms that we define in the article). Our core team is developing a proof-of-concept system (based on the Coq proof assistant) whose specification and verification work is divided across largely decoupled subteams at our four institutions, encompassing hardware microarchitecture, compilers, operating systems and applications, along with cross-cutting principles and tools for effective specification. We also aim to catalyse interest in the approach, not just by basic researchers but also by users in industry.This article is part of the themed issue Verified trustworthy software systems.

AbstractGenerative type abstractions – present in Haskell, OCaml, and other languages – are useful concepts to help prevent programmer errors. They serve to create new types that are distinct at compile time but share a run-time representation with some base type. We present a new mechanism that allows for zero-cost conversions between generative type abstractions and their representations, even when such types are deeply nested. We prove type safety in the presence of these conversions and have implemented our work in GHC.

Most dependently-typed programming languages either require that all expressions terminate (e.g. Coq, Agda, and Epigram), or allow infinite loops but are inconsistent when viewed as logics (e.g. Haskell, ATS, Ωmega. Here, we combine these two approaches into a single dependently-typed core language. The language is composed of two fragments that share a common syntax and overlapping semantics: a logic that guarantees total correctness, and a call-by-value programming language that guarantees type safety but not termination. The two fragments may interact: logical expressions may be used as programs; the logic may soundly reason about potentially nonterminating programs; programs can require logical proofs as arguments; and "mobile" program values, including proofs computed at runtime, may be used as evidence by the logic. This language allows programmers to work with total and partial functions uniformly, providing a smooth path from functional programming to dependently-typed programming.

Keywords: termination, dependent types, general recursion

Generative type abstractions -- present in Haskell, OCaml, and other languages -- are useful concepts to help prevent programmer errors. They serve to create new types that are distinct at compile time but share a run-time representation with some base type. We present a new mechanism that allows for zero-cost conversions between generative type abstractions and their representations, even when such types are deeply nested. We prove type safety in the presence of these conversions and have implemented our work in GHC.

Keywords: type class, coercion, newtype deriving, haskell

System FC, the core language of the Glasgow Haskell Compiler, is an explicitly-typed variant of System F with first-class type equality proofs called coercions. This extensible proof system forms the foundation for type system extensions such as type families (type-level functions) and Generalized Algebraic Datatypes (GADTs). Such features, in conjunction with kind polymorphism and datatype promotion, support expressive compile-time reasoning.However, the core language lacks explicit kind equality proofs. As a result, type-level computation does not have access to kind-level functions or promoted GADTs, the type-level analogues to expression-level features that have been so useful. In this paper, we eliminate such discrepancies by introducing kind equalities to System FC. Our approach is based on dependent type systems with heterogeneous equality and the "Type-in-Type" axiom, yet it preserves the metatheoretic properties of FC. In particular, type checking is simple, decidable and syntax directed. We prove the preservation and progress theorems for the extended language.

Keywords: equality, dependent types, haskell

Modular languages support generative type abstraction, ensuring that an abstract type is distinct from its representation, except inside the implementation where the two are synonymous. We show that this well-established feature is in tension with the non-parametric features of newer type systems, such as indexed type families and GADTs. In this paper we solve the problem by using kinds to distinguish between parametric and non-parametric contexts. The result is directly applicable to Haskell, which is rapidly developing support for type-level computation, but the same issues should arise whenever generativity and non-parametric features are combined.

Keywords: generic programming, haskell, name binding, patterns

This paper proposes a type-and-effect system that distinguishes terminating terms and total functions from possibly diverging terms and partial functions, for a lambda calculus with general recursion and equality types. The central idea is to include a primitive type-form “Terminates t”, expressing that term t is terminating; and then allow terms t to be coerced from possibly diverging to total, using a proof of Terminates t. We call such coercions termination casts, and show how to implement terminating recursion using them. For the meta-theory of the system, we describe a translation from this system to a logical theory of termination for general recursive, simply typed functions. Every typing judgment of this system is translated to a theorem expressing the appropriate termination property of the computational part of the term.

Propositions that express type equality are a frequent ingredient of modern functional programming---they can encode generic functions, dynamic types, and GADTs. Via the Curry-Howard correspondence, these propositions are ordinary types inhabited by proof terms, computed using runtime type representations. In this paper we show that two examples of type equality propositions actually do reflect type equality; they are only inhabited when their arguments are equal and their proofs are unique (up to contextual equivalence.) We show this result in the context of a strongly normalizing language with higher-order polymorphism and primitive recursion over runtime type representations by proving Reynolds's abstraction theorem. We then use this theorem to derive “free” theorems about equality types.

The definition of type equivalence is one of the most important design issues for any typed language. In dependently-typed languages, because terms appear in types, this definition must rely on a definition of term equivalence. In that case, decidability of type checking requires decidability for the term equivalence relation.

Almost all dependently-typed languages require this relation to be decidable. Some, such as Coq, Epigram or Agda, do so by employing analyses to force all programs to terminate. Conversely, others, such as DML, ATS, Omega, or Haskell, allow nonterminating computation, but do not allow those terms to appear in types. Instead, they identify a terminating index language and use singleton types to connect indices to computation. In both cases, decidable type checking comes at a cost, in terms of complexity and expressiveness.

Conversely, the benefits to be gained by decidable type checking are modest. Termination analyses allow dependently typed programs to verify total correctness properties. However, decidable type checking is not a prerequisite for type safety. Furthermore, decidability does not imply tractability. A decidable approximation of program equivalence may not be useful in practice.

Therefore, we take a different approach: instead of a fixed notion for term equi valence, we parameterize our type system with an abstract relation that is not n ecessarily decidable. We then design a novel set of typing rules that require on ly weak properties of this abstract relation in the proof of the preservation an d progress lemmas. This design provides flexibility: we compare valid instantiat ions of term equivalence which range from beta-equivalence, to contextual equiva lence, to some exotic equivalences.

Since Findler and Felleisen introduced higher-order contracts, many variants have been proposed. Broadly, these fall into two groups: some follow Findler and Felleisen 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, who defined a latent calculus lambdac and a manifest calculus lambdah, gave a translation phi from lambdac to lambdah, and proved that, if a lambdac term reduces to a constant, then so does its phiimage. We enrich their account with a translation psi from lambdah to lambdac 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 lambdah and two dialects (“lax” and “picky”) of lambdac, establish type soundness---a substantial result in itself, for lambdah---and extend phi and psi 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.

Many programs operate reactively---patiently waiting for user input, running for a while producing output, and eventually returning to a state where they are ready to accept another input (or occasionally diverging). When a reactive program communicates with multiple parties, we would like to be sure that it can be given secret information by one without leaking it to others. Motivated by web browsers and client-side web applications, we explore definitions of noninterference for reactive programs and identify two of special interest---one corresponding to termination-insensitive noninterference for a simple sequential language, the other to termination-sensitive noninterference. We focus on the former and develop a proof technique for showing that program behaviors are secure according to this definition. To demonstrate the viability of the approach, we define a simple reactive language with an information-flow type system and apply our proof technique to show that well-typed programs are secure.

Languages supporting polymorphism typically have ad-hoc restrictions on where polymorphic types may occur. Supporting “first-class” polymorphism, by lifting those restrictions, is obviously desirable, but it is hard to achieve this without sacrificing type inference. We present a new type system for higher-rank and impredicative polymorphism that improves on earlier proposals: it is an extension of Damas-Milner; it relies only on System F types; it has a simple, declarative specification; it is robust to program transformations; and it enjoys a complete and decidable type inference algorithm.

This paper defines Aspectml, a typed functional, aspect-oriented programming language. The main contribution of Aspectml is the seamless integration of polymorphism, run-time type analysis and aspect-oriented programming language features. In particular, Aspectml allows programmers to define type-safe polymorphic advice using pointcuts constructed from a collection of polymorphic join points. Aspectml also comes equipped with a type inference algorithm that conservatively extends Hindley-Milner type inference. To support first-class polymorphic point-cut designators, a crucial feature for developing aspect-oriented profiling or logging libraries, the algorithm blends the conventional Hindley-Milner type inference algorithm with a simple form of local type inference.

We give our language operational meaning via a type-directed translation into an expressive type-safe intermediate language. Many complexities of the source language are eliminated in this translation, leading to a modular specification of its semantics. One of the novelties of the intermediate language is the definition of polymorphic labels for marking control-flow points. These labels are organized in a tree structure such that a parent in the tree serves as a representative for all of its children. Type safety requires that the type of each child is less polymorphic than its parent type. Similarly, when a set of labels is assembled as a pointcut, the type of each label is an instance of the type of the pointcut.

Machine-checked proofs of properties of programming languages have become a critical need, both for increased confidence in large and complex designs and as a foundation for technologies such as proof-carrying code. However, constructing these proofs remains a black art, involving many choices in the formulation of definitions and theorems that make a huge cumulative difference in the difficulty of carrying out large formal developments. The representation and manipulation of terms with variable binding is a key issue.

We propose a novel style for formalizing metatheory, combining locally nameless representation of terms and cofinite quantification of free variable names in inductive definitions of relations on terms (typing, reduction, ...). The key technical insight is that our use of cofinite quantification obviates the need for reasoning about equivariance (the fact that free names can be renamed in derivations); in particular, the structural induction principles of relations defined using cofinite quantification are strong enough for metatheoretic reasoning, and need not be explicitly strengthened. Strong inversion principles follow (automatically, in Coq) from the induction principles. Although many of the underlying ingredients of our technique have been used before, their combination here yields a significant improvement over existing methodology, leading to developments that are faithful to informal practice, yet require no external tool support and little infrastructure within the proof assistant.

We have carried out several large developments in this style using the Coq proof assistant and have made them publicly available. Our developments include type soundness for and ML (with references, exceptions, datatypes, recursion and patterns) and subject reduction for the Calculus of Constructions. Not only do these developments demonstrate the comprehensiveness of our approach; they have also been optimized for clarity and robustness, making them good templates for future extension.

Higher-order abstract syntax is a simple technique for implementing languages with functional programming. Object variables and binders are implemented by variables and binders in the host language. By using this technique, one can avoid implementing common and tricky routines dealing with variables, such as capture-avoiding substitution. However, despite the advantages this technique provides, it is not commonly used because it is difficult to write sound elimination forms (such as folds or catamorphisms) for higherorder abstract syntax. To fold over such a datatype, one must either simultaneously define an inverse operation (which may not exist) or show that all functions embedded in the datatype are parametric.

In this paper, we show how first-class polymorphism can be used to guarantee the parametricity of functions embedded in higher-order abstract syntax. With this restriction, we implement a library of iteration operators over data-structures containing functionals. From this implementation, we derive fusion laws that functional programmers may use to reason about the iteration operator. Finally, we show how this use of parametric polymorphism corresponds to the Schürmann, Despeyroux and Pfenning method of enforcing parametricity through modal types. We do so by using this library to give a sound and complete encoding of their calculus into System F-omega. This encoding can serve as a starting point for reasoning about higher-order structures in polymorphic languages.

Reynolds' abstraction theorem, often referred to as the parametricity theorem, can be used to derive properties about functional programs solely from their types. Unfortunately, in the presence of runtime type analysis, the abstraction properties of polymorphic programs are no longer valid. However, runtime type analysis can be implemented with term-level representations of types, as in the language of Crary et al., where case analysis on these runtime representations introduces type refinement. In this paper, we show that representation-based analysis is consistent with type abstraction by extending the abstraction theorem to such a language. We also discuss the “free theorems” that result. This work provides a foundation for the more general problem of extending the abstraction theorem to languages with generalized algebraic datatypes.

Haskell's popularity has driven the need for ever more expressive type system features, most of which threaten the decidability and practicality of Damas-Milner type inference. One such feature is the ability to write functions with higher-rank types --- that is, functions that take polymorphic functions as their arguments.

Complete type inference is known to be undecidable for higher-rank (impredicative) type systems, but in practice programmers are more than willing to add type annotations to guide the type inference engine, and to document their code. However, the choice of just what annotations are required, and what changes are required in the type system and its inference algorithm, has been an ongoing topic of research.

We take as our starting point a lambda-calculus proposed by Odersky and Laufer. Their system supports arbitrary-rank polymorphism through the exploitation of type annotations on lambda-bound arguments and arbitrary sub-terms. Though elegant, and more convenient than some other proposals, Odersky and Laufer's system requires many annotations. We show how to use local type inference (invented by Pierce and Turner) to greatly reduce the annotation burden, to the point where higher-rank types become eminently usable.

Higher-rank types have a very modest impact on type inference. We substantiate this claim in a very concrete way, by presenting a complete type-inference engine, written in Haskell, for a traditional Damas-Milner type system, and then showing how to extend it for higher-rank types. We write the type-inference engine using a monadic framework: it turns out to be a particularly compelling example of monads in action.

The paper is long, but is strongly tutorial in style.

Polytypic programming is a way of defining type-indexed operations, such as map, fold and zip, based on type information. Run-time polytypic programming allows that type information to be dynamically computed---this support is essential in modern programming languages that support separate compilation, first-class type abstraction, or polymorphic recursion.

However, in previous work we defined run-time polytypic programming with a type-passing semantics. Although it is natural to define polytypic programs as operating over first-class types, such a semantics suffers from a number of drawbacks. This paper describes how to recast that work in a type-erasure semantics, where terms represent type information in a safe manner. The resulting language is simple and easy to implement---we present a prototype implementation of the necessary machinery as a small Haskell library.

Generalized algebraic data types (GADTs), sometimes known as “guarded recursive data types” or “first-class phantom types”, are a simple but powerful generalization of the data types of Haskell and ML. Recent works have given compelling examples of the utility of GADTs, although type inference is known to be difficult. Our contribution is to show how to exploit programmer-supplied type annotations to make the type inference task almost embarrassingly easy. Our main technical innovation is wobbly types, which express in a declarative way the uncertainty caused by the incremental nature of typical type-inference algorithms.

Languages with rich type systems are beginning to employ a blend of type inference and type checking, so that the type inference engine is guided by programmer-supplied type annotations. In this paper we show, for the first time, how to combine the virtues of two well-established ideas: unification-based inference, and bidirectional propagation of type annotations. The result is a type system that conservatively extends Hindley-Milner, and yet supports both higher-rank types and impredicativity.

Type-directed programming is an important idiom for software design. In type-directed programming the behavior of programs is guided by the type structure of data. It makes it possible to implement many sorts of operations, such as serialization, traversals, and queries, only once and without needing to continually revise their implementation as new data types are defined.

Type-directed programming is the basis for recent research into "scrapping" tedious boilerplate code that arises in functional programming with algebraic data types. This research has primarily focused on writing type-directed functions that are closed to extension. However, Lämmel and Peyton Jones recently developed a technique for writing openly extensible type-directed functions in Haskell by making clever use of type classes. Unfortunately, this technique has a number of limitations.

We present an alternate approach to writing openly extensible type-directed functions by using the aspect-oriented programming features provided by the language AspectML. Our solution not only avoids the limitations present in Lämmel and Peyton Jones technique, but also allows type-directed functions to be extended at any time with cases for types that were not even known at compile-time. This capability is critical to writing programs that make use of dynamic loading or runtime type generativity.

Some type class instances can be automatically derived from the structure of types. As a result, the Haskell language includes the "deriving" mechanism to automatic generates such instances for a small number of built-in type classes. In this paper, we present RepLib, a GHC library that enables a similar mechanism for arbitrary type classes. Users of RepLib can define the relationship between the structure of a datatype and the associated instance declaration by a normal Haskell functions that pattern-matches a representation types. Furthermore, operations defined in this manner are extensible---instances for specific types not defined by type structure may also be incorporated. Finally, this library also supports the definition of operations defined by parameterized types.

We explore an axiomatized nominal approach to variable binding in Coq, using an untyped lambda-calculus as our test case. In our nominal approach, alpha-equality of lambda terms coincides with Coq's built-in equality. Our axiomatization includes a nominal induction principle and functions for calculating free variables and substitution. These axioms are collected in a module signature and proved sound using locally nameless terms as the underlying representation. Our experiences so far suggests that it is feasible to work from such axiomatized theories in Coq and that the nominal style of variable binding corresponds closely with paper proofs. We are currently working on proving the soundness of a primitive recursion combinator and developing a method of generating these axioms and their proof of soundness from a grammar describing the syntax of terms and binding.

How close are we to a world in which mechanically verified software is commonplace? A world in which theorem proving technology is used routinely by both software developers and programming language researchers alike? One crucial step towards achieving these goals is mechanized reasoning about language metatheory. The time has come to bring together the theorem proving and programming language communities to address this problem. We have proposed the POPLMark challenge as a concrete set of benchmarks intended both for measuring progress in this area and for stimulating discussion and collaboration. Our goal is to push the boundaries of existing technology to the point where we can achieve mechanized metatheory for the masses.

This paper defines PolyAML, a typed functional and aspect-oriented programming language. The main contribution of PolyAML is in the seamless integration of polymorphism, run-time type analysis and aspect-oriented programming language features. In particular, PolyAML allows programmers to define type-safe polymorphic advice using pointcuts constructed from a collection of polymorphic join points. PolyAML also comes equipped with a type inference algorithm that conservatively extends Hindley-Milner type inference. In order to support first-class polymorphic point-cut designators, a crucial feature for developing aspect-oriented profiling or logging libraries, the algorithm blends the conventional Hindley-Milner type inference algorithm with a simple form of local type inference.

We give our language operational meaning via a type-directed translation into an expressive type-safe intermediate language. Many complexities of the source language are eliminated in this translation, leading to a modular specification of its semantics. One of the novelties of the intermediate language is the definition of polymorphic labels for marking control-flow points. These labels are organized in a tree structure such that a parent in the tree serves as a representative for the collection of all its children. Type safety requires that the type of each child is a generic instance of the type of the polymorphic parent. Similarly, when a set of labels is assembled as a pointcut, the type of each label is an instance of the type of the pointcut.

How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machine-checked proofs?

We propose a concrete set of benchmarks for measuring progress in this area. Based on the metatheory of System F-sub, a typed lambda-calculus with second-order polymorphism, subtyping, and records, these benchmarks embody many aspects of programming languages that are challenging to formalize: variable binding at both the term and type levels, syntactic forms with variable numbers of components (including binders), and proofs demanding complex induction principles. We hope that these benchmarks will help clarify the current state of the art, provide a basis for comparing competing technologies, and motivate further research.

Run-time type analysis allows programmers to easily and concisely define many operations based upon type structure, such as serialization, iterators, and structural equality. However, when types can be inspected at run time, nothing is secret. A module writer cannot use type abstraction to hide implementation details from clients: those clients can use type analysis to determine the structure of these supposedly “abstract” data types. Furthermore, access control mechanisms do not help in isolating the implementation of abstract datatypes from their clients. Buggy or malicious authorized modules may simply leak type information to unauthorized clients, so module implementors cannot reliably tell which parts of a program rely on their type definitions and which parts do not.

Currently, module implementors rely on parametric polymorphism to provide guarantees about the use of their abstract datatypes. Standard type parametricity does not hold for a language with run-time type analysis, but in this paper we show how to generalize the statement of parametricity so that it does hold in the presence of type analysis and still encompasses the integrity and confidentiality policies that are normally derived from parametricity. The key is to augment the type system with annotations about information flow. Because the type system tracks the flow of dynamic type information, the implementor of an abstract data type can easily see what parts of the program depend on the implementation of a given type.

Two different ways of defining ad-hoc polymorphic operations commonly occur in programming languages. With the first form polymorphic operations are defined inductively on the structure of types while with the second form polymorphic operations are defined for specific sets of types.

In intensional type analysis operations are defined by induction on the structure of types. Therefore no new cases are necessary for user-defined types, because these types are equivalent to their underlying structure. However, intensional type analysis is “closed” to extension, as the behavior of the operations cannot be differentiated for the new types, thus destroying the distinctions that these types are designed to express.

Haskell type classes on the other hand define polymorphic operations for sets of types. Operations defined by class instances are considered “open”---the programmer can add instances for new types without modifying existing code. However, the operations must be extended with specialized code for each new type, and it may be tedious or even impossible to add extensions that apply to a large universe of new types.

Both approaches have their benefits, so it is important to let programmers decide which is most appropriate for their needs. In this paper, we define a language that supports both forms of ad-hoc polymorphism, using the same basic constructs.

Comparing two types for equality is an essential ingredient for an implementation of dynamic types. Once equality has been established, it is safe to cast a value from one type to another. In a language with run-time type analysis, implementing such a procedure is fairly straightforward. Unfortunately, this naive implementation destructs and rebuilds the argument while iterating over its type structure. However, by using higher-order polymorphism, a casting function can treat its argument parametrically. We demonstrate this solution in two frameworks for ad-hoc polymorphism: intensional type analysis and Haskell type classes.

Type-directed programming is an important and widely used paradigm in the design of software. With this form of programming, an application may analyze type information to determine its behavior. By analyzing the structure of data, many operations, such as serialization, cloning, adaptors and iterators may be defined once, for all types of data. That way, as the program evolves, these operations need not be updated---they will automatically adapt to new data forms. Otherwise, each of these operations must be individually redefined for each type of data, forcing programmers to revisit the same program logic many times during a program's lifetime.

The Java language supports type directed programming with the instanceof operator and the Java Reflection API. These mechanisms allow Java programs to depend on the name and structure of the run-time classes of objects. However, the Java mechanisms for type-directed programming are difficult to use. They also do not integrate well with generics, an important new feature of the Java language.

In this paper, we describe the design of several expressive new mechanisms for type-directed programming in Java, and show that these mechanisms are sound when included in a language similar to Featherweight Java. Basically, these new mechanisms pattern-match the name and structure of the type parameters of generic code, instead of the run-time classes of objects. Therefore, they naturally integrate with generics and provide strong guarantees about program correctness. As these mechanisms are based on pattern matching, they naturally and succinctly express many operations that depend on type information. Finally, they provide programmers with some degree of protection for their abstractions. Whereas instanceof and reflection can determine the exact run-time type of an object, our mechanisms allow any supertype to be supplied for analysis, hiding its precise structure.

Higher-order abstract syntax is a simple technique for implementing languages with functional programming. Object variables and binders are implemented by variables and binders in the host language. By using this technique, one can avoid implementing common and tricky routines dealing with variables, such as capture-avoiding substitution. However, despite the advantages this technique provides, it is not commonly used because it is difficult to write sound elimination forms (such as folds or catamorphisms) for higher-order abstract syntax. To fold over such a datatype, one must either simultaneously define an inverse operation (which may not exist) or show that all functions embedded in the datatype are parametric.

In this paper, we show how first-class polymorphism can be used to guarantee the parametricity of functions embedded in higher-order abstract syntax. With this restriction, we implement a library of iteration operators over data-structures containing functionals. From this implementation, we derive “fusion laws” that functional programmers may use to reason about the iteration operator. Finally, we show how this use of parametric polymorphism corresponds to the Schuermann, Despeyroux and Pfenning method of enforcing parametricity through modal types. We do so by using this library to give a sound and complete encoding of their calculus into System F-omega. This encoding can serve as a starting point for reasoning about higher-order structures in polymorphic languages.

Intensional polymorphism, the ability to dispatch to different routines based on types at run time, enables a variety of advanced implementation techniques for polymorphic languages, including tag-free garbage collection, unboxed function arguments, polymorphic marshalling, and flattened data structures. To date, languages that support intensional polymorphism have required a type-passing (as opposed to type-erasure) interpretation where types are constructed and passed to polymorphic functions at run time. Unfortunately, type-passing suffers from a number of drawbacks; it requires duplication of constructs at the term and type levels, it prevents abstraction, and it severely complicates polymorphic closure conversion. We present a type-theoretic framework that supports intensional polymorphism, but avoids many of the disadvantages of type passing. In our approach, run-time type information is represented by ordinary terms. This avoids the duplication problem, allows us to recover abstraction, and avoids complications with closure conversion. In addition, our type system provides another improvement in expressiveness; it allows unknown types to be refined in place thereby avoiding certain beta-expansions required by other frameworks.

Intensional type analysis provides the ability to analyze abstracted types at run time. In this paper, we extend that ability to higher-order and kind-polymorphic type constructors. The resulting language is elegant and expressive: we show through examples how it extends the repertoire of polytypic functions that may be defined.

Languages for intensional type analysis permit ad-hoc polymorphism, or run-time analysis of types. However, such languages require complex, specialized constructs to support this operation, which hinder optimization and complicate the meta-theory of these languages. In this paper, we observe that such specialized operators need not be intrinsic to the language, and in fact, their operation may be simulated through standard encodings of iteration in the polymorphic lambda calculus. Therefore, we may more easily add intensional analysis operators to complicated languages via a translation semantics, instead of through language extension.

We present the design and implementation of the first complete framework for flexible and safe dynamic linking of native code. Our approach extends Typed Assembly Language with a primitive for loading and typechecking code, which is flexible enough to support a variety of linking strategies, but simple enough that it does not significantly expand the trusted computing base. Using this primitive, along with the ability to compute with types, we show that we can program many existing dynamic linking approaches. As a concrete demonstration, we have used our framework to implement dynamic linking for a type-safe dialect of C, closely modeled after the standard linking facility for Unix C programs. Aside from the unavoidable cost of verification, our implementation performs comparably with the standard, untyped approach.

In a language with non-parametric or ad-hoc polymorphism, it is possible to determine the identity of a type variable at run time. With this facility, we can write a function to convert a term from one abstract type to another, if the two hidden types are identical. However, the naive implementation of this function requires that the term be destructed and rebuilt. In this paper, we show how to eliminate this overhead using higher-order type abstraction. We demonstrate this solution in two frameworks for ad-hoc polymorphism: intensional type analysis and type classes.

Various code certification systems allow the certification and static verification of a variety of important safety properties such as memory safety and control-flow safety. These systems provide valuable tools for verifying that untrusted and potentially malicious code is safe before execution. However, one important safety property that is not usually included is that programs adhere to specific bounds on resource consumption, such as running time.

We present a decidable type system capable of specifying and certifying bounds on resource consumption. Our system makes two advances over previous resource bound certification systems, both of which are necessary for a practical system: we allow the execution time of programs and their subroutines to vary, depending on their arguments, and we provide a fully automatic compiler generating certified executables from source-level programs. The principal device in our approach is a strategy for simulating dependent types using sum and inductive kinds.

Run-time type dispatch enables a variety of advanced optimization techniques for polymorphic languages, including tag-free garbage collection, unboxed function arguments, and flattened data structures. However, modern type-preserving compilers transform types between stages of compilation, making type dispatch prohibitively complex at low levels of typed compilation. It is crucial therefore for type analysis at these low levels to refer to the types of previous stages. Unfortunately, no current intermediate language supports this facility.

To fill this gap, we present the language LX, which provides a rich language of type constructors supporting type analysis (possibly of previous-stage types) as a programming idiom. This language is quite flexible, supporting a variety of other applications such as analysis of quantified types, analysis with incomplete type information, and type classes. We also show that LX is compatible with a type-erasure semantics.

The goal of typed assembly language (TAL) is to provide a low-level, statically typed target language that is better suited than Java bytecodes for supporting a wide variety of source languages and a number of important optimizations. In previous work, we formalized idealized versions of TAL and proved important safety properties about them. In this paper, we present our progress in defining and implementing a realistic typed assembly language called TALx86. The TALx86 instructions comprise a relatively complete fragment of the Intel IA32 (32-bit 80x86 flat model) assembly language and are thus executable on processors such as the Intel Pentium. The type system for the language incorporates a number of advanced features necessary for safely compiling large programs to good code.

To motivate the design of the type system, we demonstrate how various high-level language features are compiled to TALx86. For this purpose, we present a type-safe C-like language called Popcorn.

Intensional polymorphism, the ability to dispatch to different routines based on types at run time, enables a variety of advanced implementation techniques for polymorphic languages, including tag-free garbage collection, unboxed function arguments, polymorphic marshalling, and flattened data structures. To date, languages that support intensional polymorphism have required a type-passing (as opposed to type-erasure) interpretation where types are constructed and passed to polymorphic functions at run time. Unfortunately, type-passing suffers from a number of drawbacks; it requires duplication of constructs at the term and type levels, it prevents abstraction, and it severely complicates polymorphic closure conversion. We present a type-theoretic framework that supports intensional polymorphism, but avoids many of the disadvantages of type passing. In our approach, run-time type information is represented by ordinary terms. This avoids the duplication problem, allows us to recover abstraction, and avoids complications with closure conversion. In addition, our type system provides another improvement in expressiveness; it allows unknown types to be refined in place thereby avoiding certain beta-expansions required by other frameworks.

MrSpidey is a user-friendly, interactive static debugger for Scheme. A static debugger supplements the standard debugger by analyzing the program and pinpointing those program operations tha may cause run-time errors suce as dereferencing the null pointer or applying non-functions. The program analysis of MrSpidey computes value set descriptions for each term in the program and constructs a value flow graph connecting the set descriptions. Using the set descriptions, MrSpidey can identify and highlight potentially erroneous program operations, whose cause the programmer can the explore by selectively exposing portions of the value flow graph.

Run-time type analysis is an increasingly important linguistic mechanism in modern programming languages. Language runtime systems use it to implement services such as accurate garbage collection, serialization, cloning and structural equality. Component frameworks rely on it to provide reflection mechanisms so they may discover and interact with program interfaces dynamically. Run-time type analysis is also crucial for large, distributed systems that must be dynamically extended, because it allows those systems to check program invariants when new code and new forms of data are added. Finally, many generic user-level algorithms for iteration, pattern matching, and unification can be defined through type analysis mechanisms.

However, existing frameworks for run-time type analysis were designed for simple type systems. They do not scale well to the sophisticated type systems of modern and next-generation programming languages that include complex constructs such as first-class abstract types, recursive types, objects, and type parameterization. In addition, facilities to support type analysis often require complicated language semantics that allow little freedom in their implementation. This dissertation investigates the foundations of run-time type analysis in the context of statically-typed, polymorphic programming languages. Its goal is to show how such a language may support type-analyzing operations in a way that balances expressiveness, safety and simplicity.

This artifact contains the complete mechanized Coq proofs of the lemmas and theorems about System DE. The VM image is preinstalled with the dependencies required to build and verify the Coq development.

Keywords: Coq, Dependent types, Mechanized metatheory

Modular languages support generative type abstraction, ensuring that an abstract type is distinct from its representation, except inside the implementation where the two are synonymous. We show that this well-established feature is in tension with the non-parametric features of newer type systems, such as indexed type families and GADTs. In this paper we solve the problem by using kinds to distinguish between parametric and non-parametric contexts. The result is directly applicable to Haskell, which is rapidly developing support for type-level computation, but the same issues should arise whenever generativity and non-parametric features are combined.

Run-time type analysis allows programmers to easily and concisely define many operations based upon type structure, such as serialization, iterators, and structural equality. However, when types can be inspected at run time, nothing is secret. A module writer cannot use type abstraction to hide implementation details from clients: those clients can use type analysis to determine the structure of these supposedly “abstract” data types. Furthermore, access control mechanisms do not help in isolating the implementation of abstract datatypes from their clients. Buggy or malicious authorized modules may simply leak type information to unauthorized clients, so module implementors cannot reliably tell which parts of a program rely on their type definitions and which parts do not.

Currently, module implementors rely on parametric polymorphism to provide guarantees about the use of their abstract datatypes. Standard type parametricity does not hold for a language with run-time type analysis, but in this paper we show how to generalize the statement of parametricity so that it does hold in the presence of type analysis and still encompasses the integrity and confidentiality policies that are normally derived from parametricity. The key is to augment the type system with annotations about information flow. Because the type system tracks the flow of dynamic type information, the implementor of an abstract data type can easily see what parts of the program depend on the implementation of a given type.

This paper defines PolyAML, a typed functional, aspect-oriented programming language. The main contribution of PolyAML is the seamless integration of polymorphism, run-time type analysis and aspect-oriented programming language features. In particular, PolyAML allows programmers to define type-safe polymorphic advice using pointcuts constructed from a collection of polymorphic join points. PolyAML also comes equipped with a type inference algorithm that conservatively extends Hindley-Milner type inference. To support first-class polymorphic point-cut designators, a crucial feature for developing aspect-oriented profiling or logging libraries, the algorithm blends the conventional Hindley-Milner type inference algorithm with a simple form of local type inference.

We give our language operational meaning via a type-directed translation into an expressive type-safe intermediate language. Many complexities of the source language are eliminated in this translation, leading to a modular specification of its semantics. One of the novelties of the intermediate language is the definition of polymorphic labels for marking control-flow points. These labels are organized in a tree structure such that a parent in the tree serves as a representative for all of its children. Type safety requires that the type of each child is less polymorphic than its parent type. Similarly, when a set of labels is assembled as a pointcut, the type of each label is an instance of the type of the pointcut.

We take one of the first steps towards developing a practical, statically-typed, functional, aspect-oriented programming language by showing how to integrate polymorphism and type analysis with aspect-oriented programming features. In particular, we demonstrate how to define type-safe polymorphic advice using pointcuts that unify a collection of polymorphic join points. We also introduce a new mechanism for specifying context-sensitive advice that involves pattern matching against the current stack of activation records, and meshes well with functional programming idioms. We give our language meaning via a type-directed translation into an expressive, but fairly simple, type-safe intermediate language. Many complexities of the source language are eliminated in this translation, leading to a modular specification of its semantics. One of the novelties of the intermediate language is the definition of polymorphic labels for marking control-flow points. These labels are organized in a tree structure such that a parent in the tree serves as a representative for the collection of all its children. Type safety requires that the type of each child is a generic instance of the type of the polymorphic parent. Similarly, when a set of labels is assembled as a pointcut, the type of each label is an instance of the type of the pointcut.

Ad-hoc polymorphism is a compelling addition to typed programming languages. There are two different forms of ad-hoc polymorphism. With the nominal form, the execution of an operation is determined solely by the name of the type argument, whereas with the structural form, operations are defined by case analysis on the structure of types. The two forms differ in the way that they treat user-defined types. Operations defined by the nominal approach are considered "open"--the programmer can add cases for new types without modifying existing code. The operations must be extended however with specialized code for the new types, and it may be tedious and even difficult to add extensions that apply to a potentially large universe of user-defined types. Structurally defined operations apply to new types by treating them as equal to their underlying definitions, so no new cases for new types are necessary. However this form is considered "closed" to extension, as the behaviour of the operations cannot be differentiated for the new types. This form destroys the distinctions that user-defined types are designed to express. Both approaches have their benefits, so it is important to provide both capabilities in a single language that is expressive enough to decouple the "openness" issue from the way that user-defined types are treated. We present such a language that supports both forms of ad-hoc polymorphism.

Generalised algebraic data types (GADTs), sometimes known as “guarded recursive data types” or “first-class phantom types”, are a simple but powerful generalisation of the data types of Haskell and ML. Recent works have given compelling examples of the utility of GADTs, although type inference is known to be difficult.

It is time to pluck the fruit. Can GADTs be added to Haskell, without losing type inference, or requiring unacceptably heavy type annotations? Can this be done without completely rewriting the already-complex Haskell type-inference engine, and without complex interactions with (say) type classes? We answer these questions in the affirmative, giving a type system that explains just what type annotations are required, and a prototype implementation that implements it. Our main technical innovation is wobbly types, which express in a declarative way the uncertainty caused by the incremental nature of typical type-inference algorithms.

Ad-hoc polymorphism allows the execution of programs to depend on type information. In modern systems, it is useful for implementing generic operations over data structures, such as equality, marshalling, or traversal. In the past, there have been two different forms of ad-hoc polymorphism. The nominal form dispatches on the name of the type argument, whereas the structural form operates by decomposing the structure of types. In languages with user-defined types, these two approaches are very different. Operations defined by the nominal approach are “open”---they must be extended with specialized branches for user-defined types. In contrast, structurally defined operations are closed to extension. They automatically apply to user-defined types by treating them as their underlying definitions. Both approaches have their benefits, so it important to provide both capabilities in a language. Therefore we present an expressive language that supports both forms of ad-hoc polymorphism in a single framework. Among the language's features are the ability to define both “open” and “closed” operations with a single mechanism, the ability to naturally restrict the domain of type-analyzing operations, and new mechanisms for defining higher-order polytypism and manipulating generative type definitions.

Higher-order abstract syntax is a simple technique for implementing languages with functional programming. Object variables and binders are implemented by variables and binders in the host language. By using this technique, one can avoid implementing common and tricky routines dealing with variables, such as capture-avoiding substitution. However, despite the advantages this technique provides, it is not commonly used because it is difficult to write sound elimination forms (such as folds or catamorphisms) for higher-order abstract syntax. To fold over such a datatype, one must either simultaneously define an inverse operation (which may not exist) or show that all functions embedded in the datatype are parametric.

In this paper, we show how first-class polymorphism can be used to guarantee the parametricity of functions embedded in higher-order abstract syntax. With this restriction, we implement a library of iteration operators over data-structures containing functionals. From this implementation, we derive "fusion laws" that functional programmers may use to reason about the iteration operator. Finally, we show how this use of parametric polymorphism corresponds to the Schuermann, Despeyroux and Pfenning method of enforcing parametricity through modal types. We do so by using this library to give a sound and complete encoding of their calculus into System F-omega. This encoding can serve as a starting point for reasoning about higher-order structures in polymorphic languages.

We present the load-calculus, used to model dynamic loading, and prove it sound. The calculus extends the polymorphic lambda-calculus with a load primitive that dynamically loads terms that are closed, with respect to values. The calculus is meant to approximate the process of dynamic loading in TAL/Load , a version of Typed Assembly Language extending with dynamic linking. To model the key aspects of TAL, the calculus contains references and facilities for named types. Loadable programs may refer to named types defined by the running program, and may export new types to code loaded later. Our approach follows the framework initially outlined by Glew et. al. This calculus has been implemented in the TALx86 version of Typed Assembly Language, and is used to implement a full-featured dynamic linking library, DLpop.