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🔗

Paulette Koronkevich

    

Ph.D. candidate working on the semantics of predicative references.

Sean Bocirnea

    

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.

Adam T. Geller

    

Ph.D. student working on indexed type systems for safety and performance. Formerly, completed a masters thesis with me on Index-Typed WebAssembly.

Alumni🔗

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.