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.
Our lab and its work have been generously supported by: Galois; Amazon Researc 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).
Members
|
|
Ph.D. candidate working on the semantics of predicative references. | |
|
|
Ph.D. student working on extensible type systems and gradual dependent types. Formerly, completed a masters thesis with me: ANF Preserves Dependent Types up to Extensional Equality. | |
|
|
Ph.D. student working on indexed type systems for safety and performance. Formerly, completed a masters thesis with me on Index-Typed WebAssembly. |
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. |