Ronald Garcia

Associate Professor
Software Practices Lab
Department of Computer Science
University of British Columbia
201-2366 Main Mall
Vancouver, B.C., Canada V6T 1Z4


Research Interests
Refereed Publications
Technical Reports

Research Interests

I am interested in many aspects of programming language semantics, design, and implementation, including language support for library-centric and modular software development, generic and generative programming, and domain specific languages and libraries.


Spring 2024: Programming Language Principles (
CPSC 509)
Fall 2023: Definition of Programming Languages (CPSC 311)
Spring 2022: Programming Language Principles (CPSC 509)
Fall 2021: Definition of Programming Languages (CPSC 311)
Spring 2021: Systematic Program Design (CPSC 107)
Fall 2020: Definition of Programming Languages (CPSC 311)
Spring 2020: Introduction to Compiler Construction (CPSC 411)
Fall 2019: Programming Language Principles (CPSC 509)
Spring 2019: Introduction to Compiler Construction (CPSC 411)
Fall 2018: Programming Language Principles (CPSC 509)
Spring 2017: Introduction to Compiler Construction (CPSC 411)
Fall 2016: Programming Language Principles (CPSC 509)
Spring 2015: Introduction to Compiler Construction (CPSC 411)
Fall 2015: Programming Language Principles (CPSC 509)
Spring 2014: Programming Language Principles (CPSC 509)
Fall 2014: Computation, Programs, and Programming (CPSC 110)
Spring 2013: Programming Language Principles (CPSC 509)
Fall 2013: Computation, Programs, and Programming (CPSC 110)
Spring 2012: Programming Language Principles (CPSC 509)
Fall 2012: Computation, Programs, and Programming (CPSC 110)
Fall 2011: Programming Language Principles (CPSC 509)


Current Students:


Recent Activities

Refereed Publications

Training Industrial End-user programmers with Interactive Tutorials [Preprint]
Nico Ritschel, Anand Ashok Sawant, David Weintrop, Reid Holmes, Alberto Bacchelli, Ronald Garcia, Chandrika K R, Avijit Mandal,
Patrick Francis, David C. Shepherd Nico Ritschel, Vladimir Kovalenko, Reid Holmes, Ronald Garcia, David C. Shepherd
Software: Practice and Experience (SPE), 53 (3), 729-747. 2023.
Can guided decomposition help end-users write larger block-based programs? a mobile robot experiment
Nico Ritschel, Felipe Fronchetti, Reid Holmes, Ronald Garcia, David C. Shepherd
Proceedings of the ACM on Programming Languages, Volume 6, Issue OOPSLA, October 2022, Article No.: 133, pp 233-258
Propositional Equality for Gradual Dependently Typed Programming [Preprint]
Joseph Eremondi, Ronald Garcia, Éric Tanter
Proceedings of the ACM on Programming Languages, Volume 6, Issue ICFP, August 2022, Article No.: 96, pp 165-193
Abstracting gradual typing moving forward: precise and space-efficient [Video]
Felipe Bañados Schwerter, Alison M. Clark, Khurram A. Jafery, Ronald Garcia
Proceedings of the ACM on Programming Languages, Volume 5, Issue POPL, January 2021, Article No.: 61, pp 1-28
Comparing Block-based Programming Models for Two-armed Robots. [Preprint] [Supplementary Data]
Nico Ritschel, Vladimir Kovalenko, Reid Holmes, Ronald Garcia, David C. Shepherd
IEEE Transactions on Software Engineering (TSE), 48 (5), 1630-1643. 2020.
Gradual Typing as if Types Mattered
Ronald Garcia, Éric Tanter
WGT '20: The First ACM SIGPLAN Workshop on Gradual Typing.
ACM DL Author-ize service Approximate Normalization for Gradual Dependent Types [Video]
Joseph Eremondi, Ronald Garcia, Éric Tanter
Proceedings of the ACM on Programming Languages, Volume 3, Issue ICFP, July 2019, Article No.: 88, pp 1-30
Novice-friendly Multi-armed Robotics Programming
Nico Ritschel, Reid Holmes, Ronald Garcia, David C. Shepherd
RoSE '19: Proceedings of the 2nd International Workshop on Robotics Software Engineering, May 2019, pp 29-32
Refining Semantics for Multi-Stage Programming
Rui Ge, Ronald Garcia.
Journal of Computer Languages. 51 (1), 222-240. April 2019.
ACM DL Author-ize serviceType-Driven Gradual Security with References
[Tech Report]
[POPL 2019 Talk]
Matías Toro, Ronald Garcia, Éric Tanter
ACM Transactions on Programming Languages and Systems (TOPLAS), 40 (4), 1-55. 2018
Gradual typing is typically understood as a way to incrementally transform untyped programs to statically-typed ones. But this perspective is too limiting: all programming languages are to some extent untyped, in the sense that many desirable program properties cannot be expressed in, or enforced by, their type systems.

