ARLI @ SPL🔗

Our logo: a cat face formed from the letters ARLI Abstractions for Reasonable Language Implementations, part of the Software Practices Lab at UBC.

Our lab is interested in developing programming language technology that enables programmers to better communicate their software and their intent to machines and other programmers, and that enables programmers to better reason about their software. This takes many forms: developing new language abstractions and new type system; designing new compilers; proving meta-theoretic properties about programming languages and language implementations; and designing and implementing new languages; and designing and implementing new tools for language implementation.

Acknowledgements🔗

Our lab practices at the UBC Point Grey (Vancouver) campus, which sits on the ancestral and unceded territory of the xʷməθkʷəy̓əm (Musqueam) First Nation.

Our work has been generously supported by: Galois; Amazon Research Awards; Huawei; the Natural Sciences and Engineering Research Council of Canada (NSERC) (RGPIN-2019-04207); the US Defense Advanced Research Projects Agency (DARPA) and Naval Information Warfare Center Pacific (NIWC Pacific) (under Contract No. NN66001-22-C-4027).

News🔗

Members🔗

Recruiting🔗

Interested in joining the lab? Unfortunately, I’m not currently accepting any new students.

See our supervisory expectations to understand more about what to expect: Supervisory Agreement and Expectations v3. You can research these posts for advice on how to apply, and what we want to see in application materials:

Current Members🔗

Paulette Koronkevich's headshot

Paulette Koronkevich

    

Ph.D. candidate working on the semantics of predicative references and a theory of universes for memory management. Formerly, completed a masters thesis with me: ANF Preserves Dependent Types up to Extensional Equality.

Ph.D. student working on extensible type systems and gradual dependent types.

    

Sean Bocirnea's headshot

Sean Bocirnea

Chester J. F. Gould's headshot

Chester J. F. Gould

    

M.Sc. student working logical frameworks for type preserving compilation.

Alumni🔗

Adam T. Geller

    

Completed a M.Sc. on Index-Typed WebAssembly; joined Nvidia's Quantum Compilers Team!

Lily Bryant

    

Completed an M.Sc. on compilation as multi-language semantics.

Junfeng Xu

    

Completed an M.Sc. on formal semantics of programming language meta-notation.

Jonathan Chan

    

Completed an M.Sc. on semantics of sized typing in extensional type theory

Justine Frank

    

Interned working on index-typed WebAssembly.

Ramon Rakow

    

Interned working on dependent-type-preservation for ANF.

"Michael" Yufeng Li

    

Interned working on the semantics of sized types for Rocq.