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.
Ronald Garcia
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.
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.