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
"Permit yourself to open a book and start reading from anywhere."
— Manuel Blum
π° 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:
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
π‘ 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
π 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?
- 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.
- Adventures in building reliable distributed systems with Liquid Haskell.
- Reasoning under uncertainty in SMT solving, research, and life.
- 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).
- 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!
- 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.
- Prospect: finding and exploiting parallelism in a productivity language for scientific computing.
- LVars for distributed programming, or, LVars and CRDTs join forces.
- 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.
- Freeze after writing: quasi-deterministic parallel
programming with LVars.
- 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.
- 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.
- Hacking the Rust object system at Mozilla.
- Some pieces of the Rust object system: extension,
overriding, and self.
- Parametric polymorphism through run-time sealing, or,
theorems for low, low prices!
- A system for testing specifications of CPU semantics, or,
what I did on my summer vacation.
π¨βπ©βπ§ βPersonal
My husband, Alex
Rudnick, does computational linguistics! We like to run marathons
together, and run after Sylvia.