This paper interrogates this phenomenon in the context of type systems for information-flow security. It develops a gradually-typed language where the "dynamic" language is untyped with respect to security properties, and the "static" language uses types to express and enforce information-flow security properties. The main technical innovation of this paper over prior gradual security languages is a notion of gradual security typing that is driven solely by the type structure of programs: all reasoning about information-flow security comes from the type system, even though the language mixes static and dynamic enforcement. A programmer can read type signatures and ascriptions as security guarantees and predict security behaviour without consulting the code itself.

The key conceptual observation of this paper is that sophisticated typing guarantees more more of the gradual type system than syntactic type safety. To achieve type-driven gradual security typing, the paper develops a semantic typing judgment that directly characterizes the security properties that each type can ascribe to code fragments, and proves that the syntactic typing judgment is sound with respect to it.

ACM DL Author-ize serviceRefining semantics for multi-stage programming
[GPCE Talk]
Rui Ge, Ronald Garcia
GPCE 2017 Proceedings of the 16th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, 2017
Multi-stage programming enhances a programming language with principled support for constructing and evaluating code at run-time. A variety of semantices for multi-stage languages appear in the literature, each suited to varied forms of reasoning, including interpretation, compilation, and translation. This paper develops and proves correct the first environment-passing abstract machine for arbitrary homogeneous multi-stage programming. This style of semantics is particularly well-suited to the development of abstract interpretation-based static analyses [Van Horn and Might 2011].
Gradual Type-and-Effect Systems
Felipe Bañados Schwerter, Ronald Garcia, and Éric Tanter.
Journal of Functional Programming, Volume 26. January, 2016
Type-and-effect systems provide stronger reasoning principles than classic type systems, especially when the programming language in question supports effectful computation. But there is no free lunch: in exchange for stronger guarantees, they demand more annotations and careful structuring of your programs. Gradual type-and-effect systems provide a smooth transition from dynamic languages to statically typed languages and on to a static type-and-effect discipline. The programmer can decide which parts of a program are checked statically and which parts are checked dynamically, treating effects and types mostly independently.
ACM DL Author-ize serviceAbstracting gradual typing
[Typo Fixes February 1, 2016][POPL Talk] [ERRATUM! July 20, 2018]
Ronald Garcia, Alison M. Clark, Éric Tanter
POPL '16 Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016
As gradual typing is applied to more and more sophisticated languages, language designers find that it becomes more difficult to figure out how to seamlessly blend dynamic checking with static checking. This paper presents a new approach to designing a gradual type system in terms of a pre-existing static type system. Building on our 2014 ICFP paper, we show how to use abstract interpretation to give gradual types a semantics in terms of static types, and from there use the underlying static type discipline to derive a corresponding gradual type system and operational semantics.
ACM DL Author-ize serviceEssential retroactive weaving
Robin Salkeld, Ronald Garcia
MODULARITY Companion 2015 Companion Proceedings of the 14th International Conference on Modularity, 2015
Advances in record and replay technology for programs has enabled the development of powerful debugging tools, as well as more information for post-mortem analysis of faults that happened in the field. However using these technologies is not as simple as printf debugging. Retroactive weaving proposes to reuse the aspect-oriented parts of a programming language as a programmatic interface to these traces. In essence, an aspect is weaved into the trace of a program that has already been executed. These ideas were previously studied in C and Java, but the core ideas are hidden within a large code base. This paper introduces a definitional interpreter for an aspect-oriented functional programming language, extends the interpreter to support retroactive weaving, demonstrates the technique's potential, and frames the core technical and formal challenges involved.
Monotonic References for Efficient Gradual Typing.
Jeremy Siek, Michael M. Vitousek, Matteo Cimini, Sam Tobin-Hochstadt, and Ronald Garcia. In ESOP '15: European Symposium on Programming. April 2015.
Gradually typed languages have made compromises in their support for mutable references. Some designs provide limited or no support gradually-typed references; other designs impose runtime overhead on all reads and writes to references, even code that is precisely typed. In addition, gradual references signal runtime errors when distinct client expressions use them inconsistently; no designs provide support for identifying those culprit expressions. This paper presents the design of a gradually typed language with full support for gradual references. Statically typed references require no runtime overhead for reads or writes: the gradual references "pay their own way". The language includes a blame-tracking strategy that identifies the parties that are responsible for runtime gradual reference errors.
								  servicePrincipal Type Schemes for Gradual Programs
