University of Oregon University of Oregon

Types, Semantics, and Program Reasoning

June 20-July 2, 2022

Technical Lectures

The sessions are non-overlapping, so participants will have the opportunity to attend all lectures. Each lecture is 80 minutes, including time for questions.

Lectures are held in 175 Knight Law Center.
Participant talks are held in 220 Deschutes Hall.
Session 1 is 9:00 AM until 10:20am.
Session 2 is 10:40 AM until noon.
Session 3 is 2:00 PM until 3:20 PM.
Session 4 is 3:40 PM until 5:00 PM.
Evening Session is 8:00pm.

Morning Afternoon Evening
Date Session 1 Session 2 Session 3 Session 4
MON 6/20 Pfenning Altenkirch Gibbons Curien
TUE 6/21 Pfenning Altenkirch Gibbons Curien Participant Talks
WED 6/22 Pfenning Altenkirch Gibbons Curien
THR 6/23 Pfenning Altenkirch Gibbons Curien Participant Talks
FRI 6/24 Pfenning Altenkirch Ghilezan Downen
SAT 6/25 Ghilezan Downen Ghilezan Downen Participant Talks
SUN 6/26 Free
MON 6/27 Downen Weirich Chlipala Zdancewic
TUE 6/28 Lindley Weirich Chlipala Zdancewic Participant Talks
WED 6/29 Lindley Weirich Chlipala Zdancewic
THR 6/30 Lindley Weirich Balzer Harper Participant Talks
FRI 7/1 Harper Balzer Lindley Balzer
SAT 7/2 Harper Balzer Harper

Participant Talks

Participants are encouraged to share their current research. Participant Talks are used to create interest around your research. Talks about unfinished research or future directions are encouraged. To schedule a talk, email jallen@cs.uoregon.edu.

The building is locked at night, so please be prompt or you will not be able to enter the building.

Date Time Presentor Title
TUE 6/21 8:00PM Breandan Considine

Type arithmetic over finite fields via compile-time code generation

In this talk, we will present a method for embedding dependent types in parametrically-polymorphic languages, inspired by an ancient tool: the abacus. Code written in our embedded language is capable of performing bounded type-level arithmetic over Galois fields GF(2n) and other bases, which may be used to design combinational circuits and simple finite state machines. Our representation is directly translatable to various backends, including SAT/SMT for program synthesis and VHDL for behavioral synthesis. We will discuss its concrete implementation and some techniques for emulating advanced type-level features like nested datatypes and higher-kinded types in blue-collar languages like Java and Kotlin. Finally, a live demo will be given featuring compile-time type inference. No prior experience is assumed or required.

9:00PM Jean-Charles Belouard

Introducing Absolutely Distributed Organizations

In this talk we introduce the concept of an Absolutely Distributed Organization (ADO), in the field of collective work, and its junction with programming languages. The purpose of an ADO is to produce (at least) a documentation, a model and an autonomous organization for a group of people with a specific recurring task. We will cover the constraints and advantages of the system, a long with the major themes of the architecture: literate programming, recursion, autonomy and distributivity. Finally, we will open the conversation to this question: "how to generalize and optimize the modeling of work procedures inside a programming language?" The talk is resolutely interdisciplinary and absolutely everyone is welcome to share their thoughts on the matter.

9:30PM Sander Huyghebaert

Universal Contracts Approach for Semi-Automatic Verification of ISA Security Guarantees

Where ISA specifications used to be defined in long prose documents, we have recently seen progress on formal and executable ISA specifications. However, for now, formal specifications provide only a functional specification of the ISA, without specifying the ISA's security guarantees. In this talk, we present a novel, general approach to specify an ISA's security guarantee in a way that

  1. can be semi-automatically validated against the ISA semantics, producing a mechanically verifiable proof,
  2. supports informal and formal reasoning about security-critical software in the presence of adversarial code.

Our approach is based on the use of universal contracts: software contracts that express bounds on the authority of arbitrary untrusted code on the ISA. We semi-automatically verify these contracts against existing ISA semantics implemented in Sail using our Katamaran tool: a verified, semi-automatic separation logic verifier for Sail. We illustrate our approach with two case studies: a minimal custom-built capability machine for which we prove capability safety and RISC-V with the Private Memory Protection (PMP) extension for which we prove a memory integrity property. We believe our approach has the potential to redefine the formalization of ISA security guarantees and we will sketch our vision and plans.

