Lindsey Kuper

Assistant Professor
Computer Science and Engineering Department
Baskin School of Engineering
University of California, Santa Cruz

Ph.D., 2015
Indiana University

lkuper@ucsc.edu

CV · Blog · GitHub · Mastodon · YouTube

🏰  Research overview

My work draws on the research traditions of programming languages, distributed systems, and software verification. I work on programming-language-based approaches to building concurrent and distributed software systems that are elegant, correct, and efficient. The unifying principle and goal of my research is to use high-level abstractions to express software systems in a way that enables both correctness and efficiency.

The current members of my group are Jonathan Castello (PhD), Tim Goodwin (PhD, co-advised with Andrew Quinn), Shun Kashiwa (MS), Nathan Liittschwager (PhD), Patrick Redmond (PhD), and Gan Shen (PhD). Together, we're the CASL group, which is part of the larger Languages, Systems, and Data (LSD) Lab. Our name is pronounced like "castle" and symbolizes strength, safety, longevity, and a bit of magic and whimsy. Here's a summary of what we're up to as of mid-2023.

Our research has been supported by an NSF CAREER Award, a Stellar Development Foundation Academic Research Grant, a Google Faculty Research Award, and a gift from Amazon Web Services. Special thanks to Zulip for a generous in-kind sponsorship, too!

👩🏻‍🏫  Teaching

I've taught the following courses at UC Santa Cruz:

• CSE114A: Foundations of Programming Languages (Spring 2024; Spring 2023; Spring 2022)
• CSE138: Distributed Systems (Winter 2024; Fall 2021; Spring 2021; Spring 2020; Spring 2019 (as CMPS128))
• CSE232: Distributed Systems (Fall 2023; Fall 2021; Fall 2020)
• CSE290S: Distributed Software Systems: Global-First and Local-First Perspectives (Winter 2023)
• CSE30: Programming Abstractions: Python (Winter 2020)
• CSE290Q: SMT Solving and Solver-Aided Systems (Fall 2019) (retrospective blog post)
• CMPS290S: Languages and Abstractions for Distributed Programming (Fall 2018) (retrospective blog post)

While teaching remotely in 2020 and 2021, I live-streamed my undergraduate distributed systems lectures on Twitch! All the lecture videos from the course (Spring 2020, Spring 2021) are available on YouTube, where they have collectively been viewed over 150,000 times according to YouTube analytics as of 2023.

🛠️  Service

I co-founded the !!Con and !!Con West conferences of ten-minute talks on the joy, excitement, and surprise of computing. I serve on the board of the Exclamation Foundation, the nonprofit entity behind !!Con and !!Con West.

I chaired or co-chaired PLMW @ ICFP 2021, PLMW @ ICFP 2020, DSLDI 2018, DSLDI 2017, OBT 2017, and OBT 2016. I served as Publicity Chair of the ICFP Steering Committee, 2015—18, and as a member of the PLMW Steering Committee, 2021—23.

I have served on the program committees (why review papers?) of ICFP 2024, HATRA 2023, FHPNC 2023, PaPoC 2023, POPL 2023, PLDI 2021, ASPLOS 2021, PLOS 2019, PaPoC 2019, the SPLASH 2018 Doctoral Symposium, OOPSLA 2018, PaPoC 2018, ICFP 2017, DSLDI 2016, IFL 2015, Onward! Papers 2015, PaPoC 2015, OBT 2015, IFL 2014, and the Haskell Symposium 2014, and on the external review committees of OOPSLA 2021, PLDI 2020, PLDI 2019, PLDI 2018, ECOOP 2016, and POPL 2016.

🌱  Recent drafts

• Inductive diagrams for causal reasoning.
  Jonathan Castello, Patrick Redmond, and Lindsey Kuper.
  Draft, 2023.

🏡  Publications

• An exceptional actor system (functional pearl). (doi)
  Patrick Redmond and Lindsey Kuper.
  Haskell Symposium 2023
• HasChor: functional choreographic programming for all (functional pearl). (doi)
  Gan Shen, Shun Kashiwa, and Lindsey Kuper.
  ICFP 2023
  Recipient of ICFP 2023 Distinguished Paper Award
  (Artifact successfully evaluated)
• CRDTs, coalgebraically. (doi)
  Nathan Liittschwager, Stelios Tsampas, Jonathan Castello, and Lindsey Kuper.
  CALCO 2023
• What goes wrong in serverless runtimes? A survey of bugs in Knative Serving. (doi)
  Tim Goodwin, Andrew Quinn, and Lindsey Kuper.
  SESAME 2023
