arXiv subjects

Matías Toro

Publications and source records attributed to Matías Toro.

6 recordsLinked to original sources

arXiv2026

A Gradual Probabilistic Lambda Calculus

Probabilistic programming languages have recently gained a lot of attention, in particular due to their applications in domains such as machine learning and differential privacy. To establish invariants of interest, many such languages include some form of static checking in the form of type systems. However, adopting such a type discipline can be cumbersome or overly conservative. Gradual typing addresses this problem by supporting a smooth transition between static and dynamic checking, and has been successfully applied for languages with different constructs and type abstractions. Nevertheless, its benefits have never been explored in the context of probabilistic languages. In this work, we present and formalize GPLC, a gradual source probabilistic lambda calculus. GPLC includes a binary probabilistic choice operator and allows programmers to gradually introduce/remove static type -- and probability -- annotations. The static semantics of GPLC heavily relies on the notion of probabilistic couplings, as required for defining several relations, such as consistency, precision, and consistent transitivity. The dynamic semantics of GPLC is given via elaboration to the target language TPLC, which features a distribution-based semantics interpreting programs as probability distributions over final values. Regarding the language metatheory, we establish that TPLC -- and therefore also GPLC -- is type safe and satisfies two of the so-called refined criteria for gradual languages, namely, that it is a conservative extension of a fully static variant and that it satisfies the gradual guarantee, behaving smoothly with respect to type precision.

cs.PL↗

arXiv2025

Compiling Gradual Types with Evidence

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.

cs.PL↗

arXiv2024

Reducing Urban Speed Limits Decreases Work-Related Traffic Injury Severity: Evidence from Santiago, Chile

Work-related transportation incidents significantly impact urban mobility and productivity. These incidents include traffic crashes, collisions between vehicles, and falls that occurred during commuting or work-related transportation (e.g., falling while getting off a bus during the morning commute or while riding a bicycle for work). This study analyzes a decade of work-related transportation incident data (2012--2021) in Santiago, Chile, using records from a major worker's insurance company. Using negative binomial regression, we assess the impact of a 2018 urban speed limit reduction law on incident injury severity. We also explore broader temporal, spatial, and demographic patterns in these incidents in urban and rural areas. The urban speed limit reduction is associated with a decrease of 4.26 days in prescribed medical leave for incidents in urban areas, suggesting that lower speed limits contribute to reduced injury severity. Our broader analysis reveals distinct incident patterns across different groups. Workers traveling by motorcycle and bicycle experience more severe injuries when involved in traffic incidents, with marginal effects of 26.94 and 13.06 additional days of medical leave, respectively, compared to motorized vehicles. Women workers tend to have less severe injuries, with an average of 7.57 fewer days of medical leave. Age is also a significant factor, with older workers experiencing more severe injuries -- each additional year of age is associated with 0.57 more days of medical leave. Our results provide insights for urban planning, transportation policy, and workplace safety initiatives.

cs.CY↗

arXiv2023

Gradual Sensitivity Typing

Reasoning about the sensitivity of functions with respect to their inputs has interesting applications in various areas, such as differential privacy. In order to check and enforce sensitivity, several approaches have been developed, notably sensitivity type systems. In these systems, sensitivity can be seen as an effect in the sense of type-and-effects systems as originally proposed by Gifford and Lucassen. Because type-and-effect systems can make certain useful programming patterns tedious or overly conservative, there is value in bringing the benefits of gradual typing to these disciplines in order to ease their adoption. In this work, we motivate, formalize, and prototype gradual sensitivity typing. The language GSoul supports both the unrestricted unknown sensitivity and bounded imprecision in the form of intervals. Gradual sensitivity typing allows programmers to smoothly evolve typed programs without any static sensitivity information towards hardened programs with a mix of static and dynamic sensitivity checking. In particular, we show that gradual sensitivity supports recursive functions for which fully static checking would be overly conservative, seamlessly enabling exact runtime sensitivity checks. GSoul satisfies both the gradual guarantees and sensitivity type soundness, known as metric preservation. We establish that, in general, gradual metric preservation is termination insensitive, and that one can achieve termination-sensitive gradual metric preservation by hardening specifications to bounded imprecision. We implement a prototype that provides an interactive test bed for gradual sensitivity typing. This work opens the door to gradualizing other typing disciplines that rely on function sensitivity such as differential privacy, as well as other quantitative type-based reasoning techniques.

cs.PL↗

arXiv2020

Contextual Linear Types for Differential Privacy

Language support for differentially-private programming is both crucial and delicate. While elaborate program logics can be very expressive, type-system based approaches using linear types tend to be more lightweight and amenable to automatic checking and inference, and in particular in the presence of higher-order programming. Since the seminal design of Fuzz, which is restricted to $\epsilon$-differential privacy in its original design, significant progress has been made to support more advancedvariants of differential privacy, like($\epsilon$,$\delta$)-differential privacy. However, supporting these advanced privacy variants while also supporting higher-order programming in full has proven to be challenging. We present Jazz, a language and type system which uses linear types and latent contextual effects to support both advanced variants of differential privacy and higher-order programming. Latent contextual effects allow delaying the payment of effects for connectives such as products, sums and functions, yielding advantages in terms of precision of the analysis and annotation burden upon elimination, as well as modularity. We formalize the core of Jazz, prove it sound for privacy via a logical relation for metric preservation, and illustrate its expressive power through a number of case studies drawn from the recent differential privacy literature.

cs.PL↗

arXiv2020

Gradual System F

Bringing the benefits of gradual typing to a language with parametric polymorphism like System F, while preserving relational parametricity, has proven extremely challenging: first attempts were formulated a decade ago, and several designs have been recently proposed, with varying syntax, behavior, and properties. Starting from a detailed review of the challenges and tensions that affect the design of gradual parametric languages, this work presents an extensive account of the semantics and metatheory of GSF, a gradual counterpart of System F. In doing so, we also report on the extent to which the Abstracting Gradual Typing methodology can help us derive such a language. Among gradual parametric languages that follow the syntax of System F, GSF achieves a unique combination of properties. We clearly establish the benefits and limitations of the language, and discuss several extensions of GSF towards a practical programming language.

cs.PL↗