THR 6/23 8:00PM Abel Nieto Rodriguez

Modular Verification of Commutative Replicated Datatypes in Separation Logic

Commutative Replicated Data Types (CRDTs) are a family of distributed data structures where all operations are designed to commute, so that replica states eventually converge. Additionally, CRDTs require that operations be propagated between replicas in causal order. This talk presents a framework for verifying safety properties of OCaml CRDT implementations using separation logic. The framework consists of two libraries. One implements a Reliable Causal Broadcast (RCB) protocol so that replicas can exchange messages in causal order. A second OpLib library then uses RCB to export a CRDT builder interface that simplifies the creation (and correctness proofs) of new CRDTs. OpLib allows clients to implement new CRDTs as purely-functional data structures, without having to reason about network operations, concurrency control and mutable state, and without having to re-implement causal broadcast each time. Using OpLib, we have implemented 10 sample CRDTs from the literature, including multiple versions of replicated registers and sets, as well as two CRDT combinators for products and maps. Our proofs are conducted in the Aneris distributed separation logic.

8:30PM Peio Borthelle

Formalizing operational game semantics via abstract machines and coinduction

Game semantics is a style of denotational models where types are interpreted as two-players games, expressing a dialogue between a term and its context. Terms are then interpreted as strategies. Their motivation is to build fully-abstract models — that is models capturing contextual equivalence — scaling to languages with side-effects and rich type systems.

Game semantics have traditionally been computed by induction on typing derivation of terms. On the other hand, operational game semantics constructs strategies by interleaving operational reduction and emission of interactions. This can be seen as incorporating interactions into abstract machines. Their equivalences can be related to normal form bisimulations on the corresponding labelled transition system.

In this talk, I will present ongoing work on formalizing these games for a simply-typed call-by-value lambda-calculus with general recursion and positive datatypes. The formal development is done in Coq, using some form of interaction trees on indexed containers/dependent polynomial functors. These theoretical tools are instrumental in achieving an intrinsically-typed style.

9:00PM Jialu Bao (Zoom)

Data-Driven Invariant Learning for Probabilistic Programs

Morgan and McIver’s weakest pre-expectation framework is one of the most well-established methods for deductive verification of probabilistic programs. Roughly, the idea is to generalize binary state assertions to real-valued expectations, which can measure expected values of probabilistic program quantities. While loop-free programs can be analyzed by mechanically transforming expectations, verifying loops usually requires finding an invariant expectation, a difficult task. But we can also view invariant expectation synthesis as a regression problem: given an input state, predict the average value of the postexpectation in the output distribution. This perspective guides us towards a data-driven invariant synthesis method for probabilistic programs. In this talk, we will explain this approach in more detail and demonstrate its effectiveness on a variety of benchmarks from the probabilistic programming literature.

9:30PM Alex Gu (Zoom)

Synthesizing Object Models from Natural Language Specifications

Program synthesis has traditionally excelled in tasks with precise specifications such as input-output examples and formal constraints by using structured and algorithmic approaches based on enumerative search and type inference. However, traditional synthesis techniques have no mechanism of incorporating real-world knowledge, which is commonplace in software engineering. Motivated by this, we introduce a new synthesis task known as specification reification: synthesizing concrete realizations of vague, high-level application specifications. We focus on a specific instance of this: generating object models from natural language application descriptions. Towards this goal, we present preliminary work in object model synthesis leveraging domain knowledge with GPT-3.

SAT 6/25 8:00PM Spencer Baugh

Adding Rich Type Information to the Linux syscall API

The Linux syscall API is largely untyped and unsafe. This makes it hard to use Linux operating system functionality in a safe way. The traditional solution is to laboriously write safe syscall wrappers by hand in one's language of choice, but most Linux functionality has no such safe wrapper in any language.

Instead, we can work upstream in Linux to create rich type information for the syscall API in a language-independent way, then generate safe and idiomatic syscall wrappers in each language using that information.

Syscalls have complex behavior, so the right way to express this type information is not clear. I will discuss the motivation for this project and the issues that it faces, and a few options for how to carry it out. This project is in early stages, and I welcome suggestions.

