Spring 2023 Seminars

Spring 2023

Organizer: Yao Li

All Talks

Date Title Speaker
Building a Verified Software Toolchain in Iris William Mansky
Demand-Driven Symbolic Execution for Functional Languages Shiwei Weng
What is the correct correctness specification for a typechecker? Katie Casamento
(Title Missing) Bart Massey
Comprehending the Power of Abstract Syntax Yao Li
The dynamically-typed actor framework that probably shouldn’t exist Patrick Redmond
Deeper Shallow Embeddings Jacob Prinz

Building a Verified Software Toolchain in Iris

Speaker: William Mansky

Mansky has been an assistant professor of computer science at the University of Illinois Chicago since 2018. His areas of expertise are interactive theorem proving, program verification, and concurrency, and he is one of the maintainers of the Verified Software Toolchain (VST) for formally proving correctness of C programs. As a participant in NSF Expedition “The Science of Deep Specification”, he helped verify an HTTP web server and developed theory for connecting program verification systems to verified operating systems. His recent work also includes a verified messaging system for interprocess shared-memory communication, a framework for specifying the correctness of non-linearizable concurrent data structures, and the integration of concurrency verification features from the Iris framework into VST.

The Verified Software Toolchain (VST) is a separation-logic-based system for verifying C programs according to the semantics of CompCert, with a guarantee that properties proved will hold on the compiled code. Iris is a more modern, generic Coq-based verification system, with many points of overlap but dramatically different foundations, based on a generic notion of higher-order step-indexed resource algebras. In this talk, I will give a brief overview of both VST and Iris, and present work in progress on re-engineering VST to build on the foundations of Iris, allowing us to prove correctness of real-world C programs using Iris’s powerful tactics and concurrency support.

Demand-Driven Symbolic Execution for Functional Languages

Speaker: Shiwei Weng

I (Shiwei Weng) am a fifth-year Ph.D. student in JHU PL Lab, advised by Scott Smith [3]. My current research focuses on symbolic execution for functional languages. Besides, my interests aim to apply ideas of programming languages to other computer science areas. I am an active OCaml programmer and maintain z3-OCaml [4]. I got my bachelor's degree at Fudan University, China. I worked as a research intern at Microsoft Research for project Checked C [5] in summer 2021. I attended the Oregon PL Summer School last year and enjoyed the weather a lot. [3] https://www.cs.jhu.edu/~scott/ [4] https://opam.ocaml.org/packages/z3/ [5] https://www.microsoft.com/en-us/research/project/checked-c/

Symbolic execution has been an active area of research for almost 50 years. Symbolic **backwards** execution (SBE) is a useful variation on standard forward symbolic execution; it allows a symbolic evaluation to start anywhere in the program and proceed by executing in reverse to the program start. SBE brings goal-directed reasoning to symbolic execution and has proven effective in e.g. automated test generations. This work DDSE is presented at ICFP'20 [1]. Several projects in JHU PL Lab [2] are established on DDSE and under exploration, including: - Demand-driven Bounded-Model Checking for Functional Languages (led by Shiwei Weng) - Refutation-based Typechecking Using Symbolic Execution (led by Ke Earl Wu and just presented at NJPLS'23) - Integration Demand-Driven Program Analysis and Execution without Compiling to ANF (led by Robert Zhang) In the talk, I will present DDSE and hope to cover ongoing work. [1] https://pl.cs.jhu.edu/projects/demand-driven-symbolic-execution/papers/icfp20-ddse-full.pdf [2] https://pl.cs.jhu.edu/

What is the correct correctness specification for a typechecker?

Speaker: Katie Casamento

(Title Missing)

Speaker: Bart Massey

Comprehending the Power of Abstract Syntax

Speaker: Yao Li

The dynamically-typed actor framework that probably shouldn’t exist

Speaker: Patrick Redmond

I am a third year PhD student in the Languages, Systems, and Data Lab at the University of California Santa Cruz advised by Lindsey Kuper. I’m exploring the design, implementation, and verification of distributed systems, runtimes for pure functional languages, and how to put my industry experience to use in practical research.

Haskell is well known as an outlier among programming languages, and its runtime exceptions are no exception: It turns out that Haskell’s asynchronous exceptions can be used to communicate arbitrary data between threads! By viewing Haskell’s asynchronous exceptions as a communication primitive, we find a message-passing actor system built-in to GHC’s runtime. This talk will guide the intermediate Haskell programmer, who might not be so familiar with the variety of exceptions in Haskell, through an encoding of message passing via exceptions, and poke a bit of fun at our favorite functional language.

Deeper Shallow Embeddings

Speaker: Jacob Prinz

Jacob Prinz is a PhD student in the PLUM group at the University of Maryland advised by Leonidas Lampropoulos. Jacob's research interests are in dependently typed metaprogramming and verification.

Deep and shallow embeddings are two contrasting techniques for embedding a language in a host language with complementary strengths and weaknesses. In a deep embedding, embedded constructs are defined as data in the host: this allows for syntax manipulation, but is challenging to implement for complicated type systems. In a shallow embedding, by contrast, constructs are encoded using features of the host: this makes them simple to implement, but limits their use in practice. I will present our paper "Deeper Shallow Embeddings", where we attempt to bridge the gap between the two by presenting a general technique for extending a shallow embedding of a type theory with a deep embedding of its typing derivations. These embeddings are almost as straightforward to implement as shallow ones, but come with capabilities traditionally associated with deep ones.