Exception handlers—and effect handlers more generally—are language mechanisms for structured nonlocal control flow. A recent trend in language-design research has introduced lexically scoped handlers, which address a modularity problem with dynamic scoping. While dynamically scoped handlers allows zero-overhead implementations when no effects are raised, existing implementations of lexically scoped handlers require programs to pay a cost just for having handlers in the lexical context. In this talk, we present a novel implementation strategy for lexically scoped handlers that satisfies the zero-cost principle—a property otherwise met by most modern compilers supporting dynamically scoped exceptions handlers. The key idea is a type-directed compilation that emits information indicating how handlers come into the lexical scope. This information guides the runtime in walking the stack to locate the right handler. The compilation scheme does not require any reified, lexically scoped representation of handlers when no effects are raised. We capture the essential aspects of this compilation scheme using core calculi. We prove the correctness of the compilation scheme by showing that it preserves semantics. Empirical results suggest that the implementation strategy is effective.

Rust is a popular systems language that offers low-level control like C/C++ and uses ownership semantics to track aliasing and mutation of data. In Rust, (1) a value has exactly one owner, (2) a reference to a value (called a borrow) cannot outlive the owner, and (3) a value can have either one mutable reference or multiple immutable references, but not both simultaneously. A program that adheres to this discipline enables the Rust compiler to reason about memory and thread safety properties statically. A successfully compiled program is therefore guaranteed to be safe to execute with respect to these properties.

However, since target architectures do not support ownership natively, this information is lost during the translation from high-level Rust to its low-level representation (e.g., LLVM-IR). We have developed semantics for representing ownership in an LLVM-IR like language called OSEA-IR. In this talk we will discuss SEAURCHIN—a compilation pipeline from Rust to OSEA-IR. We then explore how leveraging ownership-aware IRs like OSEA-IR can facilitate compiler optimization, testing and verification.

SQL with Paths (SQLP) is an extension of the standard SQL query language designed to work with the Abstract Relational Model (ARM), which includes entities and abstract identifiers. A key feature of SQLP is the use of attribute paths, such as x.f1.f2, to compactly express sequences of unary foreign key joins, simplifying navigation across related data. This approach aims to hide the complexities of explicit primary and foreign keys from users, offering a more conceptual querying experience. Notably, SQLP queries can be rewritten into equivalent standard SQL queries for execution on relational database systems, ensuring compatibility with existing relational database technologies.

Development in the field of Algebraic Effects and Handlers is always exciting, getting us closer to a modular effect management system. On the other hand, a question language designers often have to ask is "How does the new feature fit into the larger landscape?" We start with developments on the effect typing of parallel effect, with the aim of incorporating it into a Eff-lang-like setting. The design of parallel effects (And other Higher-order effects) demands higher-order types, a feature not yet present in Eff-lang. We will examine the effect subtyping system in previous works and understand the "skeleton" mechanism used to enable effect erasure. Finally, we will discuss our attempt at enriching the system with kinds.

Notions of derivative abound in functional programming. An obvious question arises: what about integrals? It turns out that folds are the analogous concept. Pursuing the analogy leads us to a proper notion of "definite fold" corresponding to definite integrals (and sums and products and ...). Many concepts are needed along the way (Route, Pointed type, etc). In return, incremental and parallel versions of fold arise naturally. The correct notion of indefinite fold is a little more elusive, making a "Fundamental Theorem of Fold-Calculus" delicate.

Certified compilers are complex software systems. Like other large systems, they demand modular, extensible designs. While there has been progress in extensible metatheory mechanization, scaling extensibility and reuse to meet the demands of full compiler verification remains a major challenge. We respond to this challenge by introducing novel expressive power to a proof language. Our language design equips the Rocq prover with an extensibility mechanism inspired by the object-oriented ideas of late binding, mixin composition, and family polymorphism. We implement our design as a plugin for Rocq, called Rocqet. We identify strategies for using Rocqet's new expressive power to modularize the monolithic design of large certified developments as complex as the CompCert compiler. The payoff is a high degree of modularity and reuse in the formalization of intermediate languages, ISAs, compiler transformations, and compiler extensions, with the ability to compose these reusable components—certified compilers à la carte. We report significantly improved proof-compilation performance compared to earlier work on extensible metatheory mechanization. We also report good performance of the extracted compiler.

