Ronald Garcia

 
Prospective Graduate Students / Postdocs

This faculty member is currently not looking for graduate students or Postdoctoral Fellows. Please do not contact the faculty member with any such requests.

Associate Professor

Research Classification

Research Interests

programming languages

Relevant Thesis-Based Degree Programs

 
 

Research Methodology

Mechanized Proof Assistants

Graduate Student Supervision

Doctoral Student Supervision

Dissertations completed in 2010 or later are listed below. Please note that there is a 6-12 month delay to add the latest dissertations.

A formal framework for understanding run-time checking errors in gradually typed languages (2024)

Although Abstracting Gradual Typing provides a systematic approach to design gradual languages, the original framework has limitations: first, it accepts design choices that lead to type inconsistencies sneaking through evaluation. Second, when a type inconsistency is identified at run time, evaluation halts without providing any feedback on the parts of the program related to the failure, a safe approach yet unhelpful for debugging.This dissertation addresses these two limitations of the Abstracting Gradual Typing framework. For the first limitation, I impose an extra constraint on the acceptable designs for gradual types: forward completeness of every type operation. This stricter constraint guarantees that, throughout evaluation, gradual types and runtime evidence objects cannot lose precision and will only represent information consistent with the original static type system. I introduce a new design for a gradual language with record subtyping that fulfills this restriction. For the second limitation, I provide a specification for runtime program slicing that can be systematically applied to languages designed using Abstracting Gradual Typing. Slicing can separate the portions of a program that are guaranteed to be uninvolved in a runtime failure. Unlike the standard blame approach, slicing does not assume that types are correct. The slicing semantics can be used to provide a debugging tool, and I apply empirical research methods to explore whether this runtime type slicing approach is useful to developers.

View record

Enriching block-based end-user programming with visual features (2024)

Today, most programmers are not professional software developers, but end-users with limited training and experience in programming. End-user-friendly programming languages and tools aim to support this type of user, and many use visual programming aids to do so. Block-based programming is a popular visual programming style that has been effectively used in computer science education and is the foundation for many modern end-user programming tools. Because of the popularity of block-based programming, language designers can use a rich set of existing technologies that save them the effort of creating visual programming designs from scratch. However, many language designers ignore that block-based programming was created with learners in mind, who have different needs than end-users. Especially when programs grow in size and complexity, blocks offer little support to help end-users understand and edit programs effectively. In our work, we augment block-based programming with visual features that extend the range of programs that end-users can comprehend and write. In particular, we create languages and environments for the domain of robotics programming that allow end-users to write larger and more expressive programs. We focus on three scenarios that represent challenges that end-users face in this domain: coordinating multiple robots that work in tandem, writing large programs that span several workstations in different locations, and reacting to external signals such as machines or user interactions. For each environment, we first discuss the limitations of existing work in the areas of block-based and end-user programming. We present and discuss the design of our visual extensions with the goal to maintain end-user-friendliness. Finally, we evaluate our work through empirical studies, both formative to inform our designs and summative to demonstrate their benefits. Our designs, and the empirical and analytical process that we applied to create them, both contribute to a stronger understanding of how to build end-user-centric tools. We further believe that although our work focuses on the domain of robotics, these contributions transfer to other areas of end-user programming as well.

View record

On the design of a gradual dependently typed language for programming (2023)

Dependently typed programming languages provide a way to write programs, specifications, and correctness proofs using a single language. If a dependent type checker accepts a program, the programmer can be assured that it behaves according to the specification given in its types. However, dependently typed programming languages can be hard to use.Gradual types provide a way to mix dynamically and statically typed code in a single language. Under this paradigm, programs may have imprecise types, causing certain type checks to be deferred to run time.We build the theoretical foundations for combining gradual and dependent types in a programming language, with the aim of making dependent types easier to use. The differences between these two paradigms lead to inherent tensions when choosing the properties such a language should satisfy. Gradual typing's effectful nature conflicts with the compile-time reductions of dependent type checking. Gradual run-time type comparisons clash with dependent types containing terms that bind variables. This dissertation identifies such tensions and proposes a design that finds balance between the conflicting goals.Our contribution has three parts:First, we present a foundational calculus for gradual dependent types, with functions, function types and universes. To ensure that type checking terminates, we reduce compile-time terms with approximate normalization, producing imprecise results when the available type information cannot guarantee termination. We use hereditary substitution to show that approximate normalization always terminates.Second, we present a notion of propositional equality for gradual dependent types. We devise a method of tracking run-time consistency information between imprecise equated terms, and introduce a composition operator in the language itself.Third, we show that the first and second contributions can be combined, giving a language with approximate normalization that supports inductive types and propositional equality with dynamic consistency tracking. Since hereditary substitution does not scale to inductive types, we use a syntactic model to establish termination. The same technique is used to model non-terminating run-time semantics using guarded type theory, paving the road for mechanizing the metatheory of gradual dependent types.

