Éric Tanter

Practical SQL engines differ in subtle ways in their handling of typing constraints and implicit type casts. These issues, usually not considered in formal accounts of SQL, directly affect the portability of queries between engines. To address this problem, we present a formal typing semantics for SQL, named TRAF , that explicitly captures both static and dynamic type behavior. The system TRAF is expressed in terms of abstract operators that provide the necessary leeway to systematically model the type and cast behavior of different SQL engines (PostgreSQL, MS SQL Server, MySQL, SQLite, and Oracle). We show that this formalism provides formal guarantees for the handling of types. We identify practical conditions under which engine instantiations satisfy type safety and type soundness. In this regard, TRAF can serve as an explicit and testable account of typing in existing engines, potentially guide their evolution, and provide a formal basis to study type-aware query optimizations and design provably-correct query translators. We also test the adequacy of the formalism by implementing TRAF in Python for these five engines and testing it with synthetic queries, SQLancer++- generated queries, and adapted Spider and Calcite benchmark queries.

Proof assistants based on dependent type theory---such as Agda, Lean, and Rocq---employ different universes to classify types, typically combining a predicative tower for computationally relevant types with a possibly impredicative universe for proof-irrelevant propositions. Several other universes with specific logical and computational principles have been explored in the literature. In general, a universe is characterized by its sort (e.g., Type, Prop, or SProp) and, in the predicative case, by its level. To improve modularity and better avoid code duplication, sort polymorphism has recently been introduced and integrated in the Rocq prover. However, we observe that, due to its unbounded formulation, sort polymorphism is currently insufficiently expressive to abstract over valid definitions with a single polymorphic schema. Indeed, to ensure soundness of a multi-sorted type theory, the interaction between different sorts must be carefully controlled, as exemplified by the forbidden elimination of irrelevant terms to produce relevant ones. As a result, generic functions that eliminate values of inductive types from one sort to another cannot be made polymorphic; dually, polymorphic records that encapsulate attributes of different sorts cannot be defined. This lack of expressiveness also breaks the possibility to infer principal types, which is highly desirable for both metatheoretical and practical reasons. To address these issues, we extend sort polymorphism with bounds that reflect the required elimination constraints on sort variables. We present the metatheory of bounded sort polymorphism, paying particular attention to the consistency of the resulting constraint graph. We implement bounded sort polymorphism in Rocq and illustrate its benefits through concrete examples. Bounded sort polymorphism with elimination constraints is a natural and general solution that effectively addresses current limitations and fosters the development of, and practical experimentation with, multi-sorted type theories.

Efficiently supporting sound gradual typing in a language with structural types is challenging. To date, the Grift compiler is the only close-to-the-metal implementation of gradual typing in this setting, exploiting coercions for runtime checks, and further extended with monotonic references for efficient access to statically-typed data structures. On the language design and semantics side, the Abstracting Gradual Typing (AGT) methodology has proven fruitful to elucidate existing designs and to innovate by deriving gradualizations of a wide variety of typing disciplines and language features. Grounded in abstract interpretation, the Curry-Howard inspired runtime semantics of AGT is based on the notion of evidence for consistent judgments that evolve during reduction, monitoring the plausibility of well-typedness. While expressive and versatile, it is unclear whether such evidence-based semantics are a viable route to realize an efficient implementation of gradual typing. In this work, we explore this question by designing, implementing, and evaluating an evidence-based compiler, called GrEv. We explain how to bridge the gap between the formal semantics and the GrEv compiler implementation, and identify novel monotonic semantics. We empirically evaluate the performance of GrEv on the Grift benchmark suite. The results show that an evidence-based compiler can be competitive with, and even faster than, a coercion-based compiler, exhibiting more stability across configurations on the static-to-dynamic spectrum. In addition to enriching the space of gradual typing compilers, this work opens a direct door to exploring efficient implementations of the many advanced gradual typing disciplines formally derived with AGT in the literature.

Certified programming, as carried out in proof assistants and dependently-typed programming languages, ensures that a software meets its requirements by supporting the definition of both specifications and proofs. However, proofs easily break with partial definitions and incremental changes because specifications are not designed to account for the intermediate incomplete states of programs. We advocate for proper support for incremental certified programming by analyzing its objectives and inherent challenges, and propose a formal framework for achieving incremental certified programming in a principled manner. The key idea is to define appropriate notions of completion refinement and completeness to capture incrementality, and to systematically produce specifications that are valid at every stage of development while preserving the intent of the original statements. We provide a prototype implementation in the Rocq Prover, called IncRease, which exploits typeclasses for automation and extensibility, and is independent of any specific mechanism used to handle incompleteness. We illustrate its use with both an incremental textbook formalization of the simply-typed λ-calculus, and a more complex case study of incremental certified programming for an existing dead-code elimination optimization pass of the CompCert project. We show that the approach is compatible with randomized property-based testing as provided by QuickChick. Finally we study how to combine incremental certified programming with deductive synthesis, using a novel incrementality-friendly adaptation of the Fiat library. This work provides theoretical and practical foundations towards systematic support for incremental certified programming, highlighting challenges and perspectives for future developments.

