Participant Lectures
| Date | time | Lecturer | Insitution | abstract |
|---|---|---|---|---|
| TUE 6/24 | 8:30PM | Johannes Hostert | ETH Zurich |
The Rust programming language is well known for its ownership-based type system,
which offers strong guarantees like memory safety and data race freedom.
However, Rust also provides unsafe escape hatches,
for which safety is not guaranteed automatically and must instead be manually upheld
by the programmer.
This creates a tension. On the one hand, compilers would like to exploit
the strong guarantees of the type system – particularly those pertaining
to aliasing of pointers—in order to unlock powerful intraprocedural optimizations.
On the other hand, those optimizations are easily invalidated by "badly behaved" unsafe code.
To ensure correctness of such optimizations, it thus becomes necessary
to clearly define what unsafe code is "badly behaved."
In prior work, external pageStacked Borrows defined a set of rules achieving this goal.
However, Stacked Borrows rules out several patterns that turn out to be common
in real-world unsafe Rust code, and it does not account for advanced features
of the Rust borrow checker that were introduced more recently.
To resolve these issues, we present Tree Borrows. As the name suggests, Tree Borrows is defined by replacing the stack at the heart of Stacked Borrows with a tree. This overcomes the aforementioned limitations: our evaluation on the 30,000 most widely used Rust crates shows that Tree Borrows rejects 54% fewer test cases than Stacked Borrows does. Additionally, we prove (in Rocq) that it retains most of the Stacked Borrows optimizations and also enables important new ones, notably read-read reorderings. |
| 9:00PM | ||||
| 9:30PM | Balasz | LMU Munich | Superposition is an efficient proof calculus for reasoning about first-order logic with equality that is implemented in many automatic theorem provers. It works by saturating the given set of clauses and is refutationally complete, meaning that if the set is inconsistent, the saturation will contain a contradiction. We restructured the completeness proof to cleanly separate the ground (i.e., variable-free) and nonground aspects, and we formalized the result in Isabelle/HOL. We relied on the IsaFoR library for first-order terms and on the Isabelle saturation framework. | |
| 10:00PM | Dustin Juliano | Indiana University Indianapolis |
Formal Artificial Intelligence (Formal AI) is an effort
to represent AI directly in the form of human-readable source code and data.
This research direction is primarily intended
to address safety and security concerns related to AI
by establishing correspondences to programming language theory and type theory.
Well-typed computer programs and their accompanying data would constrain the behavior of AI,
enabling reliability, trust, and control.
This approach, however, has numerous open problems that will require a multi-disciplinary effort,
and this talk focuses on those challenges and attempts to initiate this new field.
slides |
|
| THR 6/26 | 8:30PM | JJ | University of British Columbia |
Toki Pona (lit. the language of good) is a constructed, artistic language,
collaboratively designed and iterated upon by its speakers throughout the early 2000s.
The language has since grown, and today it is spoken by a scattered community
of several thousand, primarily centred around online forums and chatrooms.
Toki Pona is minimalist -- consisting of 14 phonemes, 140 core words, a small number of grammatical rules, and no inflectional morphology. This sheer minimalism raises the question: how does Toki Pona function as a *language*? How are speakers able to adequately communicate with each other? How can *meaning* be derived from such a limited set of words? In this presentation, I will discuss the language and community, discuss the principles behind Toki Pona (and language more broadly) that allow it to function in the way it does, and (briefly) teach how to read and speak it. |
| 9:00PM | Claire Wang | University of Pennsylvania |
DJ Set
Rocq N' Roll (currently work in progress) is an interactive tool that allows a user to step through a rocq proof and listen to their proofs given a MIDI input device. We will have a quick explanation on how the tool works, a short live demo, and then feedback. We can also go through ways to sonify proofs so that attendees can start building their own proof sounds. The tool is a way to explore the following questions:
|
|
| 9:30PM | Bartłomiej Królikowski | Uniwersytet Wrocławski |
Algebraic Effects are a way to present effectful behaviour of programs
in a unified manner and together with handlers they provide high expressivity
and allow for more modular programming. Dependent types, on the other hand,
are a fundamental feature of proof assistants and allow for strong specification of programs.
In our work, we try to combine algebraic effects with Calculus of Constructions
to achieve a fully functional proof assistant that could also serve
as a general purpose language.
As an intermediate step we design a classical Calculus of Constructions,
where classicality is provided by the call/cc operator.
During the presentation we will discuss complications arising in the process
and see some rules of the type-and-effect system, together with subtyping
and reduction relation of that language.
slides |
|
| TUE 7/1 | 8:30PM | Julian Haas | TU Darmstadt | LoRe: Reasoning about Safety and Consistency in Local-First Software
The "Local-First Software" movement calls for distributed applications that move data processing from the cloud back to local user devices. This allows for applications that work offline and preserve user privacy while still enabling collaboration and data synchronization. Unfortunately, the distributed and asynchronous nature of such applications makes them hard to reason about and existing programming models provide little to no support for verification. We propose LoRe, a programming language and compiler that automatically verifies developer-supplied safety properties for local-first applications. LoRe combines the declarative data flow of reactive programming with static analysis and verification techniques to precisely determine concurrent interactions that violate safety invariants and to selectively employ strong consistency through coordination where required. We introduce a formalized proof principle and demonstrate how to automate the process in a prototype implementation that outputs verified executable code. |
| 9:00PM | Arjun Vedantham | University of California, Santa Cruz |
Software defined radio (SDR) allows for greater flexibility
in signal processing pipelines when compared to discrete hardware components.
While even general purpose SDR hardware is capable of performing some functions
on its own, in practice much of the decoding and processing workload
falls to traditional CPUs as part of this flexibility/specialization tradeoff.
Our language Zinnia combines the flexibility of SDR systems with the higher processing throughput offered by FPGAs and reconfigurable hardware fabrics. In this talk, I'll talk about building Zinnia as a class project, interacting with the Calyx hardware IR, and discussing the state of hardware tooling (and opine about how PL research can make it better). |
|
| 9:30PM | Hongyi Ling | ETH Zurich | Many program verification tools are organized into a front-end, which encodes an input program along with its specification and verification logic into an intermediate verification language (IVL), and a back-end, which computes proof obligations from the IVL program and discharges them, using an SMT solver for example. We identify potential unsoundness of the encoding from front-ends into IVLs arising from mismatches between front-end and IVL state models, propose backward satisfiability as a sufficient property for soundness, and based on this property, build a general framework for proving the soundness of encodings from front-ends into IVLs. Our framework is able to deal with general concurrent separation logic based front-ends with various state models and operational semantics. Although we choose Viper as the IVL in our work, the idea behind our framework is applicable to other IVLs as well. | |
| 10:00PM | Slim Lim | Baseball is a game of immense conceptual depth, but tragically mis-marketed and hence misunderstood by most OPLSS attendees. In this talk, I explain the appeal of baseball from first principles, and provide an overview of key concepts and rules of gameplay. This talk assumes no preexisting knowledge and is ideal for those with indifferent-to-negative attitudes regarding baseball. | ||
| THR 7/3 | 8:30PM | Kartik Sabharwal | University of Iowa | We will discuss some of the key ideas behind boolean satisfiability (SAT) and satisfiability modulo theories (SMT) solvers. We will begin with a quick review of propositional and first-order logic so that we may properly define a 'theory' in the context of SMT. Once we have a clear idea of the problem we will familiarize ourselves with abstract conflict-driven clause learning (CDCL(T)). We will then discuss how abstract CDCL(T) compares with its concrete implementation in the SMT solver cvc5. |
| 9:00PM | Amelia Dobis | Unified Deductive Hardware Verification | ||
| 9:30PM | Ricardo Aguilera | Introduction to the logical paradoxes — a zoo of paradoxes and the logical developments inspired by them in philosophy. | ||
| 10:00PM | Jiaqui We |
Human spoken languages, like English, are often ambiguous and not formalized.
Lojban is an attempt to construct a formalized human spoken language
that aims to be logical and flexible yet unambiguous and simple.
Founded nearly 40 years ago, Lojban has developed into a living language
spoken by thousands around the world, maintained by community,
and has been demonstrated in translation and in original works of prose and poetry.
In this introductory talk, we will briefly cover the pronunciation, grammar, basic vocabulary and formalization of Lojban. We will also illustrate how to express everyday conversation, logical predicate and even figurative literature in Lojban. |