View record

Master's Student Supervision

Theses completed in 2010 or later are listed below. Please note that there is a 6-12 month delay to add the latest theses.

Formalizing Rust Traits (2016)

Rust is a new systems programming language designed with a focus on bare metal performance, safe concurrency and memory safety. It features a robust abstraction mechanism in the form of traits, which provide static overloading and dynamic dispatch. In this thesis, we present MiniRust—a formal model of a subset of Rust. The model focuses on the trait system and includes some advanced features of traits such as associated types and trait objects. In particular, we discuss the notion of object safety—the suitability of a particular trait for creating trait objects—and we formally determine very general conditions under which it can be guaranteed. To represent the runtime semantics of MiniRust programs, we develop an explicitly-typed internal language RustIn, for which we prove type safety, and we show that well-typed MiniRust programs can be translated to well-typed RustIn programs. Finally, we adapt the informally-described Rust trait coherence rules to our model and we show thatthey are sufficient to ensure that overloads are always well-determined, even in the presence of library extensions.

View record

Refining semantics for multi-stage programming (2016)

Multi-stage programming is a programming paradigm that supports runtime code generation and execution. Though researchers have extended several mainstream programming languages to support it, multi-stage programming has not been widely recognised or used. The popularisation of multi-stage programming has been impeded by the lack of development aids such as code refactoring and optimisation, for which the culprit is the lack of static analysis support. Van Horn and Might proposed a general-purpose approach to systematically developing static analyses for a programming language by applying transformations to its formal semantics, an approach we believe is applicable to multi-stage programming. The approach requires that the initial semantics be specified as an environmental abstract machine that records the change of control strings, environments and continuations as a program evaluates. Developing an environmental abstract machine for a multi-stage language is not straightforward and has not been done so far in the literature. In the thesis, we study multi-stage programming through a functional language, MetaML. The main research problem of the thesis is: Can we refine the pre-existing substitutional natural semantics of MetaML to a corresponding environmental abstract machine and demonstrate their equivalence?We first develop a substitutional structural operational semantics for MetaML. Then we simplify the research problem along two dimensions—each dimension leads to a less complicated semantics refinement problem. The first dimension is to refine semantics for a single-stage language rather than a multi-stage language: we stepwise develop an environmental abstract machine, the CEK machine, for a single-stage language, ISWIM, based on its substitutional structural operational semantics. The second dimension is to derive a substitutional abstract machine rather than an environmental abstract machine: we stepwise develop a substitutional abstract machine, the MK machine, for the multi-stage language MetaML, based on its substitutional structural operational semantics. Finally, utilising the experience of refining semantics along two dimensions, we stepwise develop an environmental abstract machine, the MEK machine, for MetaML, based on its substitutional structural operational semantics. Furthermore, we introduce three proof techniques which are used throughout the thesis to prove the equivalence of semantics.

View record

IR-MetaOCaml: (re)implementing MetaOCaml (2015)

Multi-stage programming is a form of metaprogramming that is anextension of ideas and techniques of partial evaluation. This thesisdiscusses a (re)implementation of a multi-stage programming systemMetaOCaml. The system presented here differs from the OCamlimplementation by Taha et al in that it is implemented on top of amodern OCaml compiler. It differs from BER MetaOCaml in that itsupports generation of native code in a turn-key fashion. It differsfrom both systems in that it uses the OCaml intermediate representationto represent the notion of code (to the best of my knowledge, existingsystem use abstract syntax trees instead.)

View record

 
 

If this is your researcher profile you can log in to the Faculty & Staff portal to update your details and provide recruitment preferences.

 
 

Follow these steps to apply to UBC Graduate School!