I am an Assistant Professor in the Computer Science and Engineering Department at the University of California, San Diego. I am a member of the Programming Systems group. I completed my PhD in 2014 at ETH Zurich (Switzerland), under the supervision of Bertrand Meyer. After that, I spent some time as a postdoc at MIT CSAIL, where I worked with Armando Solar-Lezama. I am a 2020 Sloan Fellow and a recipient of the 2020 Intel Rising Stars Award and the 2020 NSF CAREER Award. My research interests are in program synthesis, program verification, and type systems.
active projects:
older projects:
current:
alumni:
spring 2021 | CSE 130: Programming Languages |
winter 2021 | CSE 291: Program Synthesis |
fall 2020 | CSE 130: Programming Languages |
spring 2020 | CSE 130: Programming Languages |
winter 2020 | CSE 291: Program Synthesis |
fall 2019 | CSE 130: Programming Languages |
winter 2019 | CSE 130: Programming Languages |
fall 2018 | CSE 291: Program Synthesis |
spring 2018 | CSE 130: Programming Languages |
fall 2017 | CSE 291: Program Synthesis |
recent talks:
2021 | Liquid Information Flow Control (Chalmers Security Seminar) [slides] |
Liquid Information Flow Control (WG2.8 2021) [slides] | |
Generating Programs from Types (Lambda Days 2021) [slides] | |
2020 | Generating Programs from Types (Keynote at APLAS'20) [video] |
Constraint Solvers for the Working PL Researcher (PLMW@ICFP) [slides] [video] | |
Program Synthesis (PL+HCI “Swimmer” School) [slides] [video] | |
Liquid Resource Types for Verification and Synthesis (Chalmers Seminar on Functional Programming) [slides] [video] [example: compress] [example: linear-time compress] [example: insertion sort] [example: insertion sort (fine-grained bound)] | |
Liquid Resource Types for Verification and Synthesis (WG2.8 2020) [slides] | |
SuSLik: Synthesis of Safe Pointer-Manipulating Programs (Invited talk at ADSL'20) [slides] | |
Synthesizing Programs from Types (Tutorial at POPL'20) [slides] | |
2019 | SuSLik: Synthesis of Safe Pointer-Manipulating Programs (Tutorial at FMCAD'19) [slides] |
Generating Programs from Types (Harvey Mudd College) [slides] | |
Type-Driven Program Synthesis (Facebook Menlo Park and Google Brain) [slides] | |
Synthesis of Safe Pointer-Manipulating Programs (Purdue and University of Wisconsin) [slides] | |
2018 | Constraint Solvers for the Working PL Researcher (PLMW@ICFP) [slides] [video] [code] [code] [code] |
Type-Driven Program Synthesis (Strangeloop) [slides] [video] |
program (co-)chair:
2020 | VSTTE |
2017 | iFM |
program committees:
2021 | POPL, OOPSLA |
2020 | ICFP, VMCAI, ADSL |
2019 | PLDI, SecDev, HCVS, Haskell |
2018 | OOPSLA, SYNT, POPL |
2017 | CAV, SYNT |
2016 | APLAS, FTfJP, SYNT, VSTTE, TAP, iFM, FESCA, VMCAI |
2015 | PSI, FTfJP, FESCA |
2014 | RV, FESCA. |
external review committees:
2019 | ICFP |
2018 | PLDI |