[Typo Fixes May 16, 2017]
Ronald Garcia, Matteo Cimini
POPL '15 Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015
For gradual typing to have impact on modern functional programming languages, it must be coexist with implicit typing, which is checked using type inference. This paper builds on prior work on gradual typing with type inference. It develops a new foundation for gradual implicit typing, a type inference algorithm that straightforwardly extends the algorithm for traditional type inference, and uncovers a fundamental distinction between gradual and static parametric polymorphism.
ACM DL Author-ize serviceFoundations of Typestate-Oriented Programming
Ronald Garcia, Éric Tanter, Roger Wolff, Jonathan Aldrich
ACM Transactions on Programming Languages and Systems (TOPLAS), 2014
Typestate extends the concept of types to account for state changes of program objects as computation progresses. Traditionally typestates have been presented as extended static checkers for programming languages with pre-existing type systems. This paper introduces and formalizes a language whose structural type system internalizes the notion of typestate. We present a Featherweight Typestate, a typestate-oriented programming language, as well as its gradually-typed counterpart, which introduces flexibility as needed to the typestate approach. This paper builds on the results from our ECOOP '11 paper.
ACM DL Author-ize serviceConfined Gradual Typing
Esteban Allende, Johan Fabry, Ronald Garcia, Éric Tanter
OOPSLA '14 Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, 2014
Adding gradual types introduces the potential for performance-sapping and reliability-compromising function wrappers to be implicitly introduced at unforeseen places in user code. This paper presents a type system with simple flow annotations that allow programmer to precisely control which program values are subject to wrapping. The need for this control is validates using Gradualtalk, a Gradually typed dialect of Smalltalk.
ACM DL Author-ize serviceA Theory of Gradual Effect Systems
Felipe Bañados Schwerter, Ronald Garcia, Éric Tanter
ICFP '14 Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, 2014
Effect systems are a powerful tool for imposing effect disciplines on programming languages, but they have failed to make much headway in programming languages. We conjecture that this is in part due to their inflexibility. To support incremental adoption of checked effect disciplines, this paper presents a general framework for developing gradually checked effect systems.
The Reaction of Open-Source Projects to New Language Features: An Empirical Study of C#
Donghoon Kim, Emerson Murphy-Hill, Chris Parnin, Christian Bird, and Ronald Garcia.
Journal of Object Technology, Volume 12, no. 4 (November 2013), pp. 1:1-31.
Generics have become viewed as a crucial feature of object oriented languages, and as such have been added to both Java and C#. This paper presents an empirical study of how generics have been adopted over time in ongoing open source projects, and to what extent the available data supports or undercuts language designers' claims about their benefits.
ACM DL Author-ize serviceCalculating Threesomes, with Blame
[Tech Report]
Ronald Garcia
ICFP '13 Proceedings of the 18th ACM SIGPLAN international conference on Functional programming, 2013
The coercion calculus of Henglein is a pleasant framework in which to design space-efficient cast calculi that embody particular blame strategies, but implementing coercions directly and correctly is challenging. The threesome calculus of Siek and Wadler also supports space-efficient casts and is straightforward to implement, but is tricky to endow with a blame strategy. This paper shows that you can enjoy the best of both worlds by designing your blame strategy using coercions, and then calculate a corresponding notion of threesomes using correctness-preserving transformations. The concrete result is three new threesome calculi that cover the design space of casts identified by Siek, Garcia, and Wadler.
Gradual Typestate
Roger Wolff, Ronald Garcia, Éric Tanter, and Jonathan Aldrich.
In ECOOP '11: The 25th European Conference on Object-Oriented Programming.
This paper presents Gradual Featherweight Typestate (GFT), a formal model of a language for Typestate-oriented programming. Though powerful, static typestate checkers, like the one built into GFT, are sometimes too weak to recognize correct programs, and sometimes too complex for programmers to use. This work averts this limitation by developing a model of combined static and dynamic typestate checking. The result is a language that provides powerful static safety and program structuring facilities with tractable and flexible type checking.
ACM DL Author-ize servicePermission-based programming languages (NIER track)
Jonathan Aldrich, Ronald Garcia, Mark Hahnenberg, Manuel Mohr, Karl Naden, Darpan Saini, Sven Stork, Joshua Sunshine, √Čric Tanter, Roger Wolff
ICSE '11 Proceedings of the 33rd International Conference on Software Engineering, 2011
This paper proposes access permissions as a powerful extension to programming language type systems. They can be used to support stronger safety checks, more flexible program structure, and safe concurrency.
Lazy Evaluation and Delimited Control
Ronald Garcia, Andrew Lumsdaine, and Amr Sabry.
In Logical Methods in Computer Science, Volume 6, Issue 3: Special Issue on POPL 2009.
This journal paper extends the results of the 2009 POPL paper with more language features and an abstract machine for cyclic call-by-need evaluation.
ACM DL Author-ize serviceToward foundations for type-reflective metaprogramming
Ronald Garcia, Andrew Lumsdaine
GPCE '09 Proceedings of the eighth international conference on Generative programming and component engineering, 2009
C++ template metaprogramming is a suite of techniques for compile-time computation that leverage the expressive power of C++'s type system. Because it relies on emergent properties of language features that were originally intended for other purposes, template metaprogramming suffers practical shortcomings and is not well-understood in theory. In this paper, we analyze core capabilities of template metaprogramming apart from the particular C++ features that support them. Guided by this analysis we develop and study a foundational language semantics that directly captures those capabilities.
Exploring the Design Space of Casts
Jeremy Siek, Ronald Garcia, and Walid Taha. In ESOP '09: The 18th European Symposium on Programming.
Variants of the lambda calculus augmented with a dynamic type and cast expressions (cast calculi) have been used to formalize languages that combine dynamic and static type disciplines. Due to the diversity of requirements imposed by these languages, no single cast calculus design suffices. In this paper, we develop a modular semantic framework that captures a number of cast calculi, some novel and some extending or matching results from the literature. Each calculus supports space-efficient implementation and tracks blame for cast failures. Furthermore, we introduce a novel and intuitive blame-assignment strategy that respects traditional subtyping.
ACM DL Author-ize serviceLazy evaluation and delimited control
Ronald Garcia, Andrew Lumsdaine, Amr Sabry
POPL '09 Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 2009
This paper formalizes the connection between lazy evaluation and coroutine-like control operations, both of which are often used to solve the same problems. Starting from a variant of the call-by-need lambda calculus, we produce a novel heap-less abstract machine that uses control operations to locally manage laziness. We then recast the machine's operational behavior as a simulation of call-by-need evaluation in a call-by-value language with delimited control operations and first-class generative prompts. Both semantic artifacts cast lazy evaluation as an elegant expression of control operations.
An extended comparative study of language support for generic programming
Ronald Garcia, Jaakko Järvi, Andrew Lumsdaine, Jeremy Siek, and Jeremiah Willcock. In Journal of Functional Programming, Volume 17, Number 2, 2007.
This paper extends the work presented in the OOPSLA 2003 paper. It adds explorations of the generic programming style using the class system of Objective Caml and the symmetric multi-methods of Cecil. The analysis of the previously studied languages has been updated to reflect changes since 2003, some of which were inspired by that work.

