arXiv subjects

Sophia Roshal

Publications and source records attributed to Sophia Roshal.

3 recordsLinked to original sources

arXiv2026

Ordered Adjoint Logic

Ordered logics and type systems have been used in a variety of applications including computational linguistics, memory allocation, stream processing, logical frameworks, parametricity, and enforcing security protocols. In most formulations, ordered types are also linear, requiring each resource to be used exactly once. Prior work by Kanovich et al. has investigated calculi that relax this constraint through subexponentials within a linear ordered logic. We generalize their work by using adjoint modalities to combine logics with varying fine-grained structural properties, including weakening, left contraction, right contraction, left mobility, and right mobility. We show that the resulting sequent calculus admits cut elimination. We further provide a natural deduction formulation in which structural rules are implicit, and show that proof checking for this system is decidable. This makes it a suitable foundation for an expressive adjoint programming language or logical framework.

cs.LO↗

arXiv2025

Semantically Separating Nominal Wyvern for Usability and Decidability

The Dependent Object Types (DOT) calculus incorporates concepts from functional languages (e.g. modules) with traditional object-oriented features (e.g. objects, subtyping) to achieve greater expressivity (e.g. F-bounded polymorphism). However, this merger of paradigms comes at the cost of subtype decidability. Recent work on bringing decidability to DOT has either sacrificed expressiveness or ease of use. The unrestricted construction of recursive types and type bounds has made subtype decidability a much harder problem than in traditional object-oriented programming. Recognizing this, our paper introduces Nominal Wyvern, a DOT-like dependent type system that takes an alternative approach: instead of having a uniform structural syntax like DOT, Nominal Wyvern is designed around a "semantic separation" between the nominal declaration of recursive types on the one hand, and the structural refinement of those types when they are used on the other. This design naturally guides the user to avoid writing undecidably recursive structural types. From a technical standpoint, this separation also makes guaranteeing decidability possible by allowing for an intuitive adaptation of material/shape separation, a technique for achieving subtype decidability by separating types responsible for subtyping constraints from types that represent concrete data. The result is a type system with syntax and structure familiar to OOP users that achieves decidability without compromising the expressiveness of F-bounded polymorphism and module systems as they are used in practice.

cs.PL↗

arXiv2024

Adjoint Natural Deduction (Extended Version)

Adjoint logic is a general approach to combining multiple logics with different structural properties, including linear, affine, strict, and (ordinary) intuitionistic logics, where each proposition has an intrinsic mode of truth. It has been defined in the form of a sequent calculus because the central concept of independence is most clearly understood in this form, and because it permits a proof of cut elimination following standard techniques. In this paper we present a natural deduction formulation of adjoint logic and show how it is related to the sequent calculus. As a consequence, every provable proposition has a verification (sometimes called a long normal form). We also give a computational interpretation of adjoint logic in the form of a functional language and prove properties of computations that derive from the structure of modes, including freedom from garbage (for modes without weakening and contraction), strictness (for modes disallowing weakening), and erasure (based on a preorder between modes). Finally, we present a surprisingly subtle algorithm for type checking.

cs.LO↗