Unordered SQL is a relaxation of SQL syntax, created by allowing the clauses of a SELECT statement to be in any order, instead of the standard SELECT-FROM-WHERE format. The key concept is that valid SQL should be valid Unordered SQL, and Unordered SQL has a direct and intuitive translation to SQL. We explore 2 variants of this language, which vary in their level of "allowed unorderedness," and discuss the benefits and drawbacks of each. Finally, we discuss different approaches for IDE support, including considerations for providing error diagnostics and supporting different SQL variants. [[ work in progress. previous work can be found at https://github.com/SaltOverflow/unordered-sql ]]

SuperOOP (Fan and Parreaux, 2023) provides a novel approach to extensible Object-Oriented Programming using the notion of mixins. Mixins are reusable code components that provide partial implementations of methods, and methods can be fused together by a composition of mixins. In industry-level programming languages such as Scala, traits provide a good abstraction as reusable code components by having explicit type signatures for methods. In this talk, I will propose a combination of traits and SuperOOP-style modular programming to bring the best of both worlds together: a programming model with explicit types and method signatures in traits and SuperOOP-style modular programming. The key to this approach is to have extensible type definitions inside traits, which can be extended with new data type variants. Developers can refer to locally defined variants or all possible variants that may be introduced in the future.

Large Language Models (LLMs) are increasingly adept at handling diverse tasks through well-crafted prompts. Moving beyond single-prompt approaches, workflows like Tree-of-Thoughts (ToT) employ LLMs as modular components to tackle more complex problems. This shift underscores the need for seamless integration between LLMs and traditional programming. To address this, we introduce APPL, A Prompt Programming Language, designed as a bridge between programs and LLMs. Retaining Python's syntax, APPL enables seamlessly integrating Python objects and control flows, natural language prompts, and LLM calls within a single cohesive function. Besides, LLM calls in APPL are asynchronously computed, enabling natural parallelization to improve resource utilization and accelerate workflows. Additionally, APPL includes a tracing module for better observability and easier diagnosing. We demonstrate how APPL simplifies implementing advanced methods like Chain-of-Thought with self-consistency (CoT-SC), ReAct tool-using agents, and virtual tool emulation. For more details, please visit https://appl-team.github.io/appl/.

A common practice in programming is aliasing constants, e.g., const one = 1, Pi = 3.14159, noon = 12. An alias may bind to another alias, transitively binding it to a constant, and aliases can represent the same value, giving synonyms. Programming languages capture this capability through constant naming. The goal is replacing values with meaningful names, increasing readability, and preventing errors when changing the binding, as the new value is automatically distribute throughout the program. Constants can be grouped into a (ordered) set, e.g., days of a week, where values are chosen implicitly or explicitly to support set operations. Programming languages capture this mathematical notion through an enumeration type, where instantiations take on the set values, and control flow provides enumerating through the set. This talk examines two aspects of enumerations. 1. An Algebraic Data Type is not an enumeration, and attempting to repurposing it for enumeration is contrived and confusing. 2. C enumerations are simple and unsafe, but can be extended into a complex and safe enumeration type, while maintaining backwards compatibility. Examples are shown in the new Cforall programming language, which are comparable to enumerations in other advanced languages.

Deep Learning compilers need to compile programs with multi-gigabyte constants. These constants come from model parameters and their activations. Traditional eager constant-propagation is a bad fit in this scenario because the constants are large, and so their evaluation is time consuming, slowing down the compiler. We present an alternative approach based on symbolic constant propagation. Instead of eagerly propagating constants during compilation, constants are symbolically evaluated as graphs of expressions. These constant graphs can then be optimized and reused as needed. Once compilation is complete, constant graphs are evaluated with input values and the results backpatched into the emitted assembly. This technique offers benefits for compilation performance and debuggability.