New Jersey
Programming Languages and Systems
Seminar

FSM is a domain specific language embedded in Racket developed for the Formal Languages and Automata Theory classroom. It aims to make such a course and the rigor it requires more appealing to Computer Science students trained in programming. In FSM, programmers can construct regular expressions, state-based machines (i.e., dfa, ndfa, pda, Turing machines, and multitape Turing machines), grammars (i.e., regular, context-free, and context-sensitive), and may implement the algorithms developed as part of a constructive proof. In addition, FSM provides a rich set of primitives and visualization tools to observe and understand the behavior of such computation models. This talk outlines how students are taught to design, implement, and prove correct their state machines. In addition, we shall illustrate how students are taught to implement their construction algorithms before attempting to prove correctness.

We elucidate the essence of Object-Oriented Programming (OOP) using a constructive approach: we identify a minimal basis of concepts with which to synthesize existing and potential object systems. We reduce them to constructions atop the pure untyped lambda calculus, thereby obtaining both denotational semantics and effective implementation.

We start from the simplest recognizable model of prototype-based OOP, so simple it arguably does not even have “objects” as such. We build further models of increasing sophistication, reproducing a growing subset of features found in past object systems, including original combinations.

We discuss how to deal with issues like types, modularity, classes, mutation—and associated tradeoffs. We use Scheme to illustrate our approach.

Strong functional programming as proposed by David Turner is a form of FP where all functions are required to pass a static check for termination. Turner's proposal did not include a path towards practicality, where terminating and nonterminating code could be combined. In this talk, I propose a practical approach to strong FP, based on Haskell's monadic approach to impure functions. I describe the language DCS, which provides a sophisticated type-based termination analysis for the core language, to which possibly diverging or impure code can be added using monads. DCS uses subtyping to elide coercions required by that interface, as well as others needed for the monadic approach. The type-based termination method supports divide-and-conquer programming, where recursive calls are permitted on values that are not subdata of the original inputs (like lists obtained by the splitting step in mergesort). Thanks to subtyping, examples like mergesort can then be written in a very natural style in DCS. The tool, which is a Haskell backend combined with an emacs mode, will be demoed.

In type systems with dependency tracking, programmers can assign an ordered set of levels to computations and prevent information flow from high-level computations to the low-level ones. The key notion in such systems is \emph{indistinguishability}: a definition of program equivalence that takes into account the parts of the program that an observer may depend on. In this paper, we investigate the use of dependency tracking in the context of dependently-typed languages. We present the Dependent Calculus of Indistinguishability (DCOI), a system that adopts indistinguishability as the definition of equality used by the type checker. DCOI also internalizes that relation as an observer-indexed propositional equality type, so that programmers may reason about indistinguishability within the language. Our design generalizes and extends prior systems that combine dependency tracking with dependent types and is the first to support conversion and propositional equality at arbitrary observer levels. We have proven type soundness and noninterference theorems for DCOI and have developed a prototype implementation of its type checker.

Algorithms operating on real numbers are implemented as floating-point computations in practice, but floating-point operations introduce roundoff errors that can degrade the accuracy of results. We propose Λnum, a functional programming language with a type system that can express quantitative bounds on roundoff error. Our type system combines a sensitivity analysis, enforced through a linear typing discipline, with a novel graded monad to track the accumulation of roundoff errors. We prove that our type system is sound by relating the denotational semantics of our language to the exact and floating-point operational semantics.

To demonstrate our system, we instantiate Λnum with error metrics proposed in the numerical analysis literature, including several notions of relative error, and we show how to incorporate rounding operations that faithfully model aspects of the IEEE 754 floating-point standard. We show how the type system of Λnum can give useful bounds on roundoff error on a range of example numerical programs. Finally, we consider semantic extensions of our graded monad to bound error under more complex rounding behaviors, such as non-deterministic and randomized rounding.

This talk introduces Stratified Type Theory (StraTT) where, rather than stratifying a hierarchy of universes by levels, as is common in dependent type theories, we instead stratify typing judgements. To retain logical consistency, the level of the domain of dependent function types is strictly lower than that of the overall type. To increase expressivity, we remove this restriction for nondependent function types and use McBride's crude-but-effective stratification (also known as displacement) to allow uniformly displacing top-level definitions to higher levels as a crude form of level polymorphism. We explore both the expressivity of StraTT as well as its logical consistency.

