ARLI @ SPL
Abstractly Reasoning about 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
-
Oct. 2025: Our lab has 5 talks and 4 papers at ICFP/OOPSLA 2025! See our ICFP/OOPSLA 2025 page for more!
-
Sept. 2025: William finally got around to making the lab a website.
Members
Interested in joining the lab? We’re not recruiting now, but see our supervisory expectations to understand more about what to expect: Supervisory Agreement and Expectations v3.
|
|
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. |
|
|
|
|
Ph.D. student working on indexed type systems for safety and performance. Formerly, completed a masters thesis with me on Index-Typed WebAssembly. |
|
M.Sc. student working logical frameworks for type preserving compilation. |
|
|
Alumni
|
|
Completed an M.Sc. on compilation as multi-language semantics. | |
|
Junfeng Xu |
|
Completed an M.Sc. on formal semantics of programming language meta-notation. |
|
|
Completed an M.Sc. on semantics of sized typing in extensional type theory | |
|
|
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. |