Winter 2024 Seminars

Winter 2024

Organizer: Laura Israel

All Talks

Date Title Speaker
So, Monads. Laura Israel
Covering All the Bases: Type-Based Verification of Test Input Generators Zhe Zhou
The Left Hand of Equals Andrew Black
Name binding in real life: a beginner’s report on the philosophy of language Katie Casamento
The Persistence of Past: A Demand Semantics for Mechanized Cost Analysis of Lazy Programs Laura Israel

So, Monads.

Speaker: Laura Israel

Laura Israel is a first-year doctoral student at Portland State University studying formal verification with Yao Li. She has a particular interest in complexity theory and its formalization in proof assistants. Laura developed a passing interest in theoretical CS while getting her BA in Psychology at Reed College, resulting in a stint in the tech industry, then culminating in her current research at PSU. When she's not doing math thinly-veiled as computer science, you can find her hanging out with her cat Socks, running Dungeons and Dragons, or writing (and occasionally publishing) short stories.

Monads. Love them, hate them, understand them, or be confused by them. Whatever your opinion is on them, one thing is for certain: no one has an easy to understand explanation of what they are. In this more casual talk, I will facilitate discussion regarding each attendee's understanding of monads, present a few ideas that have helped me get a better idea of what they are, and maybe if we're lucky, I'll walk away from this talk feeling like I finally understand what a monad is. No prior knowledge of monads is assumed for this talk.

Covering All the Bases: Type-Based Verification of Test Input Generators

Speaker: Zhe Zhou

I am currently a PhD Student of Computer Science at Purdue University, advised by Prof. Suresh Jagannathan. My research interests lie in programming languages (PL) - program verification, property-based testing, type systems, and program synthesis. I am also interested in combine machine learning (ML) and PL - using ML to solve PL problems, and vice versa.

Test input generators are an important part of property-based testing (PBT) frameworks. Because PBT is intended to test deep semantic and structural properties of a program, the outputs produced by these generators can be complex data structures, constrained to satisfy properties the developer believes is most relevant to testing the function of interest. An important feature expected of these generators is that they be capable of producing all acceptable elements that satisfy the function’s input type and generator-provided constraints. However, it is not readily apparent how we might validate whether a particular generator’s output satisfies this coverage requirement. Typically, developers must rely on manual inspection and post-mortem analysis of test runs to determine if the generator is providing sufficient coverage; these approaches are error-prone and difficult to scale as generators become more complex. To address this important concern, we present a new refinement type-based verification procedure for validating the coverage provided by input test generators, based on a novel interpretation of types that embeds “must-style” underapproximate reasoning principles as a fundamental part of the type system. The types associated with expressions now capture the set of values guaranteed to be produced by the expression, rather than the typical formulation that uses types to represent the set of values an expression may produce. Beyond formalizing the notion of coverage types in the context of a rich core language with higher-order procedures and inductive datatypes, we also present a detailed evaluation study to justify the utility of our ideas.

The Left Hand of Equals

Speaker: Andrew Black

When is one object equal to another object? While object identity is fundamental to object-oriented systems, object equality, although tightly intertwined with identity, is harder to pin down. The distinction between identity and equality is reflected in object-oriented languages, almost all of which provide two variants of "equality", while some provide many more. Programmers can usually override at least one of these forms of equality, and can always define their own methods to distinguish their own objects. This essay takes a reflexive journey through fifty years of identity and equality in object-oriented languages, and ends somewhere we did not expect: a "left-handed" equality relying on trust and grace.

Name binding in real life: a beginner’s report on the philosophy of language

Speaker: Katie Casamento

I'm a Senior Instructor in Computer Science at Portland State, usually lecturing on things like programming language theory, formal methods, and software maintenance. I finished my MS at Portland State in 2019, which included a thesis on verified typechecking in languages with complex scoping. Agda is my favorite puzzle game. In my recent free time, I've been hacking on a TI-83+ emulator in Rust, playing old video games, and trying to get outside more.

A few years ago, during my MS degree, I took an intro-level Philosophy of Language course from Dr. Avram Hiller in the PSU Philosophy department. It was a great course and I think I still remember some of it. This very informal talk will cover my experience as a PL person stepping outside my comfort zone into a field that feels both familiar and foreign: the semantics of natural language, specifically "how proper nouns work". I'll discuss some historical questions, debates, and proposals in this area, all of which I only half-understand at best, and I'll try to relate them back to my much more confident understanding of how names work in programming languages. I hope you'll come away from the talk feeling motivated to learn more about this topic from someone more knowledgeable about it than me.

The Persistence of Past: A Demand Semantics for Mechanized Cost Analysis of Lazy Programs

Speaker: Laura Israel

Laura Israel is a first-year doctoral student at Portland State University studying formal verification with Yao Li. She has a particular interest in complexity theory and its formalization in proof assistants. Laura developed a passing interest in theoretical CS while getting her BA in Psychology at Reed College, resulting in a stint in the tech industry, then culminating in her current research at PSU. When she's not doing math thinly-veiled as computer science, you can find her hanging out with her cat Socks, running Dungeons and Dragons, or writing (and occasionally publishing) short stories.

Lazy evaluation is a powerful tool that enables better compositionality and potentially better performance in functional programming, but it is challenging to analyze its computation cost. Existing works either require manually annotating sharing, or rely on separation logic to reason about heaps of mutable cells. In this paper, we propose a bidirectional demand semantics that allows for reasoning about the computation cost of lazy programs without relying on special program logics. To show the effectiveness of our approach, we apply the demand semantics to formally prove that Okasaki's banker's queue is both amortized and persistent using the Coq theorem prover. We also propose the reverse physicist's method, a novel variant of the classical physicist's method, which enables mechanized, modular and compositional reasoning about amortization and persistence with the demand semantics.