• Verified causal broadcast with Liquid Haskell. (doi)
  Patrick Redmond, Gan Shen, Niki Vazou, and Lindsey Kuper.
  IFL 2022
• Toward hole-driven development in Liquid Haskell.
  Patrick Redmond, Gan Shen, and Lindsey Kuper.
  HATRA 2021
• Toward SMT-based refinement types in Agda.
  Gan Shen and Lindsey Kuper.
  HATRA 2021
• Verifying replicated data types with typeclass refinements in Liquid Haskell. (doi)
  Yiyun Liu, James Parker, Patrick Redmond, Lindsey Kuper, Michael Hicks, and Niki Vazou.
  OOPSLA 2020
  (Artifact successfully evaluated)
• Toward domain-specific solvers for distributed consistency. (doi)
  Lindsey Kuper and Peter Alvaro.
  SNAPL 2019
• Toward scalable verification for safety-critical deep networks.
  Lindsey Kuper, Guy Katz, Justin Gottschlich, Kyle Julian, Clark Barrett, and Mykel J. Kochenderfer.
  SysML 2018
  (Poster also available)
• Parallelizing Julia with a non-invasive DSL. (doi)
  Todd A. Anderson, Hai Liu, Lindsey Kuper, Ehsan Totoni, Jan Vitek, and Tatiana Shpeisman.
  ECOOP 2017
  (Artifact successfully evaluated)
• Taming the parallel effect zoo: extensible deterministic parallelism with LVish. (doi)
  Lindsey Kuper, Aaron Todd, Sam Tobin-Hochstadt, and Ryan R. Newton.
  PLDI 2014
  (Artifact successfully evaluated)
• Joining forces: toward a unified account of LVars and convergent replicated data types.
  Lindsey Kuper and Ryan R. Newton.
  WoDet 2014
• Freeze after writing: quasi-deterministic parallel programming with LVars. (doi)
  Lindsey Kuper, Aaron Turon, Neelakantan R. Krishnaswami, and Ryan R. Newton.
  POPL 2014
• LVars: lattice-based data structures for deterministic parallelism. (doi)
  Lindsey Kuper and Ryan R. Newton.
  FHPC 2013
• A pattern matcher for miniKanren, or, how to get into trouble with CPS macros.
  Andrew W. Keep, Michael D. Adams, Lindsey Kuper, William E. Byrd, and Daniel P. Friedman.
  Scheme 2009

📕  Dissertation

• Lattice-based data structures for deterministic parallel and distributed programming.
  September 2015.

🏚  Older drafts

These papers are not being actively worked on and may be in disrepair.

• Deterministic threshold queries of distributed data structures.
  Lindsey Kuper and Ryan R. Newton.
  Draft, July 2014.
• Parametric polymorphism through run-time sealing, or, theorems for low, low prices!
  Amal Ahmed, Lindsey Kuper, and Jacob Matthews.
  Draft, fall 2011.
• Efficient representations for triangular substitutions: A comparison in miniKanren.
  David C. Bender, Lindsey Kuper, William E. Byrd, and Daniel P. Friedman.
  Draft, January 2010.

🎤  Talks

• What could go wrong?
  • Sunday Assembly Silicon Valley, Mountain View, CA, USA, August 13, 2023.
• Verified causal broadcast with Liquid Haskell.
  • Programming Languages and Verification Seminar, Portland State University, online, March 23, 2023.
  • Dagstuhl Seminar 23112: Unifying Formal Methods for Trustworthy Distributed Systems, Wadern, Germany, March 13, 2023.
  • Programming Systems Seminar, University of California, Berkeley, Berkeley, CA, USA, October 24, 2022.
  • Programming Languages & Software Engineering Seminar, National University of Singapore, online, October 12, 2022.
  • IFL 2022, Copenhagen, Denmark, August 31, 2022.
• Causally ordered communication, cooked three ways.
  • IFIP TC2 Working Group 2.16 (Programming Language Design), Claremont, CA, USA, January 11, 2023.
• Adventures in building reliable distributed systems with Liquid Haskell.
  • Keynote talk at FLOPS 2022, online, May 10, 2022. (video)
• Reasoning under uncertainty in SMT solving, research, and life.
  • Programming Languages Mentoring Workshop at PLDI 2021, online, June 21, 2021.
  • Programming Languages Mentoring Workshop at POPL 2020, New Orleans, LA, USA, January 21, 2020.
