Ronald Garcia
Associate ProfessorSoftware Practices Lab
Department of Computer Science
University of British Columbia
201-2366 Main Mall
Vancouver, B.C., Canada V6T 1Z4
rxg+xoxo@cs.ubc.ca
Vita
|
|
Ronald GarciaAssociate ProfessorSoftware Practices Lab Department of Computer Science University of British Columbia 201-2366 Main Mall Vancouver, B.C., Canada V6T 1Z4 rxg+xoxo@cs.ubc.ca Vita |
Alumni:
Can guided decomposition help end-users write larger block-based programs? a mobile robot experiment
Propositional Equality for Gradual Dependently Typed Programming [Preprint]
Abstracting gradual typing moving forward: precise and space-efficient [Tech Report] [Video]
Comparing Block-based Programming Models for Two-armed Robots. [Preprint] [Supplementary Data]
Gradual Typing as if Types Mattered
Approximate Normalization for Gradual Dependent Types
[Video]
Novice-friendly Multi-armed Robotics Programming
Refining Semantics for Multi-Stage Programming
Type-Driven Gradual Security with References
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.
Refining semantics for multi-stage programming
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
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.
Abstracting gradual typing
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.
Essential retroactive weavingAdvances 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.
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.
Principal
Type Schemes for Gradual Programs
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.
Foundations of
Typestate-Oriented
ProgrammingTypestate 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.
Confined Gradual TypingAdding 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.
A Theory of Gradual Effect SystemsEffect 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#
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.
Calculating Threesomes, with Blame
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
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.
Permission-based programming languages (NIER track)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
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.
Toward foundations for type-reflective metaprogrammingC++ 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
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.
Lazy evaluation and delimited controlThis 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
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.
A comparative study of language support for generic programmingBoth 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.
Interpretations of the gradually-typed lambda calculusGradual 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
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.