Zoom recording (passcode: &1a@n9#2)

8:30PM Jonathan Chan

A Syntactic Model of Sized Dependent Types

Contemporary proof assistants based on dependent type theories must restrict nonterminating recursive functions to ensure logical consistency of the type theory and decidability of type checking. This is done via guard predicates that only allow functions that are structurally recursive and that recur only on syntactically smaller arguments. However, guard predicates are too restrictive and reject functions that aren't structurally recursive but are obviously terminating, creating extra work for the programmer to convince the guard checker.

An alternative is sized types, a type-based termination checking method where inductively-defined types are annotated with sizes. Type checking guarantees that functions recur only on arguments whose types have smaller sizes, rather than on arguments that syntactically appear smaller, allowing more terminating functions to be accepted. Unfortunately, models of sized dependent type theories fail to support pragmatic features such as higher-rank size quantification, which allows for passing around size-preserving functions, and bounded size quantification, which eliminates the need for complex monotonicity checks required by prior sized type systems.

I present a sized dependent type theory with higher-rank and bounded sizes (STT), and prove its logical consistency with a syntactic model: by compiling STT into the Extensional Calculus of Inductive Constructions (CICE), a variant of the type theory on which Coq is based, and showing that this translation is type preserving, the consistency of STT follows from the consistency of CICE.

TUE 6/28 8:00PM Kartik Singhal

Q# as a Quantum Algorithmic Language

Q# is a standalone domain-specific programming language from Microsoft for writing and running quantum programs. Like most industrial languages, it was designed without a formal specification, which can naturally lead to ambiguity in its interpretation. We aim to provide a formal language definition for Q#, placing the language on a solid mathematical foundation and enabling further evolution of its design and type system. This paper presents λ-Q#, an idealized version of Q# that illustrates how we may view Q# as a quantum Algol (algorithmic language). We show the safety properties enforced by λ-Q#’s type system and present its equational semantics based on a fully complete algebraic theory by Staton.

8:30PM Jacob Prinz

Deeper Shallow Embeddings

Deep and shallow embeddings are two popular 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 and facilitates metatheoretic reasoning, but is challenging to implement— especially in the case of dependently typed embedded languages. In a shallow embedding, by contrast, constructs are encoded using features of the host: this makes them quite straightforward to implement, but limits their use in practice.

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. Such embeddings are almost as straightforward to implement as shallow ones, but come with capabilities traditionally associated with deep ones. We demonstrate these increased capabilities in a number of case studies; including a DSL that only holds affine terms, and a dependently typed core language with computational beta reduction that leverages function extensionality.

9:00PM Nabil Hassein

Arabic-based programming languages and communities

Mainstream programming languages have been dominated for decades by Latinate character sets and English-inspired syntax, including in cases when they emerge from linguistically far different settings like Japan (e.g. Ruby) or Brazil (e.g. Lua), notwithstanding multilingual precedents at least as early as the 1960s' ALGOL supporting other scripts and languages such as Cyrillic/Russian. The practical obligation to learn English or another European language in order to participate in programming at even the most basic level — including to read documentation or ask for help online, beyond the relatively superficial matter of syntax — contributes to the ongoing Western dominance of computing at the expense of broad participation in the field, even as it increasingly structures the lives of the global majority, and despite many rich traditions of mathematical and algorithmic thought indigenous to other cultures and languages, including Arabic. In this mostly non-technical talk, I will review what I have found so far in my early-stage research on existing work on Arabic-based programming languages, consider some of the social challenges standing in the way of their widespread adoption, and speculate on the potential of applying techniques like compiler bootstrapping to create a more fully Arabic circuit of computing than is currently extant to my knowledge.

9:30PM Stephen Mell

Computation Beyond Functions and Syntax Beyond Trees: A Calculus on Graphs (Work in Progress)

Motivated by the canonicity of types and programs and the representation of complex data structures, we introduce a calculus whose types and terms both possess graph structure. The graph structure on types provides canonicity and generalizes both product and (linear) function types. The graph structure on terms avoids unwanted equivalences while still allowing for an operational semantics analogous to beta reduction. The calculus is closely related to polymorphic multiplicative exponential linear logic. In this talk, we outline the types, terms, and operational semantics of our calculus.

THR 6/30 8:00PM Molly Pan

A Mechanized Formalization of P4: Language and Verification

As network traffic grows in volume and diversity, it’s increasingly important for operators to identify and understand what’s happening inside the network. For example, operators may want to log heavy downloaders regularly, rate-limit large flows, or drop unsolicited incoming packets. However, programming in the existing data plane languages like P4 is difficult. The P4 Language Specification can be ambiguous, the compilers can differ in intended or unintended ways, domain-specific constructs can introduce subtle bugs — and the language itself is not always intuitive to program in. To address those issues, we have built machine-processable specifications, proofs, and tooling, strictly compliant with the language specification, that can output accurate answers to P4 test cases and corner cases, can rule out "undefined behavior'', and allows users to prove the correctness of P4 programs with respect to high-level specifications. We present a mechanized complete formalization of P4, including its abstract syntax, operational semantics, type system, reference interpreter, and program logic for proving correctness of P4 programs. We developed our formal semantics to closely track the P4 specification; in the process we corrected many ambiguities in the P4 document (in consultation with the language steering committee). To allow general users to take advantage of our system, we are developing a library of formally verified P4 data structures. We are also designing a high-level programming language, which gets compiled into P4 depending on our data structure library, opening the opportunity of automatic proof of the generated programs.

8:30PM Mohit Tekriwal

Formal Verification of Convergence of Numerical Solutions of Differential Equations

Differential equations are used throughout science and engineering to model and predict the behavior and performance of aircraft, cars, trains, robots, chemical power plants, the stock exchange, and many more. For example, the aerodynamics of an airplane can be represented by the Navier-Stokes equations; the Riccati differential equation is encountered in the problems of optimal control; and the Black-Scholes equation is a partial differential equation that is used to model valuation of stock options in mathematical finance. Differential equations are thus pervasive in almost every aspect of science and engineering, and being able to solve those differential equations precisely and accurately, but also while trusting that the solutions are accurate, is of utmost importance.

Solving these differential equations analytically is often intractable. Therefore, these equations are solved numerically by discretizing the continuous system in a finite computational domain. We thus obtain approximations of the exact or the analytical solution. In this process of numerical computation, we incur many errors: discretization errors due to computation in a finite computational domain, floating point errors due to finite precision, and other forms of errors that depend on the methods used for solving the discretized system of equations. To certify the quality of numerical solutions, we need to reason about the errors in a formal or rigorous manner. We therefore formalize the mathematics of numerical methods using the Coq theorem prover. We state these mathematical properties as a theorem in Coq and prove them formally by exploiting recent developments in real arithmetic, real analysis [the Coquelicot library in Coq], linear algebra [the mathcomp library in Coq]. We are currently working on an end-to-end verification of numerical programs by incorporating rounding error analysis in our verification framework.

9:00PM Jaiwei Chen

Robotics Verification with Synchronous Programming and Refinement Types

Robots, industrial automation, and other cyber-physical systems are seeing increasing adoption in many diverse fields. Due to their interactions with the physical world and the nature of the applications in which they are often deployed, they often need to be held to stringent safety standards. Formal verification is employed when rigorous safety guarantees are required in such systems, but conventional methods often require complex or error-prone translation between the implementation layer and the verification layer. We introduce a synchronous programming language that enables system modeling, formal verification, and execution. Our design leverages the properties of synchronous programs to reason temporally on programs destined for robots and other embedded systems.

9:30PM Nishant Kheterpal

Automating Geometric Proofs of Collision Avoidance with Active Corners

Avoiding collisions between obstacles and vehicles such as cars, robots or aircraft is essential to the development of automation and autonomy. To simplify the problem, many collision avoidance algorithms and proofs consider vehicles to be a point mass, though the actual vehicles are not points. In this paper, we consider a convex polygonal vehicle with nonzero area traveling along a 2-dimensional trajectory. We derive an easily-checkable, quantifier-free formula to check whether a given obstacle will collide with the vehicle moving on the planned trajectory. We apply our method to two case studies of aircraft collision avoidance and study its performance.

10:00PM Enzo Aldal

ZenSheet project update

ZenSheet is an experimental live programming environment that generalizes the core functionality of spreadsheets with modern programming language concepts. The aim of the project is to realize a computing environment amenable to a wide spectrum of users - particularly suitable for computing education. The presentation will illustrate the evolution of the project, design choices made (and discarded) along the way, and current challenges. ZenSheet has been demonstrated at conferences, including SPLASH 2017, OPLSS 2018, and Lambda Days 2020.