I am an Associate 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. Since 2022, I am a member of the IFIP Working Group 2.8 on Functional Programming. My research interests are in program synthesis, program verification, and type systems.
active projects:
older projects:
current:
alumni:
spring 2024 | CSE 130: Programming Languages |
winter 2024 | CSE 291: Program Synthesis |
fall 2023 | CSE 130: Programming Languages |
spring 2023 | CSE 130: Programming Languages |
winter 2023 | CSE 291: Program Synthesis |
fall 2022 | CSE 230: Programming Languages (graduate) |
spring 2022 | CSE 130: Programming Languages |
winter 2022 | CSE 291: Program Synthesis |
fall 2021 | CSE 130: Programming Languages |
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:
2024 | AI-Assisted Programming Today and Tomorrow (Keynote at PLDI) [slides] |
2023 | How Programmers Interact with AI Assistants (Guest Lecture at UPenn) [slides] |
Big Ideas in Program Synthesis (PLMW @ PLDI'23) | |
How Programmers Interact with AI Assistants (DL4Code @ ICLR'23, ASA @ PLDI'23) [slides] | |
Leveraging Rust Types for Program Synthesis (WG 2.8 2023) [slides] | |
Big Ideas in Program Synthesis (PLMW @ POPL'23) [slides] | |
2022 | Tutorial on Deductive Program Synthesis (Summer School on Neurosymbolic Programming) [slides] |
Equality-Constrained Tree Automata (EGRAPHS 2022) | |
Learning Better Abstractions with E-Graphs and Anti-Unification (WG2.8 2022) [slides] | |
Hacking your CAREER (NSF CAREER Workshop 2022) [slides] | |
2021 | Synthesis of Safe Pointer-Manipulating Programs (EPFL) |
Live Programming and Programming by Example: Better Together (Berkeley PL Seminar) | |
Generating Programs from Types (Haskell eXchange 2021) [video] | |
Synthesis of Safe Pointer-Manipulating Programs (Workshop on Dependable and Secure Software Systems, ETH Zurich) [slides] [video] | |
SuSLik: Synthesis of Safe Pointer-Manipulating Programs (Tutorial at CAV'21) | |
Synthesis of Safe Pointer-Manipulating Programs (Invited Talk at LICS/ITP'21) [slides] [video] | |
Synthesis of Safe Pointer-Manipulating Programs (Isaac Newton Institute Workshop on Verified Software: Tools and Experiments) [slides] | |
Liquid Information Flow Control (Chalmers Security Seminar) [slides] | |
Liquid Information Flow Control (WG2.8 2021) [slides] | |
Generating Programs from Types (Lambda Days 2021) [slides] [video] | |
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:
2026 | OOPSLA |
2022 | Haskell |
2020 | VSTTE |
2017 | iFM |
program committees:
2024 | PLDI, Dafny |
2023 | POPL, OOPSLA, HATRA, MAPS |
2022 | PLDI, EGRAPHS |
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. |