AppelFest! May 4, 2024 Princeton University

AppelFest is a celebration honoring the career and work of Andrew Appel. The event will feature talks from Andrew’s students and collaborators, discussing a broad range of topics, from functional programming, compilers, and run-time systems to denotational semantics and verification to public policy and voter safe-guards.  We may even see some physics!

General Chair: David Walker        Program Chair: Gary Tan

8:30-9am               Breakfast and coffee

9-9:10am        Opening remarks

- Andrew Appel. An appreciation of my mentors, collaborators, and students

9:10-10:30am Talks (Session Chair:David Walker)

- John Reppy. Safe-for-space closure conversion revisited

- Zhong Shao. A Compositional Theory of Linearizability

- Amal Ahmed. The unusual effectiveness of step-indexed logical relations

- Andrew Tolmach. Back to Indirect Style

10:45-12pm Talks (Session Chair: Gary Tan)

- Xavier Leroy. On foundational approaches: from FPCC to VST and beyond

- Adam Chlipala. From Functional-Language Compilers to Verified Cryptography

- Lennart Beringer. Objects, subtyping, and VST

- Sandrine Blazy. Learning Coq in Paris

12-1pm Lunch

1:15-2:35pm Talks (Session Chair: Lujo Bauer)

- J. Alex Halderman. Election Security in 2024

- Xinming Ou. From Turing to Polanyi, and back: a journey about anthropology and cybersecurity

- Dinghao Wu. The Good Olden Days with Andrew

- Santiago Cuellar. Let the Tiger (compiler) choose its target (architecture)

3-4:20pm Talks (Session Chair:  Amal Ahmed)

- Kai Li. Collecting Garbage with Andrew

- Jon Bentley. Andrew Appel and Recursive Partitioning

- Dave Naumann. Man on fire: a personal appreciation of Andrew Appel

- Dave MacQueen. Andrew and Standard ML of New Jersey.

5:00                Reception and Dinner at Brick Farm Tavern

Talk abstracts

Safe-for-space Closure Conversion Revisited

John Reppy (University of Chicago)

Abstract: One of the key implementation issues for higher-order functional languages is managing the environment structure that arises from first-class function values.  The standard approach to this problem is *closure conversion*, which is a compiler transformation that introduces an explicit data structure to represent the environment of a function value.  Andrew Appel has worked on this problem several times over the past 35 years (most recently with Zoe Paraskevopoulou in 2019). In this talk, we revisit the work by Andrew and Zhong Shao on ``safe-for-space closure conversion'' in the Standard ML of New Jersey compiler.  In this new work, we use higher-order control-flow analysis to provide more precise analysis information for making environment-representation decisions.

         Joint work with Byron Zhong (University of Chicago).

 A Compositional Theory of Linearizability

Zhong Shao (Yale University)

Abstract: A common theme in Andrew’s research is about building realistic compilers and verification systems using foundational language theory and formal methods. In this talk, I will present a new general semantics for supporting horizontal and vertical composition of linearizable concurrent objects. We start by showcasing a common issue, which is independent of linearizability, in the construction of compositional models of concurrent computation: interaction with the neutral element for composition can lead to emergent behaviors, a hindrance to compositionality. Category theory provides a solution for the issue in the form of the Karoubi envelope. Surprisingly, this abstract construction is deeply related to linearizability and leads to a novel formulation of it. Notably, this new formulation neither relies on atomicity nor directly upon happens-before ordering and is only possible because of compositionality, revealing that linearizability and compositionality are intrinsically related to each other. We use this new, and compositional, understanding of linearizability to revisit much of the theory and practice of building certified concurrent abstraction layers.

The unusual effectiveness of step-indexed logical relations

Amal Ahmad (Northeastern University)

Abstract: Andrew and Dave McAllester developed the first step-indexed model for recursive types in 2001, which I then scaled up to a model of mutable references in my PhD thesis. In the years since, step-indexing has has been unusually effective in applying to a wide range of language and logic features. It has become so ubiquitous, and incorporated into logics like Iris and VST, that people barely cite the original papers any more!  In this talk, I'll do a trip down memory lane to the early days of the Foundational Proof-Carrying Code project when step-indexing was born, and then talk about a novel form of step indexed relation that I'm using these days for verifying type soundness in the presence of language interoperability.

Back to Indirect Style

Andrew Tolmach (Portland State University)

Abstract: Andrew's oeuvre continues to anchor my bookshelf. I will describe work-in-progress on (mini) Dynamix, a DSL for specifying the dynamic semantics of an (object) language via its transformation into "Green Book" CPS. A Dynamix program is intended to be as readable as a definitional interpreter, while still generating a reasonably efficient compiler.  I will illustrate the style of Dynamix by showing some of the definition of the "Tiger Book" language.

On foundational approaches: from FPCC to VST and beyond

Xavier Leroy (Collège de France)