Gradual typing has long been advocated as a means to bridge the gap between static and dynamic typing disciplines, enabling a range of use cases such as the gradual migration of existing dynamically typed code to more statically typed code, as well as making advanced static typing disciplines more accessible. To assess whether a given gradual language can effectively support these use cases, several formal properties have been proposed, most notably the refined criteria set forth by Siek et al. One criterion asserts that the dynamic extreme of the spectrum should be expressible in the gradual language, formalized by the existence of an adequate embedding from the corresponding dynamic language. We observe that the existing dynamic embedding criterion does not capture the desirable property of being able to ascribe embedded code to a static type that it semantically satisfies, and ensure reliable interactions with other components within the gradual language. Specifically, we introduce the notion of robustness for gradual terms, meaning that when interacting with any gradual context, runtime failures that may occur ought to be caused by the context, not by the robust term itself. We then formulate the robust dynamic embedding criterion: if a dynamic component semantically satisfies a given static type, then its embedding subsequently ascribed to that static type should be a robust term. We demonstrate that robust dynamic embedding is not implied by any existing metatheoretical property from the literature, and is not upheld by various existing gradual languages. We show that robust dynamic embedding is achievable with a gradualized simply-typed language. All the results are formalized in the Rocq proof assistant. This novel criterion complements the set of criteria for gradual languages and opens several venues for further exploration, in particular for typing disciplines that enforce rich semantic properties.

Proof assistants based on dependent type theory, such as Coq, Lean and Agda, use different universes to classify types, typically combining a predicative hierarchy of universes for computationally-relevant types, and an impredicative universe of proof-irrelevant propositions. In general, a universe is characterized by its sort, such as Type or Prop, and its level, in the case of a predicative sort. Recent research has also highlighted the potential of introducing more sorts in the type theory of the proof assistant as a structuring means to address the coexistence of different logical or computational principles, such as univalence, exceptions, or definitional proof irrelevance. This diversity raises concrete and subtle issues from both theoretical and practical perspectives. In particular, in order to avoid duplicating definitions to inhabit all (combinations of) universes, some sort of polymorphism is needed. Universe level polymorphism is well-known and effective to deal with hierarchies, but the handling of polymorphism between sorts is currently ad hoc and limited in all major proof assistants, hampering reuse and extensibility. This work develops sort polymorphism and its metatheory, studying in particular monomorphization, large elimination, and parametricity. We implement sort polymorphism in Coq and present examples from a new sort-polymorphic prelude of basic definitions and automation. Sort polymorphism is a natural solution that effectively addresses the limitations of current approaches and prepares the ground for future multi-sorted type theories.

Current static verification techniques such as separation logic support a wide range of programs. However, such techniques only support complete and detailed specifications, which places an undue burden on users. To solve this problem, prior work proposed gradual verification, which handles complete, partial, or missing specifications by soundly combining static and dynamic checking. Gradual verification has also been extended to programs that manipulate recursive, mutable data structures on the heap. Unfortunately, this extension does not reward users with decreased dynamic checking as more specifications are written and more static guarantees are made. In fact, all properties are checked dynamically regardless of any static guarantees. Additionally, no full-fledged implementation of gradual verification exists so far, which prevents studying its performance and applicability in practice. We present Gradual C0, the first practicable gradual verifier for recursive heap data structures, which targets C0, a safe subset of C designed for education. Static verifiers supporting separation logic or implicit dynamic frames use symbolic execution for reasoning; so Gradual C0, which extends one such verifier, adopts symbolic execution at its core instead of the weakest liberal precondition approach used in prior work. Our approach addresses technical challenges related to symbolic execution with imprecise specifications, heap ownership, and branching in both program statements and specification formulas. We also deal with challenges related to minimizing insertion of dynamic checks and extensibility to other programming languages beyond C0. Finally, we provide the first empirical performance evaluation of a gradual verifier, and found that on average, Gradual C0 decreases run-time overhead between 7.1 and 40.2% compared to the fully dynamic approach used in prior work (for context, the worst cases for the approach by Wise et al. [ 2020 ] range from 0.1 to 4.5 seconds depending on the benchmark). Further, the worst-case scenarios for performance are predictable and avoidable. This work paves the way towards evaluating gradual verification at scale.

Indexed inductive types are essential in dependently-typed programming languages, enabling precise and expressive specifications of data structures and properties. Recognizing that programming and proving with dependent types could benefit from the smooth integration of static and dynamic checking that gradual typing offers, recent efforts have studied gradual dependent types. Gradualizing indexed inductive types however remains mostly unexplored: the standard encodings of indexed inductive types in intensional type theory, e.g., using type-level fixpoints or subset types, break in the presence of gradual features; and previous work on gradual dependent types focus on very specific instances of indexed inductive types. This paper contributes a general framework, named P unk , specifically designed for exploring the design space of gradual indexed inductive types. P unk is a versatile framework, enabling the exploration of the space between eager and lazy cast reduction semantics that arise from the interaction between casts and the inductive eliminator, allowing them to coexist and interoperate in a single system. Our work provides significant insights into the intersection of dependent types and gradual typing, by proposing a criteria for well-behaved gradual indexed inductive types, systematically addressing the outlined challenges of integrating these types. The contributions of this paper are a step forward in the quest for making gradual theorem proving and gradual dependently-typed programming a reality.