• Using solver-aided languages to build reliable distributed systems.
  • Computer Science and Engineering Colloquium, University of California, Riverside, online, December 11, 2020.
• A few big ideas from distributed systems.
  • Blizzard Entertainment, Inc., Irvine, CA, USA, July 24, 2019.
• Toward domain-specific solvers for distributed consistency.
  • Shonan Meeting No. 143: Programming Language Support for Data-Intensive Applications, Hayama, Japan, July 2, 2019.
  • SNAPL 2019, Providence, RI, USA, May 16, 2019.
• Domain-specific SMT solving for neural network verification (or anything else).
  • IFIP TC2 Working Group 2.16 (Programming Language Design), Portland, OR, USA, February 6, 2019.
• Abstractions for expressive, efficient parallel and distributed computing.
  • Jane Street Tech Talk, New York, NY, USA, January 24, 2019. (video)
  • UC Santa Cruz, Santa Cruz, CA, USA, March 5, 2018.
• Proving that safety-critical neural networks do what they're supposed to!
  • The Recurse Center, New York, NY, USA, May 8, 2017.
• A tour of ParallelAccelerator.jl: a library and compiler for high-level, high-performance scientific computing in Julia.
  • Center for Computer Research in Music and Acoustics, Stanford University, Palo Alto, CA, USA, January 18, 2017.
  • JuliaCon 2016, Cambridge, MA, USA, June 24, 2016. (video)
• Prospect: a library and compiler for high-level, high-performance scientific computing in Julia.
  • University of California, Berkeley, Berkeley, CA, USA, April 14, 2016.
• Prospect: finding and exploiting parallelism in a productivity language for scientific computing.
  • SPLASH-I 2015, Pittsburgh, PA, USA, October 29, 2015. (video)
• LVars for distributed programming, or, LVars and CRDTs join forces.
  • IFIP TC2 Working Group 2.8 (Functional Programming), Kefalonia, Greece, May 26, 2015.
• LVars: lattice-based data structures for deterministic parallel and distributed programming.
  • Compose :: Conference, New York, NY, USA, January 31, 2015.
  • The Recurse Center, New York, NY, USA, March 24, 2014.
  • Intel Labs, Santa Clara, CA, USA, March 21, 2014.
  • University of Utah, Salt Lake City, UT, USA, March 4, 2014.
  • Microsoft Research, Mountain View, CA, USA, January 27, 2014.
• Joining forces: toward a unified account of LVars and convergent replicated data types.
  • WoDet 2014, Salt Lake City, UT, USA, March 2, 2014.
• Freeze after writing: quasi-deterministic parallel programming with LVars.
  • POPL 2014, San Diego, CA, USA, January 23, 2014.
• LVars: lattice-based data structures for deterministic parallelism.
  • Mozilla Corporation, Mountain View, CA, USA, October 31, 2013.
  • RICON West 2013, San Francisco, CA, USA, October 29, 2013. (video (starting at about 1:36:00 in the linked recording))
  • FHPC 2013, Boston, MA, USA, September 23, 2013.
  • The Recurse Center, New York, NY, USA, June 10, 2013.
• A lattice-based approach to deterministic parallelism.
  • MPI-SWS, Saarbrücken, Germany, January 30, 2013. (video)
  • POPL 2013 student talk session, Rome, Italy, January 25, 2013.
• A lattice-based approach to deterministic parallelism with shared state.
  • Aarhus University, Aarhus, Denmark, September 14, 2012.
  • University of California, Berkeley, Berkeley, CA, USA, August 16, 2012.
• Rust typeclasses turn trait-er.
  • Mozilla Corporation, Mountain View, CA, USA, August 9, 2012. (video)
• Hacking the Rust object system at Mozilla.
  • Grinnell College, Grinnell, IA, USA, April 5, 2012.
    (invited talk, hosted by the Grinnell Alumni Scholars Program)
• Some pieces of the Rust object system: extension, overriding, and self.
  • Mozilla Corporation, Mountain View, CA, USA, August 18, 2011.
• Parametric polymorphism through run-time sealing, or, theorems for low, low prices!
  • Northeastern University, Boston, MA, USA, February 23, 2011.
• A system for testing specifications of CPU semantics, or, what I did on my summer vacation.
  • GrammaTech, Inc., Ithaca, NY, USA, August 20, 2010.

👨‍👩‍👧  ‍Personal

My husband, Alex Rudnick, does computational linguistics! We like to run marathons together, and run after Sylvia.