Abstract: The Foundational Proof-Carrying Code (FPCC) project, started by Andrew Appel in 1999, pioneered several approaches that are now widely used, such as step-indexing to break circularities in semantic definitions. I will reflect on another innovation of FPCC, part of the "Foundational" approach: the idea that a type system or program logic can be derived in a sound-by-construction manner from a low-level operational semantics, and on how this idea led to a resurgence of program logics, no longer as Hoare-style axiomatic systems, but as theories embedded in interactive theorem provers, as exemplified in Andrew's VST project and in the Iris framework.

From Functional-Language Compilers to Verified Cryptography

Adam Chlipala (MIT)

Abstract: It's a suspicious coincidence how many people who used to work on ML compilers (I mean the *right* meaning of ML, of course) wound up working on compiler verification with proof assistants.  I'd like to tell my own related story, working up to bringing it all together in the context of cryptography, another Appel topic.  I'll sketch Fiat Cryptography, our formally verified functional-language compiler that's used to produce some of the fastest cryptographic software in production.

Objects, subtyping, and VST

Lennart Beringer (Princeton University)

Abstract: Although object-oriented programming does not constitute Andrew's favorite programming paradigm, supporting the abstraction and reasoning principles of objects is an often-cited motivation for step-indexed models. The talk will outline verification of object-oriented C programming in VST with a focus on subtyping in the sense of Liskov substitution, leading to some open problems concerning VST and its connection to CompCert.

Learning Coq in Paris

Sandrine Blazy (University of Rennes)

Abstract: I first met Andrew almost 20 years ago, when we were on sabbatical in Paris Rocquencourt. Each of us was working on our first Coq formalization, that would later become CompCert and VST. My talk will revisit two of our collaborations: the design of a new continuation-based semantic style and the formal verification of register allocation by graph coloring.

Election Security in 2024

J. Alex Halderman (University of Michigan)

Abstract: Elections face the challenge of producing trustworthy results while using untrustworthy computer systems. Work by Andrew Appel and other scientists over the past 20 years has produced sweeping changes to the way the U.S. counts its votes, but significant risks remain. In this talk, I’ll discuss some of the open research questions and the most pressing problems facing security and policy as we prepare for the 2024 presidential election.

From Turing to Polanyi, and back -- a journey about anthropology and cybersecurity

Xinming Ou (University of South Florida)

Abstract: My work with Andrew during my PhD led to my later work of applying anthropology to cybersecurity. During that inquiry I came to know a debate between Michael Polanyi and Alan Turing in 1949, during the symposium on Mind and Machine organized by the Department of Philosophy at the University of Manchester. This debate laid the seed for Turing's seminal paper on artificial intelligence a year later. It also motivated Polanyi to formulate the notion of tacit knowledge, as an exposition of his belief that a machine can never achieve real human intelligence. As a cybersecurity researcher applying anthropological methods, I had been solidly subscribed to Polanyi's belief, until about a year ago. The power illustrated by generative AI made me come back to revisit the 1949 debate and read a detailed transcript made available by Turing scholars. To my astonishment, it appears that Turing already foresaw the trajectory of AI long before the key breakthroughs we know today. From the conversation archive of 1949, it appears to me that Polanyi's opposition to Turing's formulation of AI was premised on Turing machine being the only computing model. Turing himself, back in 1949, was already not bound by this limit. I am now solidly back in Turing's camp.

The Good Olden Days

Dinghao Wu (Pennsylvania State University)

Abstract: In this short talk, I’ll present a few random points based on my good olden days experience with Andrew. The goal is to demystify some of Andrew’s traits that enable him to achieve both highly influential research and be extremely successful in mentoring students. I’ll focus mostly on a unique aspect of his advising style.

Let the Tiger (compiler) choose its target (architecture).

Santiago Cuellar (Galois, Inc.)

Abstract: What if the Tiger compiler, from Andrew’s book, had the autonomy to select its target architecture during compilation? This intriguing idea emerged in a project about Zero-Knowledge proofs that requires code to be translated into efficient (i.e. small) circuits. Using 'Modern Compiler Implementation' as a reference, our approach identified areas where the compiler is constrained by the architecture. We then replaced them with options for the compiler to customize its target. In this talk, I'll share both new and old lessons learned, along with various formal methods tricks that have enhanced our project.

Collecting Garbage with Andrew

Kai Li (Princeton University)

Abstract: I will briefly talk about the collaborative work with Andrew on real-time concurrent GC, published in 1988. The paper was later selected as one of the 50 influential papers in 20 years of PLDI.

Andrew Appel and Recursive Partitioning

Jon Bentley (Bell Labs Research, Retired)

Abstract: In this talk we’ll examine some of the many contributions of Andrew’s 1985 paper “An efficient program for many body simulation”, which was based on his 1981 Princeton Senior Thesis “An investigation of galaxy clustering using an asymptotically fast n-body algorithm”. We’ll examine it in the context of its time, and especially as an instance of the computational geometric tool of “data driven recursive partitioning”.

Man on fire: a personal appreciation of Andrew Appel

Dave Naumann (Stevens Institute of Technology)

Abstract: Personal remarks on Andrew's role in my scientific and academic life.

Andrew and Standard ML of New Jersey

David MacQueen (University of Chicago, Emeritus)

Abstract: I will talk about the early years of Standard ML of New Jersey and Andrew's part in creating that system.