Fall 2022 Seminars

Fall 2022

Organizer: Yao Li

All Talks

Date Title Speaker
Polarized Subtyping Zeeshan Lakhani
Towards Formalizing Representation Transformation Katherine Philip
Index-oriented programming: an exercise in abstract datatype design Mark P. Jones
Expanding the Reach of Fuzz Testing Caroline Lemieux
ASTs in TypeScript: union and intersection types in practice Katie Casamento
Why functional programming matters Yao Li

Polarized Subtyping

Speaker: Zeeshan Lakhani

Zeeshan Lakhani is a co-founder and organizer of Papers We Love and PWLConf, an applied researcher working on local-first software, among other things, at fission.codes, and a Ph.D. student at Carnegie Mellon University’s School of Computer Science (S3D), studying Programming Language Theory under Frank Pfenning. Formerly, he was director of fraud engineering and strategic research at BlockFi, drove programmable networking at Comcast, worked on impactful distributed systems at Basho, co-wrote the Readability 2.0 iOS app while at Arc90, and helped drive interactive content at NYPL Labs.

Polarization of types in call-by-push-value naturally leads to the separation of inductively defined observable values (classified by positive types), and coinductively defined computations (classified by negative types), with adjoint modalities mediating between them. Taking this separation as a starting point, we develop a semantic characterization of typing with step indexing to capture observation depth of recursive computations. This semantics justifies a rich set of subtyping rules for an equirecursive variant of call-by-push-value, including variant and lazy records. We further present a bidirectional syntactic typing system for both values and computations that elegantly and pragmatically circumvents difficulties of type inference in the presence of width and depth subtyping for variant and lazy records. We demonstrate the flexibility of our system by systematically deriving related systems of subtyping for (a) isorecursive types, (b) call-by-name, and (c) call-by-value, all using a structural rather than a nominal interpretation of types.

Towards Formalizing Representation Transformation

Speaker: Katherine Philip

Representation transformation is a collection of compilation techniques that changes the representation of data value, while preserving the original program semantics. These techniques are what enables us to efficiently compile programs written in the Habit programming language. In this talk, I'll present some of our in-progress work where we're developing a formalization framework and a common calculus dubbed “Lambda I”—a lambda calculus with indexed lets. Then, I’ll share about how we used it to formalize specialization of polymorphism. In the long term, we hope that this framework can inspire more useful transformations and optimizations.

Index-oriented programming: an exercise in abstract datatype design

Speaker: Mark P. Jones

Arrays are one of the most fundamental and widely used data structures. And yet programmers continue to make seemingly basic mistakes using them, leading to significant vulnerabilities, even in mature and high profile software systems. Could we design an abstract datatype (or perhaps a set of abstract datatypes) to ensure that arrays are always used correctly, without compromising on either expressiveness or performance? In this talk, I'll provide an update on a (still unfinished) quest to answer this question, drawing on experiences with the House operating system, the design of the Habit programming language, and more recent attempts to explore the implementation of a capability-based microkernel. Along the way, we'll see some (possibly) new ways to think about loop variables and comparisons, while also contemplating some next steps for further rumination and experimentation.

Expanding the Reach of Fuzz Testing

Speaker: Caroline Lemieux

Caroline Lemieux is an Assistant Professor at the University of British Columbia. Her research aims to help developers improve the correctness, security, and performance of large, existing software systems, ranging from complex open-source projects to industrial-scale software. Her current projects tackle these goals with a focus on fuzz testing, specification mining, and program synthesis. Her work on fuzz testing has been awarded an ACM SIGSOFT Distinguished Paper Award, ACM SIGSOFT Distinguished Artifact Award, ACM SIGSOFT Tool Demonstration Award, and Best Paper Award (Industry Track). She received her PhD at UC Berkeley advised by Koushik Sen, where she was the recipient of a Berkeley Fellowship for Graduate Study and a Google PhD Fellowship in Programming Technologies and Software Engineering.

Software bugs are pervasive in modern software. As software is integrated into increasingly many aspects of our lives, these bugs have increasingly severe consequences, both from a security (e.g. Cloudbleed, Heartbleed, Shellshock) and cost standpoint. Fuzzing refers to a set of techniques that automatically find bug-triggering inputs by sending many random-looking inputs to the program under test. In this talk, I will discuss how, by identifying core under-generalized components of modern fuzzing algorithms, and building algorithms that generalize or tune these components, I have expanded the application domains of fuzzing. First, by building a general feedback-directed fuzzing algorithm, I enabled fuzzing to consistently find performance and resource consumption errors. Second, by developing techniques to maintain structure during mutation, I brought fuzzing exploration to “deeper” program states. Third, by decoupling the user-facing abstraction of random input generators from their sampling distributions, I built faster validity fuzzing and even tackled program synthesis. Finally, I will discuss the key research problems that must be tackled to make fuzzing readily-available and useful to all developers.

ASTs in TypeScript: union and intersection types in practice

Speaker: Katie Casamento

Why functional programming matters

Speaker: Yao Li