ARLI @ SPL
ARLI @ SPL
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
-
Aug. 2026: Paulette presented our work-in-progress relating Regions and Continuation Marks at Scheme 2026! See the short paper!
-
July 2026: Paulette gave a talk, Paradoxes and Proofs with Pointers, at WiL 2026! See the extended abstract!
-
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
Recruiting
Interested in joining the lab? Unfortunately, I’m not currently accepting any new students.
Current Members
|
|
Ph.D. candidate working on the semantics of predicative references and a theory of universes for memory management. Formerly, completed a masters thesis with ARLI: ANF Preserves Dependent Types up to Extensional Equality. |
|
Undergraduate student working on implementing kind-based regions for memory management. |
|
|
|
|
Ph.D. student working on extensible type systems and gradual dependent types. |
|
M.Sc. student working on logical frameworks for type preserving compilation. |
|
|
|
|
Undergraduate student working on logical frameworks for type-preserving compilation. |
|
M.Sc. student working on type-safety and type-preservation for assembly languages. |
|
|
|
|
Undergraduate student working on logical frameworks for type-preserving compilation. |
Alumni
|
|
Completed an M.Sc. on Index-Typed WebAssembly; joined Nvidia's Quantum Compilers Team! | |
|
|
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. |