We introduce simple, universal, sound, and complete proof methods for producing machine-verifiable proofs of linearizability and its close cousin, strong linearizability. Universality means that our method works for any object type; soundness means that an algorithm can be proved correct by our method only if it is linearizable (resp. strong linearizable); and completeness means that any linearizable (resp. strong linearizable) implementation can be proved so using our method. We demonstrate the simplicity and power of our method by producing proofs of linearizability for the Herlihy-Wing queue and Jayanti's single-scanner snapshot, as well as a proof of strong linearizability of the Jayanti-Tarjan union-find object. All three of these proofs are machine-verified by TLAPS (the TLA+ Proof System).

Concurrent search structure templates are a technique for separating the verification of a concurrent data structure into concurrency-control and data-structure components, which can then be modularly combined with no additional proof effort. In this work, we implement the template approach in the Verified Software Toolchain (VST), and use it to prove correctness of C implementations of fine-grained concurrent data structures.

Flow analysis plays a critical role in program optimization by producing semantic facts, which enable non-local, interprocedural program transformations. Unfortunately, these non-local transformations often don't preserve well-typedness of the intermediate representation, and so they are difficult to perform in compilers that preserve types throughout compilation (e.g. every intermediate representation is well-typed). In this talk we discuss how to perform these transformations in the typed setting, which relies on producing facts via the type system itself, extending the ideas and applications of ["Better Defunctionalization through Lambda Set Specialization" by Brandon, et al.]. Producing these facts through the type system turns out to be inexpensive --- only adding a small operation to each unification step during type inference --- so this method yields a cheap and easy-to-implement flow analysis.

Examples of useful non-local program transformations for functions in particular are defunctionalization, unused parameter/argument removal, unboxing, argument flattening, and uncurrying. We also discuss other program transformations (that don't deal with functions), such as an automatic list to vector transformation.

In turns out that just like classic abstract interpretations (e.g. k-CFA), this "type-derived analysis" can be tuned for higher or lower precision, via a special kind of polymorphism. In particular, for any k, there are programs for which it is more precise than k-CFA!

In most cases, this polymorphism is simply an analysis artifact: once used to obtain semantic facts, it can be erased from the program. However, we show that other choices for resolving this polymorphism, such as dynamically passing around a form of type tag, can yield even more opportunities for optimizations.

On microcontrollers, timer devices provide high-precision timing, but that precision is lost when using high-level languages without suitable abstractions for temporal behavior. So, for timing-sensitive applications, programmers resort to low-level languages like C which provide direct access to those devices, but lack expressiveness and safety guarantees.

In this talk, I will discuss how we achieve sub-microsecond precision from a high-level programming language on the RP2040, a cheap, widely available microcontroller. We take advantage of the RP2040’s Programmable I/O (PIO) devices to implement input capture and output compare peripherals. These timestamp peripherals mediate I/O events to and from software written in Sslang, a synchronous, ML-like programming language. When we couple Sslang's precise timing abstractions with a suitable implementation in hardware, Sslang programs are capable of achieving timing accuracy on par with that of the RP2040's timer hardware.

We describe a style of applying symbolic model checking developed over the course of eight years at Amazon Web Services (AWS). Lessons learned are drawn from proving properties of numerous Rust and C-based systems, e.g., custom hypervisors, encryption code, boot loaders, an IoT operating system, a microVM manager and more. Using our methodology, we find that we can prove the correctness of industrial low-level Rust and C-based systems with reasonable effort and predictability. Furthermore, AWS developers are increasingly writing their own formal specifications. We also discuss the current challenges to provide unbounded guarantees at scale.

The harmonic analysis of music has a rich tradition of music theories that seek to explain the 'why' and 'how' a musical tradition sounds the way it does to listeners. Much of the work in automated analysis is carried out in an ad-hoc manner, with informal appeals to the underlying theory. We seek to reason about the harmonic analysis of certain forms of music in a similar way that the Programming Languages community reasons about program analysis.

Darais and Van Horn showed that by leveraging a theory of "Constructive Galois Connections" we can constructively reason about program analyses. We take this idea into the realm of Computer Music, where we treat the harmonic analysis of a score as a program analysis. This requires us to make explicit the nature of the scores we are able to analyze, as well as the musical theory in which the analysis takes place.

Much of benefit from Constructive Galois Connections comes from an appropriate choice of abstract domain. Therefore, we must be intentional with the choice of abstract domain for 'Music'. The various soundness properties in program analysis have a related set of concerns in harmonic analysis, which is 'sound' in a different way.

This is work in progress, and we are hoping to solicit feedback on the nature of the domains we believe can lead to interesting harmonic analysis.