Type classes without types
Ronald Garcia and Andrew Lumsdaine. In Scheme '05: the 2005 ACM SIGPLAN Workshop on Scheme and Functional Programming.

Haskell type classes are an interesting example of how static type information can be used to enhance the expressiveness of a programming language. Scheme macros are a powerful mechanism for developing syntactic abstractions. This paper explores how far macros can go toward extending a dynamically typed language with a feature normally associated with static typing.

MultiArray: a C++ library for generic programming with arrays
Ronald Garcia and Andrew Lumsdaine. In Software: Practice and Experience, Volume 35, Number 2, 2005.

This paper reports on the design and implementation of MultiArray, a library for multi-dimensional array programming. This library is based on the generic programming style popularized by the Standard Template Library. It provides array containers, adaptors, and views, all built on a consistent conceptual basis.
ACM DL Author-ize serviceA comparative study of language support for generic programming
Ronald Garcia, Jaakko Jarvi, Andrew Lumsdaine, Jeremy G. Siek, Jeremiah Willcock
OOPSLA '03 Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, 2003
Both research and mainstream programming languages now provide mechanisms for type-based abstraction, including templates, parametric polymorphism, and sophisticated module systems. This paper uses a case-study to explore the capabilities and shortcomings of several programming languages with respect to their ability to express libraries of generic data structures and algorithms.

