Abstract Recursive types and bounded quantification are prominent features in many modern programming languages, such as Java, C#, Scala, or TypeScript. Unfortunately, the interaction between recursive types, bounded quantification, and subtyping has shown to be problematic in the past. Consequently, defining a simple foundational calculus that combines those features and has desirable properties, such as decidability , transitivity of subtyping, conservativity , and a sound and complete algorithmic formulation, has been a long-time challenge. This paper shows how to extend $F_{\le}$ with iso-recursive types in a new calculus called $F_{\le}^{\mu}$ . $F_{\le}$ is a well-known polymorphic calculus with bounded quantification. In $F_{\le}^{\mu}$ , we add iso-recursive types and correspondingly extend the subtyping relation with iso-recursive subtyping using the recently proposed nominal unfolding rules. In addition, we use so-called structural folding/unfolding rules for typing iso-recursive expressions, inspired by the structural unfolding rule proposed by Abadi et al . (1996). The structural rules add expressive power to the more conventional folding/unfolding rules in the literature, and they enable additional applications. We present several results, including: type soundness; transitivity; the conservativity of $F_{\le}^{\mu}$ over $F_{\le}$ ; and a sound and complete algorithmic formulation of $F_{\le}^{\mu}$ . We study two variants of $F_{\le}^{\mu}$ . The first one uses an extension of the $\textrm{kernel}~F_{\le}$ (a well-known decidable variant of $F_{\le}$ ). This extension accepts equivalent rather than equal bounds and is shown to preserve decidable subtyping. The second variant employs the $\textrm{full}~F_{\le}$ rule for bounded quantification and has undecidable subtyping. Moreover, we also study an extension of the kernel version of $F_{\le}^{\mu}$ , called $F_{\le\ge}^{\mu\wedge}$ , with a form of intersection types and lower bounded quantification . All the properties from the kernel version of $F_{\le}^{\mu}$ are preserved in $F_{\le\ge}^{\mu\wedge}$ . All the results in this paper have been formalized in the Coq theorem prover.

Many programming languages need to check whether two recursive types are in a subtyping relation. Traditionally recursive types are modelled in two different ways: equi- or iso- recursive types. While efficient algorithms for subtyping equi-recursive types are well studied for simple type systems, efficient algorithms for iso-recursive subtyping remain understudied. In this paper we present QuickSub : an efficient and simple to implement algorithm for iso-recursive subtyping. QuickSub has the same expressive power as the well-known iso-recursive Amber rules. The worst case complexity of QuickSub is O ( nm ), where m is the size of the type and n is the number of recursive binders. However, in practice, the algorithm is nearly linear with the worst case being hard to reach. Consequently, in many common cases, QuickSub can be several times faster than alternative algorithms. We validate the efficiency of QuickSub with an empirical evaluation comparing it to existing equi-recursive and iso-recursive subtyping algorithms. We prove the correctness of the algorithm and formalize a simple calculus with recursive subtyping and records. For this calculus we also show how type soundness can be proved using QuickSub . All the results have been formalized and proved in the Coq proof assistant.

Program verifiers for imperative languages such as C may be annotation-based , in which assertions and invariants are put into source files and then checked, or tactic-based, where proof scripts separate from programs are interactively developed in a proof assistant such as Coq. Annotation verifiers have been more automated and convenient, but some interactive verifiers have richer assertion languages and formal proofs of soundness. We present VST-A, an annotation verifier that uses the rich assertion language of VST, leverages the formal soundness proof of VST, but allows users to describe functional correctness proofs intuitively by inserting assertions. VST-A analyzes control flow graphs, decomposes every C function into control flow paths between assertions, and reduces program verification problems into corresponding straightline Hoare triples . Compared to existing foundational program verification tools like VST and Iris, in VST-A such decompositions and reductions can nonstructural, which makes VST-A more flexible to use. VST-A’s decomposition and reduction is defined in Coq, proved sound in Coq, and computed call-by-value in Coq. The soundness proof for reduction is totally logical, independent of the complicated semantic model (and soundness proof) of VST’s Hoare triple. Because of the rich assertion language, not all reduced proof goals can be automatically checked, but the system allows users to prove residual proof goals using the full power of the Coq proof assistant.

There are two well-known formulations of recursive types: iso-recursive and equi-recursive types. Abadi and Fiore [LICS 1996] have shown that iso- and equi-recursive types have the same expressive power. However, their encoding of equi-recursive types in terms of iso-recursive types requires explicit coercions. These coercions come with significant additional computational overhead , and complicate reasoning about the equivalence of the two formulations of recursive types. This paper proposes a generalization of iso-recursive types called full iso-recursive types. Full iso-recursive types allow encoding all programs with equi-recursive types without computational overhead. Instead of explicit term coercions, all type transformations are captured by computationally irrelevant casts, which can be erased at runtime without affecting the semantics of the program. Consequently, reasoning about the equivalence between the two approaches can be greatly simplified. We present a calculus called λ F i μ , which extends the simply typed lambda calculus (STLC) with full iso-recursive types. The λ F i μ calculus is proved to be type sound, and shown to have the same expressive power as a calculus with equi-recursive types. We also extend our results to subtyping, and show that equi-recursive subtyping can be expressed in terms of iso-recursive subtyping with cast operators.

Recursive types and bounded quantification are prominent features in many modern programming languages, such as Java, C#, Scala or TypeScript. Unfortunately, the interaction between recursive types, bounded quantification and subtyping has shown to be problematic in the past. Consequently, defining a simple foundational calculus that combines those features and has desirable properties, such as decidability , transitivity of subtyping, conservativity and a sound and complete algorithmic formulation has been a long time challenge. This paper presents an extension of kernel ‍ F ≤ , called F ≤ µ , with iso-recursive types. F ≤ is a well-known polymorphic calculus with bounded quantification. In F ≤ µ we add iso-recursive types, and correspondingly extend the subtyping relation with iso-recursive subtyping using the recently proposed nominal unfolding rules. We also add two smaller extensions to F ≤ . The first one is a generalization of the kernel ‍ F ≤ rule for bounded quantification that accepts equivalent rather than equal bounds. The second extension is the use of so-called structural folding/unfolding rules, inspired by the structural unfolding rule proposed by Abadi, Cardelli, and Viswanathan [1996]. The structural rules add expressive power to the more conventional folding/unfolding rules in the literature, and they enable additional applications. We present several results, including: type soundness; transitivity and decidability of subtyping; the conservativity of F ≤ µ over F ≤ ; and a sound and complete algorithmic formulation of F ≤ µ . Moreover, we study an extension of F ≤ µ , called F ≤≥ µ , which includes lower bounded quantification in addition to the conventional (upper) bounded quantification of F ≤ . All the results in this paper have been formalized in the Coq theorem prover.