Technical Reports

ACM DL Author-ize serviceInterpretations of the gradually-typed lambda calculus
Jeremy G. Siek, Ronald Garcia
Scheme '12 Proceedings of the 2012 Annual Workshop on Scheme and Functional Programming, 2012
Gradual typing combines static and dynamic checking in a single language. A substantial amount of research has appeared and explored both the static and dynamic semantics of gradual languages. This invited tutorial introduces a variety of flavours of gradual typing for a functional language by way of interpreters written in Scheme.

Nourishing the Future of the Field: The Programming Language Mentoring Workshop 2012.
Kathleen Fisher and Ronald Garcia and Stephanie Weirich. In ACM SIGPLAN Notices, Volume 47, Issue 4a, April 2012.

This activity report documents our goals, efforts, and observations about the first Programming Languages Mentoring Workshop, which was colocated with the ACM/SIGPLAN Conference on Principles of Programming Languages (POPL) 2012. This event has been colocated with POPL every year since, and in 2015 branched out to the ACM/SIGPLAN International Conference on Functional Programming (ICFP) as well as the ACM/SIGPLAN conference on Sysems Programming, Languages, and Applications: Software for Humanity (SPLASH).

Concepts for C++0x
Jeremy Siek, Douglas Gregor, Ronald Garcia, Jeremiah Willcock, Jaakko Järvi, and Andrew Lumsdaine. Technical report N1758=05-0018, ISO/IEC JTC 1, Information Technology, Subcommittee SC 22, Programming Language C++, 2005.

C++ has been a very capable language for implementing generic libraries, but provides limited explicit support for generic programming. Based on our experiences implementing C++ libraries and studying language support for the generic programming style, we designed C++ language extensions to directly support concepts, a modular constraint formalism for generics. The design has since evolved into a joint proposal with colleagues at Texas A&M, and is expected to be part of the next C++ standard (so-called C++0X).


I am an active participant in the Boost C++ Libraries project. I serve (with John Phillips) as Review Wizard, primarily responsible for coordinating review managers and library reviews.

I am the primary developer of the Boost MultiArray Library. MultiArray is a library of multi-dimensional array abstractions. MultiArray is based on generic programming. It provides a number of array types (self-managed containers, adaptors, and views) as well as a type-generic programming interface (or concept in generic programming terms) that enables the implementation of generic array algorithms.

I've contributed code to a variety of other Boost projects. For example, I implemented a flexible GraphViz parser for the Boost Graph Library. I have also provided an IOStreams codecvt facet for the Unicode UTF-8 encoding. This facet is used in several Boost libraries including the Serialization and Program Options libraries.


I am an avid fan and player of ultimate frisbee. I also like to run and ride my bike around interesting places. While not particularly fond of cooking, I'm a big fan of eating.