Jump To Semester:
Schedule (Fall 2023)
Below is a list of seminar dates for with information on the speakers:
Flèche: Incremental processing of rich proof documents
Time: Sep 1, Friday, 10:30 – 11:30 AM, Boston Time
Speaker: Emilio Jesús Gallego Arias (IRIF)
In-person Location: CDS 1001
Abstract: The field of interactive theorem proving has achieved significant milestones in the last decades, including the formal verification of complex mathematical theorems and programs such as the Feit-Thompson theorem for the classification of finite groups, the 4 color theorem, or the CompCert optimizing C compiler.
On the other side, the complexity and volume of mathematical knowledge and software is scaling exponentially, making the challenge of manual organization and verification of such knowledge harder by the day.
Interactive proof assistants can help tackle this problematic by encoding program specifications and mathematics in a way that allows to both organize and verify them with computer help. Due to this, interest in ITP tools such as Coq, Lean, or Isabelle has seen a huge rise of popularity among mathematicians and computer scientists aiming to validate their results.
Unfortunately, the gap between regular mathematical practice and the way interactive theorem provers work is large. We think it is safe to state that ITP systems do remain hard to use, which remains a thick barrier for widespread adoption.
Causes for this steep learning curve are various, ranging from cultural differences among research communities, to the hardness of programming featureful interactive proof assistants, which need complex IDEs that go beyond from these used in more traditional programming settings.
In this talk we will present Flèche, a new engine for the incremental validation of rich, hybrid documents.
Flèche is based on our work in jsCoq and SerAPI for the Coq system over the last 8 years, and in the experience of similar systems, which has allowed us to collect a set of requirements more in the HCI tradition, and a set of hardships more in the software engineering one.
At the core of Flèche is the notion of rich, hybrid proof document, that can freely intermix natural language, informal mathematical definitions, and formal mathematical vernaculars.
Document evolution and interaction is at the center of Flèche’s design, providing incremental validation of incomplete documents, and a rich view of document data and meta-data, which supports the common non-linear, refinement editing used by many scientists.
Implementing a system like Flèche is complex for several reasons, in particular due to incremental computing and several needs related to effects and programmable error recovery. A naïve implementation will quickly face maintainability and code size issues. Our solution to these implementation issues is based on the combination of two known techniques: stacks of interpreters, and algebraic effects.
This combo has proved to be very effective in practice, allowing us to have a small, modular implementation, where the different layers and features compose in a natural lightweight manner.
While Flèche is designed to be reusable by different systems, our first release is based on the Coq system combined with Myst Markdown.
We have successfully used Flèche to implement coq-lsp, a fully functional language server and VS Code client for Coq that provides many new features, and jsCoq 2, a new version of jsCoq with advanced literate programming facilities.
Bio: Emilio J. Gallego Arias is a researcher in the Picube team at Inria Paris. Emilio’s background is in programming language semantics, functional programming, and program verification. Emilio is a member of the Coq development team, and enjoys proving lots of stuff with it!
These days he is mostly interested in improving the usability and accessibility of foundational interactive theorem provers.
Formalizing Algorithmic Bounds in the Query Model in EasyCrypt
Time: Sep 5, Tuesday, 12:30-1:30 PM, Boston Time
Speaker: Alley Stoughton (Boston University)
In-person Location: CDS 1001
Abstract: We use the EasyCrypt proof assistant to formalize the adversarial approach to proving lower bounds for computational problems in the query model. This is done using a lower bound game between an algorithm and adversary, in which the adversary answers the algorithm’s queries in a way that makes the algorithm issue at least the desired number of queries. A complementary upper bound game is used for proving upper bounds of algorithms; here the adversary incrementally and adaptively realizes an algorithm’s input. We prove a natural connection between the lower and upper bound games, and apply our framework to three computational problems, including searching in an ordered list and comparison-based sorting, giving evidence for the generality of our notion of algorithm and the usefulness of our framework.
A Two-Level Linear Dependent Type Theory
Time: Sep 12, Tuesday, 12:30-1:30 PM, Boston Time
Speaker: Qiancheng Fu (Boston University)
In-person Location: CDS 1001
Abstract: We present a type theory combining both linearity and dependency by stratifying typing rules into a level for logics and a level for programs. The distinction between logics and programs decouples their semantics, allowing the type system to assume tight resource bounds. A natural notion of irrelevancy is established where all proofs and types occurring inside programs are fully erasable without compromising their operational behavior. Through a heap-based operational semantics, we show that extracted programs always make computational progress and run memory clean. Additionally, programs can be freely reflected into the logical level for conducting deep proofs in the style of standard dependent type theories. This enables one to write resource safe programs and verify their correctness using a unified language.
Memory access protocols: certified data-race freedom for GPU kernels
Time: Sep 26, Tuesday, 12:30-1:30 PM, Boston Time
Speaker: Tiago Cogumbreiro (UMass Boston)
In-person Location: CDS 1001
Abstract: GPUs offer parallelism as a commodity, but they are difficult to program correctly. Static analyzers that guarantee data-race freedom (DRF) are essential to help programmers establish the correctness of their programs (kernels). However, existing approaches produce too many false alarms and struggle to handle larger programs. To address these limitations we formalize a novel compositional analysis for DRF, based on memory access protocols. These protocols are behavioral types that codify the way threads interact over shared memory. Our work includes fully mechanized proofs of our theoretical results, the first mechanized proofs in the field of DRF analysis for GPU kernels. Our theory is implemented in Faial, a tool that outperforms the state-of-the-art. Notably, it can correctly verify at least 1.42× more real-world kernels, and it exhibits a linear growth in 4 out of 5 experiments, while others grow exponentially in all 5 experiments.
In this talk, Tiago presents the journal paper [1] and then gives a live demonstration of some of the new features of Faial.
1. https://link.springer.com/article/10.1007/s10703-023-00415-0
Bio: Tiago Cogumbreiro researches software verification with an emphasis on GPU programming. Tiago Cogumbreiro joined the Department of Computer Science at the University of Massachusetts Boston in fall 2018 as an assistant professor. Prior to that, Tiago was a postdoctoral researcher at the Georgia Institute of Technology and Rice University, supervised by Professor Vivek Sarkar, and a research assistant at Imperial College London, supervised by Professor Nobuko Yoshida. Tiago obtained a PhD from the University of Lisbon, Portugal.
GKAT with Indicator Variables, Fast Decompilation Verification
Time: Oct 3rd, Tuesday, 12:30-1:30 PM, Boston Time
Speaker: Cheng Zhang (Boston University)
In-person Location: CDS 1001
Abstract: Decompilation is not only a method to solve several practical problems, like binary analysis, binary migration, and binary optimization; it also gives us understanding of theoretical problems like the correspondence between structured and unstructured programs. Although plenty of works have been done in decompilations, and many automated tools has been developed. There are not as many tools that can verify the correctness of the decompilation result. Here we present a scalable algorithm based on techniques developed in Guarded Kleene Algebra with Tests (GKAT). This algorithm will decide the trace-equivalence between a flowchart and its decompiled program in a efficient manner, thus verifying the correctness of the decompilation process. This project is still on-going work.
Concurrent Tree Contracts
Time: Oct 17, Tuesday, 12:30-1:30 PM, Boston Time
Speaker: Hannah Gommerstadt (Vassar College)
In-person Location: CDS 1001
Abstract: A concurrent system is a system where multiple processes collaborate on a computation. A concurrent contract represents a property of the computation that should remain true throughout the computation. Monitors can be used to check at runtime that a computation adheres to its contract. My work uses session types to monitor concurrent contracts. This talk will focus on binary search trees, which are widely used in a concurrent setting, and have multiple interesting contracts (ordering, balance) to monitor.
A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability
Time: Oct 31, Tuesday, 12:30-1:30 PM, Boston Time
Speaker: Uğur Yavuz (Boston University)
In-person Location: CDS 1001
Abstract: 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).
Certificates for Probabilistic Pushdown Automata
Time: Nov 07, Tuesday, 12:30-1:30 PM, Boston Time
Speaker: Tobias Winkler (RWTH Aachen University)
In-person Location: CDS 1001
Abstract: Probabilistic pushdown automata (pPDA) are a natural model for programs with recursive first-order functions and discrete probabilistic choices. Applications of such programs include Bayesian machine learning, natural language processing, and the study of various infinite-state Markov processes.
Verification and model checking of pPDA have been extensively studied in the literature. Typical verification questions include “Is the probability to reach a bad configuration at most 0.99?” and “Does the pPDA terminate (= reach an empty stack) in finite expected time?”. Most existing works answer these questions by computing sufficiently precise numerical approximations of the sought-after probabilities and expectations.
A disadvantage of these approaches is a lack of explainability: It is not obvious that the results are actually correct, the user just sees a bunch of numbers that they are forced to trust. This is in stark contrast to, e.g., classic safety model checking where verification results are substantiated by further information such as a counter-example trace or an inductive invariant which can be checked independently. This additional information can be understood as a certificate that increases the trustworthiness of (potentially buggy) real-world implementations.
Local Structure Abstractions for Heap Commutativity
Time: Nov 14, Tuesday, 12:30-1:30 PM, Boston Time
Speaker: Jared Pincus (Boston University)
In-person Location: CDS 1001
Abstract: The program property of commutativity is analyzed or utilized in a growing body of theories and tools, including efforts in scalable concurrency, data structure design, security analysis, and parallelization. However, relatively few works have explored commutativity reasoning with a heap-based memory model.
We introduce local structure abstractions: a versatile family of abstractions, agnostic to concrete semantics, which adapt principles of separation logic and abstract interpretation to reason about operations on heap-allocated data structures. This technique overcomes weaknesses of typical strategies such as relational reasoning, and enables straightforward commutativity analysis in the abstract space, while capturing nondeterminism and observational equivalence for free. We share a mechanization of this formalism in Coq, which may be used to assist in verification and inference of commutativity conditions.
A Separation Logic for Negative Dependence
Time: Nov 21, Tuesday, 12:30-1:30 PM, Boston Time
Speaker: Jialu Bao (Cornell University)
In-person Location: CDS 1001
Abstract: Formal reasoning about hashing-based probabilistic data structures often requires reasoning about random variables where when one variable gets larger (such as the number of elements hashed into one bucket), the others tend to be smaller (like the number of elements hashed into the other buckets). This is an example of negative dependence, a generalization of probabilistic independence that has recently found interesting applications in algorithm design and machine learning. Despite the usefulness of negative dependence for the analyses of probabilistic data structures, existing verification methods cannot establish this property for randomized programs.
In this talk, I will present LINA, a probabilistic separation logic for reasoning about negative dependence. In the end, I will also briefly discuss some other interesting problems for probabilistic separation logics.
New methods for scalably reasoning about probabilistic systems
Time: Nov 28th, Tuesday, 12:30-1:30 PM, Boston Time
Speaker: Steven Holtzen (Northeastern University)
In-person Location: CDS 1001
Abstract: Probabilistic systems are notoriously difficult to reason about, but this doesn’t stop people from making them: machine learning practitioners and scientists make probabilistic models for reasoning about the world, and software developers use randomness in designing their algorithms. What are the principles for designing scalable systems and tools to aid in the development, verification, and application of probabilistic uncertainty across today’s software stack? In this talk I will discuss two ongoing efforts in our group that attack this problem. The first, reasoning-via-compilation, seeks to scalably automate probabilistic reasoning by compiling probabilistic systems into tractable representations that afford efficient reasoning. I will discuss ongoing efforts and successes in applying reasoning-via-compilation to scaling probabilistic inference and decision-making. The second approach I will discuss is a deductive approach that seeks to prove facts about programs by reasoning about their behavior within a new probabilistic separation logic we call Lilac. Ultimately, I hope to show you these two complementary approaches to probabilistic reasoning ought to be part of a cohesive foundation for future scalable systems for automated (or semi-automated) reasoning about uncertainty.
An Old Problem in Automata and Logic
Time: Dec 05th, Tuesday, 12:30-1:30 PM, Boston Time
Speaker: Howard Straubing (Boston College)
In-person Location: CDS 1001
Abstract: I will survey some recent (and some not-so-recent) progress on an old problem: In the 1990’s, it was shown (Barrington, Compton , Straubing, and Théren) that the regular languages definable by first-order sentences with no restrictions on the numerical predicates (i.e., the atomic formulas giving relations on the positions in a string) could be defined by sentences in which all these relations could themselves be computed by finite automata (the regular numerical predicates). More succinctly, regular languages require only regular numerical predicates in their logical definitions, proving a conjecture originally made by Robert McNaughton in 1960.
This simple-sounding characterization of first-order definable regular languages had to wait for advances in circuit complexity in order to be solved: it was finally proved by appeal to the theorem of Furst, Saxe and Sipser showing that the circuit complexity class AC0 cannot count the number of 1’s in an input string modulo any n>1. This led to a number of questions, which for the most part remain unsolved: First, does the property hold for logics other than first-order logic? For example, does it continue to hold for Sigma-k formulas, or for Boolean combinations of Sigma-k formulas, or for generalized first-order sentences containing modular counting quantifiers? Second, a somewhat more vague question: is there an ‘elementary’ proof of this fact about logic and automata, one that does not depend on circuit lower bounds? Such a proof for modular quantifiers would settle a long-standing open question about the circuit complexity class ACC. Much of the talk will be devoted to a 2020 paper (Borlido, Gehrke, Krebs, Straubing) giving such an elementary proof of the property for Boolean combinations of Sigma-1 sentences. I will also mention recent progress (Barloy, Cadilhac, Papeman, Zeume, LICS 2022) on establishing the property for Sigma-2 sentences, and older work by Hansen and Koucky suggesting that things are very differeent for modular quantifiers.
A Complete Implicit Formalism For Polynomial Time Over Inductive Datatypes
Time: Dec 12th, Tuesday, 12:30-1:30 PM, Boston Time
Speaker: Norman Danner (Wesleyan University)
In-person Location: CDS 1001
Abstract: In the 2010s, Dal Lago and collaborators settled an outstanding question from the earliest papers in implicit computational complexity theory: how to extend the tiered recurrence formalisms that are sound and complete for polynomial time over binary words to more complex data types such as trees? The difficulty arises because of the presence of sharing, which leads to “small” representations of values that appear “large” to the program, and the solution involves implementing recurrences in a memoizing fashion. Dal Lago et al.’s formalism is sound, but we argue that it is likely not complete. We then present a formalism that is sound and complete for polynomial time over inductive datatypes. This is joint work with Jim Royer (Syracuse University).
Schedule (Spring 2023)
Below is a list of seminar dates for with information on the speakers:
The Lambda Calculus – 40 Years Later
Time: Jan 20th, Friday, 3:00 – 4:00 PM Boston Time
Speaker: Giulio Manzonetto (LIPN)
In-person Location: CDS 1646
Abstract: Barendregt’s book “The Lambda Calculus, its syntax and semantics” (1981/84) has become a `classic’ in Theoretical Computer Science because it presents the state of the art in lambda calculus at that time in a comprehensive way. Moreover, a number of open problems and conjectures were proposed. In 2022, Barendregt and Manzonetto published a `sequel’ of this book, presenting the solutions of several of these problems, and more. In this talk, I will present a selection of these problems and the key ingredients that were employed to solve them.
A Compositional Theory of Linearizability
Time: Feb 3rd, Friday, 3:00 – 4:00 PM Boston Time
Speaker: Arthur Oliveira Vale (Yale University)
In-person Location: CDS 1646
Abstract: Compositionality is at the core of programming languages research and has become an important goal toward scalable verification of large systems. Despite that, there is no compositional account of linearizability, the gold standard of correctness for concurrent objects.
In this talk, I will discuss recent work in developing a compositional semantics for linearizable concurrent objects, and a few interesting results surrounding it. This compositional semantics is a consequence of first observing a common issue, which is independent of linearizability, in the construction of compositional models of concurrent computation: interaction with the neutral element for composition can lead to emergent behaviors, a hindrance to compositionality. Category theory provides a solution for the issue in the form of the Karoubi envelope. Surprisingly, and this is the main discovery of our work, this abstract construction is deeply related to linearizability and leads to a novel formulation of it. Notably, this new formulation neither relies on atomicity nor directly upon happens-before ordering and is only possible because of compositionality, revealing that linearizability and compositionality are intrinsically related to each other. We use this new, and compositional, understanding of linearizability to revisit much of the theory of linearizability, providing novel, simple, algebraic proofs of the locality property and of an analogue of the equivalence with observational refinement. We show our techniques can be used in practice by connecting our semantics with a simple program logic that is nonetheless sound concerning this generalized linearizability.
Bio: Arthur Oliveira is a 4th year Ph.D. candidate in Yale’s FLINT group working on mathematical models for computer systems with a focus on large-scale systems verification and compositionality.
Allegories of Symbolic Manipulations
Time: Feb 10th, Friday, 3:00 – 4:00 PM Boston Time
Speaker: Francesco Gavazzo (University of Pisa)
In-person Location: CDS 1646
Abstract: In the last decades, researchers have shown an increasing interest in developing mathematical theories of symbolic expressions, with the so-called mathematics of syntax having provided an impressive unifying account of (abstract) syntax in terms of initial algebras and free monads.
Symbolic syntax, however, is largely sterile without symbolic manipulation, namely that “symbol pushing” that makes symbolic reasoning and computation so effective.
Abstract rewriting is the discipline that studies symbolic manipulation per se, having at its conceptual heart a relational understanding of symbolic transformations. Its generality, however, is achieved by ignoring the syntactic structure of the expressions manipulated, this way making abstract rewriting ineffective when dealing with concrete formalisms and leading to a proliferation of ad hoc syntax-based theories of rewriting.
In this talk, I will show that a general relational theory of rewriting parametric with respect to, and accounting for, the syntactic structure of expressions can be given by extending the aforementioned mathematics of syntax from a categorical and algebraic basis to an allegorical and relational one.
Once formulated in the setting of allegory theory, the same notions of initial algebras, free monads, etc. used in abstract syntax provide all that is needed to define theories of symbolic manipulation for such syntax.
To maintain the talk as accessible as possible, I will not present the theory in its full generality; instead, I will follow a couple of concrete running examples and use them to first introduce the mathematics of syntax, and then move to the relational theory of symbolic manipulation in a concrete way, hinting to possible generalisation along the way.
Higher-Order Leak and Deadlock Free Locks
Time: Mar 03rd, Friday, 3:00 – 4:00 PM Boston Time
Speaker: Jules Jacobs (Radboud University)
In-person Location: CDS 1101
Abstract: [Joint work with Stephanie Balzer] Well-typed Rust programs are guaranteed to be memory safe and data-race free. Originally, Rust was also believed to be memory leak free, but there are well-typed programs that leak memory when using Rust’s shared memory concurrency APIs. This talk is about a step toward getting stronger guarantees by type checking: we present a linear type system for locks that guarantees leak and deadlock freedom. These locks are flexible in two ways: (1) they are first-class values that can be stored in data structures and passed around to other threads, (2) there is no restriction on the order of lock acquisition. Analogous to session types, the linear type system instead restricts the “sharing topology” to be acyclic. As an extension, we add lock orders to allow some well-behaved circular dependencies, and prove in Coq that all well-typed programs are leak and deadlock free.
Towards an observational Coq
Time: Mar 17th, Friday, 3:00 – 4:00 PM Boston Time
Speaker: Loïc Pujet (Inria)
In-person Location: CDS 1101
Abstract: The Coq proof assistant is based on a dependent type theory, the Calculus of Inductive Constructions (CIC). This theory plays both the role of a programming language with a very expressive type system, and that of a framework for constructive mathematics.
However, reasoning in the CIC is not always straightforward: if we try to manipulate higher-order objects, e.g. functions or predicates, we quickly run into the fact that Coq’s equality type does not support many extensionality principles — for instance, we cannot prove that the functions n -> n+2 and n -> 2+n are equal without having to extend the theory with axioms. Another severely limiting consequence of this lack of extensionality is that we cannot form quotient types without encoding them in complicated ways.
In this talk, I will present joint work with Nicolas Tabareau, which aims at integrating the observational equality of Altenkirch and McBride to the theory of Coq. This results in a system that supports the previously mentioned extensionality principles, while preserving the correspondence between proofs and programs and the good properties that come with it (canonicity, decidability of typing, normalization…). After a bit of exposition, I will go over the complex parts of the CIC (the impredicative propositions and the indexed inductive types) and how they interact with the observational equality.
Most of the results that I will present have been formalised in Agda and Coq.
Languages with Decidable Learning: a Meta-theorem
Time: Mar 24th, Friday, 3:00 – 4:00 PM Boston Time
Speaker: Paul Krogmeier (UIUC)
In-person Location: CDS 1101
Abstract: Many classic symbolic languages studied in computer science, e.g. regular expressions, finite-variable logics, modal logics like LTL and CTL, and many others, have the following intriguing property (let’s call it [*]): the semantics of expressions can be evaluated over arbitrary fixed structures using an amount of memory which depends on the structure but is largely independent of expression size. For example, checking whether a finite word w is matched by a regular expression e can be accomplished by a recursive program that navigates the syntax tree for e and checks that smaller and smaller subwords of w match the subexpressions of e. We call languages that possess the property [*] finite aspect checkable (FAC). These languages are interesting because they have decidable synthesis and learning problems. For instance, given finite sets of positively and negatively labeled words, as well as a grammar specifying a syntactic fragment of regular expressions, we can ask whether there exists a regular expression from the grammar that separates the words. This problem is decidable, despite the fact there may be infinitely-many expressions to search over. The proof relies on translating the recursive programs for evaluating expression semantics (mentioned above) into tree automata, with decision procedures obtained by reduction to tree automaton emptiness. In this talk, I will explain this generic technique for proving such decidable learning results for FAC languages and go through some examples.
This work builds on our popl 2022 paper (https://dl.acm.org/doi/pdf/10.1145/3498671) and will appear at oopsla 2023 (preprint: https://arxiv.org/abs/2302.05741).
Hefty Algebras — Modular Elaboration of Higher-Order Algebraic Effects
Time: Apr 07th, Friday, 3:00 – 4:00 PM Boston Time
Speaker: Casper Bach Poulsen (Delft University of Technology)
In-person Location: CDS 1101
Abstract: Algebraic effects and handlers is an increasingly popular approach to programming with effects. An attraction of the approach is its modularity: effectful programs are written against an interface of declared operations, which allows the implementation of these operations to be defined and refined without changing or recompiling programs written against the interface. However, higher-order operations (i.e., operations that take computations as arguments) break this modularity. While it is possible to encode higher-order operations by elaborating them into more primitive algebraic effects and handlers, such elaborations are typically not modular. In particular, operations defined by elaboration are typically not a part of any effect interface, so we cannot define and refine their implementation without changing or recompiling programs. To resolve this problem, a recent line of research focuses on developing new and improved effect handlers. In this paper we present a (surprisingly) simple alternative solution to the modularity problem with higher-order operations: we modularize the previously non-modular elaborations commonly used to encode higher-order operations. Our solution is as expressive as the state of the art in effects and handlers.
Owl: Compositional Verification of Security Protocols via an Information-Flow Type System
Time: Apr 14th, Friday, 3:00 – 4:00 PM Boston Time
Speaker: Joshua Gancher (CMU)
In-person Location: CDS 548
Abstract: Computationally sound protocol verification tools promise to deliver full-strength cryptographic proofs for security protocols, such as TLS and WireGuard. However, existing tools are difficult to apply at scale, due to a lack of either modularity or automation.
This work is to appear at IEEE S&P 2023. Link here: https://eprint.iacr.org/2023/473.pdf
Contextual Coinduction and Classical Logic
Time: Apr 21st, Friday, 3:00 – 4:00 PM Boston Time
Speaker: Paul Dowen (UMass Lowell)
In-person Location: CDS 1101
Abstract: Induction has become the cornerstone in the theory and practice of formal methods and programming. From the design of functional algorithms, to the verification of software, to the mechanization of mathematics, to just pencil-and-paper proofs, all of these challenges in programming languages rest on the shoulders of a well-understood computational foundation for induction. Yet somehow the treatment of coinduction, the dual to induction, is much less mature. As a result, naturally coinductive systems — like web servers, operating systems, and user interfaces — are much harder to describe and reason about. Mechanizing coinductive proofs can be easily foiled by ad-hoc and surprising restrictions. And even putting together an informal prose proof by coinduction becomes a daunting task fraught with hidden pitfalls that lead to cyclical paradoxes.
This talk will explore a computational understanding of coinduction that puts it on equal and opposite footing as its well-used partner, induction. The key idea is that — while induction primarily revolves around a highly structured flow of information and answers — coinduction is founded on a structured view for organizing questions and control flow based on contextual equivalence. We will look at examples of an informal method to directly write pencil-and-paper coinductive arguments, with confidence that we have avoided vicious cycles and paradoxes, using an easy-to-check pattern. Then we will formalize this intuitive pattern of coinductive proof in terms of a computational classical logic which reveals the implicit structure underlying the questions that make up the coinductive hypothesis. Just like the formalization of the inductive hypothesis, we can immediately check for well-founded applications of the coinductive hypothesis using only local information based on the names of labels, rather than ad-hoc syntactic checks.
Integrating quantity calculus into Montague semantics
Time: Apr 28th, Friday, 3:00 – 4:00 PM Boston Time
Speaker: Elizabeth Coppock (Boston University)
In-person Location: CDS 1101
Abstract: Quantities can be added, subtracted, multiplied and divided. Are there expressions of natural language that can express the concept of quantity division? In this talk, I argue that English “per” is one such item. I then show how mathematical foundations can be borrowed from the field of ‘quantity calculus’ into a Montague-style fragment of English (building of course on the lambda calculus, as we do in
formal semantics). With these tools, and a few slightly fancy assumptions about “per”, we will be able to account for what I call “triangle equivalences”, such as the equivalence between “The cost of wheat per ton is $100” and “The cost of wheat is $100 per ton”.
Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
Time: May 05th, Friday, 3:00 – 4:00 PM Boston Time
Speaker: Lorenz Leutgeb (Max Planck Institute for Informatics)
In-person Location: CDS 1101
Abstract: Amortised analysis, introduced by Sleator and Tarjan, enables formal argument about the complexity of operations on self-adjusting data structures (insertion, deletion, etc.). Applying the physicist method of amortised analysis yields potential functions that involve logarithmic expressions, for which methods of automated reasoning and solvers are not as advanced as for e.g. linear real arithmetic. This might be one of the reasons why most complexity bounds in the literature were obtained manually or using interactive theorem provers.
In this talk I will present our approach to fully-automated analysis of logarithmic amortised complexity. We were, for the first time, able to fully automatically reproduce, and in some cases improve upon, the results in the literature for a number of self-adjusting data structures, such as splay trees, randomised splay trees, splay heaps, randomised splay heaps, pairing heaps, and randomised meldable heaps. Our approached is based on a type-and-effect system, i.e. the challenge of finding potential functions that represent bounds on amortised cost is framed as type inference. The programming language we introduce to express operations is strict, first-order and purely functional. It allows sampling static Bernoulli distributions, includes non-deterministic choice, and a ticking operator that results in a very flexible cost model. It comes with both a small-step and big-step semantics that yield two subtly different notions of soundness.
In the talk I will recap amortised analysis, present our results, explain our method along a simple example, and state key features of our setup.
Gradual Typing for Effect Handlers
Time: May 12th, Friday, 3:00 – 4:00 PM Boston Time
Speaker: Max New (University of Michigan)
In-person Location: CDS 1101
Abstract: Algebraic effect operations and handlers are a typed abstraction for working with delimited continuations that generalize exception handlers to allow for resumption at the site where an effect is raised. Long popular in theoretical calculi and research languages for effects, handlers are only recently seeing adoption in mainstream languages with their support in OCaml 5. However the lack of an effect typing system in OCaml means that there are no guarantees an effect will be caught, similar to unchecked exception types in Java. Adding a conventional effect system to OCaml would result in the need to migrate large codebases to use the new effects or sacrifice re-use of existing codebases.
We present GrEff, a language that uses gradual typing to allow for programs with and without effect typing to safely interact, and for a smooth migration path for code from unchecked to checked effects. This
allows for the code written in the unchecked and checked sub-languages to interact freely, with mediating handlers inserted automatically to ensure the interaction obeys the typing discipline of the checked code. To support this interaction, GrEff has a simple module system with checked and unchecked modules in the style of Typed Racket, where different modules can have different typings for the same effect name. We derive a reduction semantics from an inequational theory for effects and gradual type casts. Then we prove that the checked language satisfies equations for checked effect handlers as well as the graduality principle by constructing a step-indexed operational logical relations model.
Schedule (Fall 2022)
Below is a list of seminar dates for with information on the speakers:
| Date | Speaker | Talk Title |
| Oct 12 | Damien Pous (CNRS) | Reductions for Kleene algebra with top |
| Oct 19 |
Pierre Civit (Sorbonne Université)
|
[Joint with BUSec] Dynamic Probabilistic Automata (Untimed, Timed, Bounded) |
| Oct 26 | Arthur Azevedo de Amorim (BU) | A Separation Logic for Cryptographic Reasoning |
| Nov 2 | Carlo Angiuli (CMU) | Internalizing Representation Independence with Univalence |
| Nov 9 | David Kahn (CMU) | The Quantum Physicist’s Method in Automatic Amortized Resource Analysis |
| Nov 16 | Farzaneh Derakhshan (CMU) | Recursive Session Logical Relations for Information Flow Control |
| Nov 23 | No Talk (Thanksgiving Recess) | |
| Nov 30 | Todd Schmid (UCL) | A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests |
| Dec 7 | Irene Yoon (University of Pennsylvania) | Formal Reasoning About Layered Monadic Interpreters |
| Dec 14 | Kevin Batz (RWTH Aachen University) | Automated Weakest Precondition Reasoning for Probabilistic Programs |
| Dec 21 |
Reductions for Kleene Algebra with Top
Time: Oct 12, Wendesday, 12:00pm Boston Time
Location: CAS 502
Speaker: Damien Pous (CNRS)
Abstract: Kleene algebra with tests (KAT) can be used to reason about imperative programs. For instance, one may easily encode Hoare triples for partial correctness. We illustrate this within the Coq proof assistant.
Recently, an extension of KAT with a top element has been proposed by Zhang, Azevedo de Amorim & Gaboardi, which makes it possible to encode O’Hearn’s incorrectness logic. However, completeness of such an extension was left open.
We will prove two completeness results for Kleene algebra with a top element, with respect to languages and binary relations. While the equational theories of those two classes of models coincide over the signature of Kleene algebra, this is no longer the case when we consider an additional constant “top” for the full element. Indeed, the full relation satisfies more laws than the full language, and we show that those additional laws can all be derived from a single additional axiom.
The proofs combine models of closed languages, reductions, a bit of graphs, and a bit of automata. (jww Jana Wagemaker, after discussions with Paul Brunet, Amina Doumane & Jurriaan Rot)
[Joint with BUSec] Dynamic Probabilistic Automata (Untimed, Timed, Bounded)
Time: Oct 19, Wendesday, 12:30pm Boston Time
Location: Hariri Seminar Room
Speaker: Pierre Civit (Sorbonne Université)
Abstract: We present Dynamic Probabilistic Automata, a framework to model dynamic probabilistic distributed systems. Our work extends Dynamic Automata formalism from Attie & Lynch [1] to probabilistic setting. The original Dynamic Automata formalism included operators for parallel composition, action hiding, action renaming, automaton creation, and behavioral sub-typing by means of trace inclusion. They can model mobility by using signature modification. They are also hierarchical: a dynamically changing system of interacting automata is itself modeled as a single automaton. Our work extends to (both timed and untimed) probabilistic settings all these features. Furthermore, we prove necessary and sufficient conditions to obtain the monotonicity of implementation precongruence with respect to automata creation and destruction .
[1] Dynamic input/output automata: A formal and compositional model for dynamic systems. P. Attie & N. Lynch
[2] Compositional security for task-PIOAs. R. Canetti, L. Cheung, D. Kaynar, N. Lynch, O. Pereira
A Separation Logic for Cryptographic Reasoning
Time: Oct 26th, Wendesday, 12:00pm Boston Time
Location: CAS 502
Speaker: Arthur Azevedo de Amorim (BU)
Abstract: Modern separation logics enable a compositional style of reasoning about challenging programming features, such as heap-allocated data structures, shared-memory concurrency, and message passing. This expressive power makes the logic well-suited to model and verify complex systems in a scalable manner. In this talk, I’ll describe an extension of separation logic that allows us to reason about yet another challenging feature: cryptography. Our logic, Cryptis, can describe secrecy and integrity invariants associated with encrypted messages in the symbolic model of cryptography. The extension makes it possible to reason about the guarantees afforded by cryptographic protocols used to protect connections over an untrusted network, and combine these guarantees with other verified components to derive end-to-end correctness proofs.
Internalizing Representation Independence with Univalence
Time: Nov 2nd, Wendesday, 12:00pm Boston Time
Location: CAS 502
Speaker: Carlo Angiuli (CMU)
Abstract:
In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. In the dependently-typed setting, however, we would like to appeal to such invariance results within a language itself, in order to transfer theorems from simple to complex implementations. Homotopy type theorists have noted that Voevodsky’s univalence principle equates isomorphic structures, but unfortunately many instances of representation independence are not isomorphisms.
In this talk, I’ll describe a technique for establishing internal relational representation independence results in Cubical Agda by using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them. The correspondence becomes an isomorphism between the quotiented types, thereby allowing us to obtain an equality of implementations by univalence. Joint work with Evan Cavallo, Anders Mörtberg, and Max Zeuner. Available at https://dl.acm.org/doi/10.1145/3434293.
The Quantum Physicist’s Method in Automatic Amortized Resource Analysis
Time: Nov 9th, Wendesday, 12:00pm Boston Time
Location: CAS 502
Speaker: David Kahn (CMU)
Abstract: This talk presents the quantum physicist’s method in Automatic Amortized Resource Analysis (AARA). AARA is a type system that can be used to automatically derive cost bounds for programs. The technique works by using types to locally define potential functions for the physicist’s method of amortized analysis, where potential energy is metaphorically stored in data structures.
However, simple program patterns like branching and tree traversals can require non-local reasoning to derive good cost bounds, and this is incompatible with AARA’s locally-defined potential functions. The quantum physicist’s method is a framework that can construct the needed non-local potential functions out of local ones, upgrading AARA’s use of the physicist’s method. The resulting system has been implemented and can provide better cost bounds for real code with only moderate overhead.
Recursive Session Logical Relations for Information Flow Control
Time: Nov 16th, Wendesday, 12:00pm Boston Time
Location: CAS 502
Speaker: Farzaneh Derakhshan (CMU)
Abstract: Information flow control (IFC) type systems restrict the propagation of sensitive data to ensure noninterference, asserting that an attacker cannot infer any secrets from made observations. In this talk, I present SILL_sec, a language for message-passing concurrency equipped with an IFC type system. SILL_sec is based on binary session types, and its building blocks are bi-directional communicating processes connected by channels. Binary session types delimit the kinds of observations that can be made along a communication channel by imposing a message exchange protocol, aka session type. These protocols govern the exchange along a single channel, but leave the propagation along adjacent channels unconstrained, demanding the need for an IFC type system to rule out insecure flow of information. We established noninterference of SILL_sec by devising a session logical relation, a logical relation indexed by the secrecy-level-enriched session types. In the talk, I describe the logical relation as a proof-enabler for verifying noninterference, a program equivalence up to the attacker’s secrecy level, in the presence of non-termination and concurrency. In particular, I explain the basic schema of session logical relations designed to establish an extensional logical equivalence and to ensure the bisimilarity of communicating processes.
A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
Time: Nov 30th, Wendesday, 12:00pm Boston Time
Location: CAS 502
Speaker: Todd Schmid (UCL)
Abstract: Guarded Kleene Algebra with Tests (GKAT) is a program logic for reasoning equationally about control flow in imperative programs. It is a fragment of Kleene Algebra with Tests (KAT) where most everyday control flow structures can be expressed and yet program equivalence can be checked in nearly linear time (as opposed to KAT’s PSPACE-complete decision problem). In a paper from 2019 (Smolka, et. al.), the authors axiomatize program equivalence in GKAT and conjecture that a much simpler axiomatization is also complete. In this talk, I will report on recent work by Tobias Kappe, Alexandra Silva, and myself that turns to recent research in process algebra to partially resolve their conjecture.
Formal Reasoning About Layered Monadic Interpreters
Time: Dec 7th, Wendesday, 12:00pm Boston Time
Location: CAS 502
Speaker: Irene Yoon (University of Pennsylvania)
Abstract: Monadic computations built by interpreting, or handling, operations of a free monad are a compelling formalism for modeling language semantics and defining the behaviors of effectful systems. The resulting layered semantics offer the promise of modular reasoning principles based on the equational theory of the underlying monads. However, there are a number of obstacles to using such layered interpreters in practice. With more layers comes more boilerplate and glue code needed to define the monads and interpreters involved. That overhead is compounded by the need to define and justify the relational reasoning principles that characterize the equivalences at each layer.
During this talk, I will discuss our ICFP ’22 paper (joint work with Yannick Zakowski and Steve Zdancewic) which addresses these problems by significantly extending the capabilities of the Coq interaction trees (ITrees) library, which supports layered monadic interpreters. We characterize a rich class of interpretable monads—obtained by applying monad transformers to ITrees—and show how to generically lift interpreters through them. We also introduce a corresponding framework for relational reasoning about “equivalence of monads up to a relation ”. This collection of typeclasses, instances, new reasoning principles, and tactics greatly generalizes the existing theory of the ITrees library, eliminating large amounts of unwieldy boilerplate code and dramatically simplifying proofs.
Paper: https://dl.acm.org/doi/10.1145/354763
Automated Weakest Precondition Reasoning for Probabilistic Programs
Time: Dec 14th, Wendesday, 12:00pm Boston Time
Location: CAS 502
Speaker: Kevin Batz (RWTH Aachen University)
Abstract: Probabilistic programs are a popular technique for modeling stochastic processes and randomized algorithms. In this talk, we consider the verification of discrete probabilistic programs. For that, I introduce a weakest precondition-style calculus for reasoning about properties like “What is the probability that a given program terminates?” or “What is the expected final value of a program variable?”. I then address several aspects regarding the automation of this calculus.
As for standard programs, automating the verification of probabilistic programs requires an assertion language for specifying properties of interest. In the probabilistic setting, assertions are quantitative – functions mapping program states to numbers. We study a syntax for those quantitative assertions, enabling relatively complete verification of probabilistic programs. I will highlight the key challenges and properties of our assertion language.
Finally, we discuss automatic weakest precondition-style verification of probabilistic programs with an emphasis on possibly unbounded probabilistic loops. The verification of loops is tackled by quantitative loop invariants. I demonstrate how to combine quantitative loop invariants with Satisfiability Modulo Theories techniques to obtain automatic verification methods.
Schedule (Spring 2022)
Below is a list of seminar dates for with information on the speakers:
Logical Tools for the PL Practitioner: from Datalog and SMT to ASP and Beyond
Time: Feb 22nd, Tuesday, 4:00pm Eastern Time
Speaker: Michael Greenberg (Stevens Institute of Technology)
Abstract: In an ideal world, the formalism we prove things about would neatly match the artifact we implement. Various logical tools help us bridge the gap between theoretical, paper proofs and practical, efficient implementations.
Datalog and SMT have long been acknowledged as powerful tools in the PL practitioner’s toolbox. Datalog use is on the rise; SMT is pervasive. Both tools marry classical logics with efficient implementations; both tools offer declarative languages supported by powerful, complex implementations.
I’ll first talk about how our Formulog language combines Datalog, SMT, and functional programming. Formulog helps bridge the theory/practice gap with efficiently executable, formal artifacts.
Then I’ll talk about a recent application of answer set programming (ASP) to a Datalog synthesis problem. ASP is a powerful technology combining features of Datalog and SAT, and it deserves to be better known in the PL community.
This is joint work with Steve Chong and Aaron Bembenek, both at Harvard.
Bio: Michael Greenberg is an assistant professor at Stevens Institute of Technology. He received BAs in Computer Science and Egyptology from Brown University (2007) and his PhD in Computer Science from the University of Pennsylvania (2013); previously, he was an assistant professor at Pomona College. His work has ranged from functional-reactive JavaScript (with Shriram Krishnamurthi at Brown) to runtime verification of higher-order programs (with Benjamin Pierce at Penn) to software-defined networking (with Dave Walker at Princeton) to present activities focused on the POSIX shell and executable formalism.
Trace-Based Control-Flow Analysis
Time: Mar 22nd, Tuesday, 4:00pm Eastern Time
Speaker: Benoît Montagu (Inria)
Abstract: I will present some recent advances in control-flow analysis (CFA) for the untyped lamba-calculus, a classic static analysis for higher-order languages.
First, I will explain how the well-known k-CFA analysis can be obtained in a simple manner, by abstracting the execution traces of a lambda-term. To this end, I will introduce a small-step semantics that builds a trace of the control-flow events (calls, and returns of functions) that are produced by a program. Using this technical development, the constraint-based formulation of k-CFA can be proved sound in a modular way, as opposed to the usual method based on “subject reduction”.
Then, building on the previous development, I will introduce a novel control-flow analysis, called nabla-CFA, that uses a widening operator. Experiments show that nabla-CFA converges faster in practice compared to k-CFA. Nabla-CFA also enables the use of domains of unbounded heights, such as intervals—a new point in the design space of CFAs. I will discuss how nabla-CFA compares to k-CFA in terms of cost and precision and, if time permits, sketch some recent developments that solve some of the limitations of nabla-CFA.
This work was presented at PLDI’21.
Executable Denotational Semantics with Interaction Trees
Time: Apr 5th, Tuesday, 4:00pm Eastern Time
Speaker: Li-yao Xia (University of Pennsylvania)
Abstract: Machine-checked proofs are now feasible at scale, in a wide variety of domains. As the systems we verify become more complex, a growing challenge is to relate specifications across many abstraction layers, expressed in disparate formalisms.
Interaction trees are a model to represent the behavior of effectful and reactive systems. Interaction trees are implemented as a library in the Coq proof assistant. This model is modular, compositional, and executable, which makes it applicable to express specifications at many layers of the computing stack. I discuss two applications. First, we verify a compiler from a simple imperative language to assembly, by proving a semantic preservation theorem which is termination-sensitive, using an equational proof. Second, we build a framework of concurrent objects. Concurrent objects are implemented using interaction trees, leveraging the functionalities provided by the library. The framework supports proof techniques for both linearizability and strict serializability, two well-known correctness conditions for concurrent objects.
From Inductive Lambda Encodings to Divide-and-Conquer Recursion
Time: Apr 12th, Tuesday, 4:00pm Eastern Time
Speaker: Aaron Stump (The University of Iowa)
Abstract: This talk begins with typed lambda encodings, where data like numbers, lists, and trees are represented as terms of pure lambda calculus, typable using impredicative polymorphism. The inability to derive induction for such encodings in the Calculus of Constructions (CC) led historically to the development of the Calculus of Inductive Constructions (CIC), the type theory underlying Coq. In CIC, inductive types are added to the theory as primitives. We will see an alternative, where induction can be derived in an extension of CC with dependent intersection types. This derivation has been implemented in the Cedille prover, and is the basis for Cedille’s elaboration of inductive types to its core theory. Going further, we will see how to derive a new form of recursion/induction called divide-and-conquer recursion. This form of recursion allows one to initiate subsidiary inner recursions which can construct data upon which outer recursions may legally recurse. This allows direct implementation in total type theory of algorithms like mergesort, quicksort, etc., which otherwise require methods like well-founded recursion. Amazingly, these ideas can be realized not just in a somewhat exotic prover like Cedille, but in Coq.
Bio: Aaron Stump is a professor of Computer Science at The University of Iowa. His current research interests are in new foundations for type theory, as well as total functional programming. He is the creator of The Iowa Type Theory Commute podcast.
Distribution Theoretic Semantics for Non-Smooth Differentiable Programming
Time: Apr 19th, Tuesday, 4:00pm Eastern Time
Speaker: Pedro Azevedo de Amorim (Cornell University)
Abstract: With the widespread of deep learning and gradient descent inspired optimization algorithms, differentiable programming has gained traction. Nowadays it has found applications in many different areas as well, such as scientific computing, robotics, computer graphics and others. One of its notoriously difficult problems consists in interpreting programs that are not differentiable everywhere.
In this work we define , a core calculus for non-smooth differentiable programs and define its semantics using concepts from distribution theory, a well-established area of functional analysis. We also show how presents better equational properties than other existing semantics and use our semantics to reason about a simplified ray tracing algorithm.
Intrinsic semantics of termination-insensitive noninterference
Time: Apr 26th, Tuesday, 4:00pm Eastern Time
Speaker: Jonathan Sterling (Aarhus University)
Abstract: Security-typed programming languages aim to control the flow of high-security information to low security clients. Starting with Abadi et al.’s dependency core calculus, the denotational semantics of such languages has been dominated by an extrinsic approach in which an existing insecure model of computation (e.g. ordinary domains) is restricted by a logical relation of “indistinguishability” to prevent low-security outputs from depending on high-security inputs (noninterference). Thus in the extrinsic approach, security properties are bolted onto an insecure model by brute force, as it were. A more refined information flow policy called termination-insensitive noninterference allows high-security bits to be leaked through termination channels but not through return values; unfortunately, the adaptation of the extrinsic/relational semantics to this more relaxed policy is incompatible with the transitivity of the logical relation, contradicting the intuition of “indistinguishability”.
In contrast, an intrinsic semantics of security typing would involve a new computational model that evinces secure information flow and noninterference properties directly without any post hoc restriction by a logical relation. We contribute the first such intrinsic semantics of security typing in this sense by considering sheaves of dcpos on a space of abstract behaviors on which security classes arise as open/closed partitions; the security monads then arise as the closed modalities of topos theory that restrict a sheaf to its component over a closed subspace.
An advantage of our intrinsic semantics is that termination-insensitive noninterference arises automatically from our computational model, namely the fact that the Sierpiński domain is not a constant sheaf; a further advantage is that our semantics is an instance of standard domain theoretic denotational semantics, albeit over a richer category of domains. This is joint work with Robert Harper.
Preprint: Sheaf semantics of termination-insensitive noninterference
Bio: Jonathan Sterling is a Marie Skłodowska-Curie Postdoctoral Fellow at Aarhus University, supervised by Lars Birkedal; previously he received his Ph.D. from Carnegie Mellon University where he was advised by Robert Harper.
Verifying Quantum Programs: From Deutsch’s Algorithm to Shor’s
Time: May 3rd, Tuesday, 4:00pm Eastern Time
Speaker: Robert Rand (University of Chicago)
Abstract: Ensuring the correctness of quantum programs is a challenging but critical problem. As a field, quantum computing has developed a broad range of powerful algorithms, with applications from computer security to machine learning. However, while these algorithms have been programmed in a variety of languages, they have never been executed: We simply don’t have quantum or classical computers capable of doing the job. The implementations are likely to fail on real-world quantum computers and when they do so, we will not be able to easily diagnose the errors. Formal verification has proven remarkably successful in addressing this problem, despite the many complications of quantum computing. In this talk, I will review progress in this domain, from early work on verifying Deutsch’s algorithm and quantum teleportation in the QWIRE language to a brand new proof of Shor’s algorithm using the proof-focused SQIR intermediate representation.
Familiarity with the Coq proof assistant will be useful in understanding the details of this talk, no quantum computing background will be assumed.
Bio: Robert Rand is an Assistant Professor of Computer Science at the University of Chicago. His research focuses on programming languages and verification for quantum computing and his main projects include the QWIRE quantum circuit language, the VOQC compiler for quantum circuits, and a stabilizer-based type system for quantum programs. He is currently developing tools for novel models of quantum computation like the ZX-calculus and the one-way quantum computer. Robert developed and maintains the INQWIRE QuantumLib, an open-source library for verified quantum computing in the Coq proof assistant, which underlies many of his projects including his online textbook, Verified Quantum Computing.
Paper link(s):
https://arxiv.org/pdf/2010.01240.pdf (ITP paper)
https://arxiv.org/pdf/2204.07112.pdf (Shor’s algorithm preprint)
Reasonable Space for the Lambda-Calculus, Logarithmically
Time: May 5th, Thursday, 4:00pm Eastern Time
Speaker: Gabriele Vanoni (University of Bologna)
Abstract: Can the lambda-calculus be considered as a reasonable computational model? Can we use it for measuring the time and space consumption of algorithms? While the literature contains positive answers about time, much less is known about space. This paper presents a new reasonable space cost model for the lambda-calculus, based on a variant over the Krivine abstract machine. For the first time, this cost model is able to account for logarithmic space. Moreover, we study the time behavior of our machine and show how to transport our results to the call-by-value lambda-calculus. Finally, we give a system of non-idempotent intersection types that is able to capture exactly the newly introduced space measure.
Short Bio: Gabriele Vanoni completed its PhD program at Università di Bologna working under the supervision of Ugo Dal Lago. He has worked mainly on implementation techniques and complexity analysis for the lambda-calculus. He has spent five months at LIPN in Paris, visiting Damiano Mazza, and is currently visiting the FLINT group, led by Zhong Shao, at Yale University.
Programming with Commutativity
Time: May 10th, Tuesday, 4:00pm Eastern Time
Speaker: Eric Koskinen (Stevens Institute of Technology)
Abstract: There is an ongoing effort to provide programming abstractions that ease the burden of exploiting multicore hardware. Many programming abstractions (eg, concurrent objects, transactional memory, etc.) simplify matters, but still involve intricate engineering. We argue that some difficulty of multicore programming can be meliorated through a declarative programming style in which programmers directly express the independence of fragments of sequential programs.
I will describe a new language paradigm in which programmers write programs in a familiar, sequential manner, with the added ability to explicitly express the conditions under which code fragments sequentially commute. Putting such commutativity conditions into source code offers a new entry point for a compiler to exploit the known connection between commutativity and parallelism. I will discuss semantic implications and how to ensure equivalence between the parallel and sequential semantics.
Commutativity conditions (in our and other settings) must be sound or else concurrent execution could be incorrect. I will next describe a series of work (TACAS’18, VMCAI’21) in which we automatically verify and even synthesize commutativity conditions of programs.
Software development meets math: Lean and its mathematical library
Time: May 31st, Tuesday, 4:00pm Eastern Time
Speaker: Robert Y. Lewis (Brown University)
Abstract: I have two goals with this talk: (1) to give an introduction to Lean, a proof assistant based on the calculus of inductive constructions; (2) to describe mathlib, a massive library of (mostly) mathematics verified in Lean.
Lean is a project of Leonardo de Moura at Microsoft Research. Lean 4, a new version of the system at milestone release stage, is a powerful programming language and largely implemented in Lean itself. While logically similar to Coq, Lean has a number of distinguishing features, some technical and some sociological. I will explain some of these features, targeting an audience that is broadly familiar with other proof assistants.
Lean has attracted a disproportionate number of users interested in mathematical applications. The de facto standard library for Lean 3, mathlib, contains nearly 900k lines of code written by 250 contributors and maintained by a team of community members including myself. Its contents span a huge range of mathematics, as well as metaprograms and more traditional data structures. The community has adopted language and tooling from the world of open-source software engineering and applied it to mathematics in novel ways. I will highlight some of the success stories and lessons that the mathlib project has taught us, drawing on two recent formalization papers of my own.
Bio: Robert Y. Lewis is a lecturer in the computer science department at Brown University. He received his PhD in Pure and Applied Logic from Carnegie Mellon University and was a postdoc at the Vrije Universiteit Amsterdam.
Related links:
The official Lean website: https://leanprover.github.io/
The Lean community/mathlib website, with many resources: https://leanprover-community.github.io/
The mathlib Community. *The Lean mathematical library*: https://arxiv.org/abs/1910.09336
Leonardo de Moura and Sebastian Ullrich. *The Lean 4 theorem prover and programming language*: https://leanprover.github.io/papers/lean4.pdf
Frédéric Dupuis, Robert Y. Lewis, and Heather Macbeth. *Formalized functional analysis with semilinear maps*: https://arxiv.org/abs/2202.05360
Johan Commelin and Robert Y. Lewis. *Formalizing the ring of Witt vectors*: https://arxiv.org/abs/2010.02595
Schedule (Fall 2021)
Below is a list of seminar dates for with information on the speakers:
Abstracts
Reasoning about the garden of forking paths
Speaker: Yao Li (University of Pennsylvania)
Time: Sep 28th, Tuesday, 4:00pm Eastern Time
Abstract: Lazy evaluation is a powerful tool for functional programmers. It enables the concise expression of on-demand computation and a form of compositionality not available under other evaluation strategies. However, the stateful nature of lazy evaluation makes it hard to analyze a program’s computational cost, either informally or formally. In this work, we present a novel and simple framework for formally reasoning about lazy computation costs based on a recent model of lazy evaluation: clairvoyant call-by-value. The key feature of our framework is its simplicity, as expressed by our definition of the clairvoyance monad. This monad is both simple to define (around 20 lines of Coq) and simple to reason about. We show that this monad can be effectively used to mechanically reason about the computational cost of lazy functional programs written in Coq.
Paper link: https://doi.org/10.1145/3473585 (you do NOT need to read the paper; I just post the link here for reference)
Code link: https://github.com/lastland/ClairvoyanceMonad
A Certified Scalably Executable Semantics for Nondeterministic True-Concurrent Languages
Speaker: Brittany Nkounkou (University of Connecticut)
Time: Oct 05th, Tuesday, 4:00pm Eastern Time
Abstract: A nondeterministic true-concurrent language defines the possible behavior of two parallel indivisible operations to include both the nondeterministic interleaving of the operations and their simultaneous execution. Executing largely parallel programs in such a language is especially challenging if it must satisfy some global predicate over simultaneously executed operations that cannot be inferred from some local predicate over each of its individual operations. In this talk, I will address this challenge with a labelled-transition operational semantics that is (1) mechanically formalized and (2) readily parametric over fitting nondeterministic true-concurrent languages, and whose execution is (3) mechanically verified and (4) scalable with respect to largely parallel programs. The semantics is built using the Coq proof assistant and utilizes a modular continuation-passing-style approach to its execution. I’ll exemplify the scalability and applicability of the semantics by using it to simulate the first asynchronous microprocessor, a largely parallel program in the nondeterministic true-concurrent language Communicating Hardware Processes (CHP). I further compare this simulation in our framework to that in Maude. This work is currently under double-blind review.
Julia: Language Design and Users Working Together.
Speaker: Julia Belyakova (Northeastern University)
Time: Oct 12th, Tuesday, 4:00pm Eastern Time
Abstract: As a programming language for scientific computing, Julia strives for predictable performance as well as flexibility and ease of use. To tackle this challenge, Julia employs two strategies. First, it enables highly compositional programs by using multiple dispatch as the core paradigm, but at the same time, pragmatically restricts the language to facilitate optimizations. Second, Julia enables productive collaboration between the programmer and the JIT compiler by making the compiler’s behavior predictable and encouraging optimization-conducive coding discipline.
In this talk, we look at several components of this two-fold approach. We start with an overview of multiple dispatch. Next, we talk about type stability, a property of the code that enables the key optimization in Julia’s optimization pipeline. Finally, we look at the world age, a mechanism that allows for a pragmatic trade-off between flexibility of “eval” and predictability of compiler optimizations.
Compositional Security for Reentrant Applications
Speaker: Ethan Cecchetti (Maryland Cybersecurity Center)
Time: Oct 19th, Tuesday, 4:00pm Eastern Time
Abstract: The disastrous vulnerabilities in smart contracts sharply remind us of our ignorance: we do not know how to write code that is secure in composition with malicious code. Information flow control has long been proposed as a way to achieve compositional security, offering strong guarantees even when combining software from different trust domains. Unfortunately, this appealing story breaks down in the presence of reentrancy attacks. In this talk I will present a highly general definition of reentrancy and reentrancy security that allows software modules like smart contracts to protect their key invariants while retaining the expressive power of safe forms of reentrancy. I will describe how we can combine a type system and run-time mechanism to enforce this new notion of security even in the presence of unknown code.
This work recently received a best paper award at IEEE S&P ’21. The paper is available at https://ethan.umiacs.io/papers/serif.pdf
Bio: Ethan is currently a post-doc at the University of Maryland working primarily with Mike Hicks and is on the market for tenure-track academic jobs this year. His research focuses broadly on designing secure decentralized systems and building tools to ease their development using programming languages and applied cryptography. He completed his PhD at Cornell in August 2021 working with Andrew Myers and Ari Juels. More information is available at his website: https://ethan.umiacs.io/
Beyond Collapsing Towers: Staging a Relational Interpreter
Speaker: Nada Amin (Havard University)
Time: Oct 26th, Tuesday, 4:00 pm Eastern Time
Abstract: Staging — splitting a program into stages, the code generator and the generated code — can mechanically turn an interpreter into a compiler. Going further, we can collapse a tower of interpreters into a one-pass compiler.
An interpreter written in a relational programming language (miniKanren) for a functional programming language (subset of Racket) can not only evaluate an expression to a value, but also synthesize an expression (or more generally, term) for a hole — in particular, turning functions into relations.
We adapt staging to the relational setting, turning functions into relations — and more — with reduced interpretive overhead, promising a tractable avenue for the synthesis of functional programs.
Semantic Techniques for Information-Flow Languages
Speaker: Andrew Hirsch (Max Planck Institute for Software Systems)
Time: Nov 02th, Tuesday, 4:00 pm Eastern Time
Abstract: Information-flow languages enforce information-security policies for any program written in them. The most basic security policy of such languages is noninterference, which states that secret inputs do not affect the observations of an adversary. However, current practices for developing and proving correct information-flow languages rely exclusively on hand-rolled proofs, making exploration of the design space slow and labor intensive. Moreover, proofs are almost never given for implementations of information-flow languages.In this talk, I discuss how semantic techniques can alleviate some of this burden by providing general frameworks for noninterference proofs. In particular, I discuss how the semantics of effects eases the burden of proof for the source language, how denotational semantics can ease proofs of security preservation for compilers, and how modal logics can ensure that low-level security enforcement preserves noninterference.
Solver-Based Gradual Type Migration
Speaker: Arjun Guha (Northeastern University)
Time: Nov 09th, Tuesday, 4:00 pm Eastern Time
Abstract: Gradually typed languages allow programmers to mix statically and dynamically typed code, enabling them to incrementally reap the benefits of static typing as they add type annotations to their code. However, this type migration process is typically a manual effort with limited tool support. In this talk, we examine the problem of automated type migration: given a dynamic program, infer additional or improved type annotations.
Existing type migration algorithms prioritize different goals, such as maximizing type precision, maintaining compatibility with unmigrated code, and preserving the semantics of the original program. We argue that the type migration problem involves fundamental compromises: optimizing for a single goal often comes at the expense of others. Ideally, a type migration tool would flexibly accommodate a range of user priorities.
We present TypeWhich, a new approach to automated type migration for an extension of the gradually-typed lambda calculus. Unlike prior work, which relies on custom solvers, TypeWhich produces constraints that can be solved by an off-the-shelf MaxSMT solver. This allows us to easily express objectives, such as minimizing the number of necessary syntactic coercions, and constraining the type of the migration to be compatible with unmigrated code.
We present the first comprehensive evaluation of GTLC type migration algorithms, and compare TypeWhich to four other tools from the literature. Our evaluation uses prior benchmarks, and a new set of “challenge problems”. Moreover, we design a new evaluation methodology that highlights the subtleties of gradual type migration. In addition, we apply TypeWhich to a suite of benchmarks for Grift, a programming language based on the GTLC. TypeWhich is able to reconstruct all human-written annotations on all but one program.
Biography: Arjun Guha is an associate professor of Computer Science at Northeastern University. Using the tools and techniques of programming languages, his research addresses security, reliability, and performance problems in web applications, systems, networking, and robotics. His work has received an ACM SIGPLAN Most Influential Paper Award, an ACM SIGPLAN Distinguished Paper Award, an ACM SIGPLAN Research Highlight, and a Google Faculty Research Award.
Steel: Proof-Oriented Programming in a Dependently Typed Concurrent Separation Logic
Speaker: Aymeric Fromherz (Inria Paris)
Time: Nov 16th, Tuesday, 4:00 pm Eastern Time
Abstract: Modern software increasingly exploits parallelism to reach new heights of performance. Unfortunately, concurrent programming is error-prone, and developers often make incorrect assumptions about how their programs will behave, raising concerns about its use in critical systems. Using formal methods to provide strong correctness guarantees is appealing, but challenging; verification frameworks either lack the expressivity required to model every advanced low-level pattern found in real-world implementations, or they do not retain the level of automation needed to ensure the scalability of verification. To address this issue, we present Steel, a new verification framework to develop and prove concurrent programs embedded in F*, a dependently typed programming language and proof assistant.
In this talk, we give an overview of Steel from the ground up.
To reason about programs, Steel provides a higher-order, impredicative concurrent separation logic with support for dynamically-allocated invariants and partial commutative monoids (PCMs). To automate verification, Steel separates verification conditions between separation logic predicates and first-order logic encodeable predicates; we develop a (partial) decision procedure using efficient, reflective tactics that focuses on the former, while the latter can be encoded efficiently to SMT by F*. We will conclude by presenting several verified Steel libraries, including mutable, self-balancing trees as well as a novel PCM-based encoding of 2-party dependently typed sessions, that illustrate the expressiveness and programmability of Steel.
Expanding the Reach of Fuzzing
Speaker: Caroline Lemieux (Microsoft Research)
Time: Nov 16th, Tuesday, 4:00 pm Eastern Time
Abstract: Software bugs are pervasive in modern software. As software is integrated into increasingly many aspects of our lives, these bugs have increasingly severe consequences, both from a security (e.g. Cloudbleed, Heartbleed, Shellshock) and cost standpoint. Fuzzing refers to a set of techniques that automatically find bug-triggering inputs by sending many random-looking inputs to the program under test. In this talk, I will discuss how, by identifying core under-generalized components of modern fuzzing algorithms, and building algorithms that generalize or tune these components, I have expanded the application domains of fuzzing. First, by building a general feedback-directed fuzzing algorithm, I enabled fuzzing to consistently find performance and resource consumption errors. Second, by developing techniques to maintain structure during mutation, I brought fuzzing exploration to “deeper” program states. Third, by decoupling the user-facing abstraction of random input generators from their sampling distributions, I built faster validity fuzzing and even tackled program synthesis. Finally, I will discuss the key research problems that must be tackled to make fuzzing readily-available and useful to all developers.
Bio: Caroline Lemieux is a Postdoc at Microsoft Research and incoming Assistant Professor at the University of British Columbia. Her research aims to help developers improve the correctness, security, and performance of large, existing software systems, ranging from complex open-source projects to industrial-scale software. Her current projects tackle these goals with a focus on fuzz testing and program synthesis. Her work on fuzz testing has been awarded an ACM SIGSOFT Distinguished Paper Award, ACM SIGSOFT Distinguished Artifact Award, ACM SIGSOFT Tool Demonstration Award, and Best Paper Award (Industry Track). She received her PhD at UC Berkeley advised by Koushik Sen, and her B.Sc. in Combined Honours Computer Science and Mathematics at UBC . She is the recipient of a Berkeley Fellowship for Graduate Study and a Google PhD Fellowship in Programming Technologies and Software Engineering.
RustBelt: A deep dive into the Abyss
Speaker: Ralf Jung (MIT)
Time: Dec 07th, Tuesday, 4:00 pm Eastern Time
Abstract: Rust is a young systems programming language that aims to fill the gap between high-level languages — which provide strong static guarantees like memory and thread safety — and low level languages — which give the programmer fine-grained control over data layout and memory management. This talk gives an introduction to RustBelt, a formal model of Rust’s type system, together with a soundness proof establishing memory and thread safety. The model is designed to verify the safety of a number of intricate APIs from the Rust standard library, despite the fact that the implementations of these APIs use unsafe language features. After explaining the basics of RustBelt and the general approach of semantic type safety, we will look at the safety proof of one particularly interesting Rust API: the Cell type, which seemingly breaks some of the fundamental constraints of the Rust type system by permitting mutation of shared state.
Title: The Calculus of Linear Constructions
Speaker: Robin Fu (Boston University)
Time:Dec 14th, Tuesday, 4:00 pm Eastern Time
Abstract: The Calculus of Linear Constructions (CLC) is an extension of the Calculus of Constructions (CC) with linear types. Specifically, CLC extends the predicative CC? with a hierarchy of linear universes that precisely controls the weakening and contraction of its term level inhabitants. We study the meta-theory of CLC, showing that it is a sound logical framework for reasoning about resource. We further extend CLC with rules for defining inductive linear types in the style of CIC, forming the Calculus of Inductive Linear Constructions (CILC). Through examples, we demonstrate that CILC facilitates correct by construction imperative programming and lightweight protocol enforcement. We have formalized and proven correct all major results in the Coq Proof Assistant.
| Date | Speaker | Talk Title |
| Sep 22 | Ankush Das (Carnegie Mellon University) |
Resource-Aware Session Types for Digital Contracts |
| Sep 29 | Social Time | |
| Oct 06 | Jonathan Protzenko (Microsoft Research) |
Latest advances in scaling cryptographic verification in F* |
| Oct 13 | June Wunder (Boston University) |
Agda Tutorial |
| Oct 20 | Assaf Kfoury (BU) |
First-Order Term Rewriting (compressed tutorial) |
| Oct 27 | Ben Greenman (Northeastern University) |
Complete Monitoring for Gradual Types |
| Nov 03 | Mirai Ikebuchi (MIT) |
Homological Methods in Rewriting |
| Nov 10 | Justin Hsu (University of Wisconsin – Madison) |
A Separation Logic for Probabilistic Independence |
| Nov 17 | Paul Downen (University of Oregon) |
Kinds Are Calling Conventions: Intensional Static Polymorphism |
| Nov 24 | Zoe Paraskevopoulou (Northeastern University) |
Compositional Optimizations for CertiCoq |
| Dec 1 | Stephanie Balzer (Carnegie Mellon University) |
Manifest Deadlock-Freedom for Shared Session Types |
| Dec 8 | Clément Pit-Claudel (MIT) |
Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs |
| Dec 15 | Andrej Dudenhefner (Saarland University) | Tamed and Mechanized: Undecidability of System F Typability and Type Checking |
Abstracts
Speaker: Andrej Dudenhefner (Saarland University)
Title: Tamed and Mechanized: Undecidability of System F Typability and Type Checking
Abstract: The undecidability of both typability and type checking for System F (second-order lambda-calculus) was established by Wells in the late 1990s [1]. After months of experience failing to mechanize the original 40 page argument in the Coq proof assistant, a new, simpler argument emerged. This talk will give an overview over the following results:
1) Simpler undecidability proof for System F typability and type checking,
2) Constructive mechanization (in the Coq proof assistant) of many-one, reductions from Turing machine halting to System F typability, type checking, and inhabitation using the Coq Library of Undecidability Proofs [2].
[1] Wells, Joe B. “Typability and type checking in System F are equivalent and undecidable.” Annals of Pure and Applied Logic 98.1-3 (1999): 111-156.
[2] https://github.com/uds-psl/coq-library-undecidability
Speaker: Clément Pit-Claudel (MIT)
Title: Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
Abstract: We present an original approach to sound program extraction in a proof assistant, using syntax-driven automation to derive correct-by-construction imperative programs from nondeterministic functional source code. Our approach does not require committing to a single inflexible compilation strategy and instead makes it straightforward to create domain-specific code translators. In addition to a small set of core definitions, our framework is a large, user-extensible collection of compilation rules each phrased to handle specific language constructs, code patterns, or data manipulations. By mixing and matching these pieces of logic, users can easily tailor extraction to their own domains and programs, getting maximum performance and ensuring correctness of the resulting assembly code.
Using this approach, we complete the first proof-generating pipeline that goes automatically from high-level specifications to assembly code. In our main case study, the original specifications are phrased to resemble SQL-style queries, while the final assembly code does manual memory management, calls out to foreign data structures and functions, and is suitable to deploy on resource-constrained platforms. The pipeline runs entirely within the Coq proof assistant, leading to final, linked assembly code with overall full-functional-correctness proofs in separation logic.
Speaker: Stephanie Balzer (Carnegie Mellon University)
Title: Manifest Deadlock-Freedom for Shared Session Types
Abstract: Shared session types generalize the Curry-Howard correspondence between intuitionistic linear logic and the session-typed pi-calculus with adjoint modalities that mediate between linear and shared session types, giving rise to a programming model where shared channels must be used according to an acquire-release discipline. The resulting language recovers the expressiveness of the untyped asynchronous pi-calculus and accommodates practical programming scenarios, such as shared servers, file systems etc. The resulting language is implemented as a prototype in C0 (a safe subset for C used to teach freshmen at CMU) and as a DSL in Rust (https://github.com/maybevoid/ferrite).
The generalization, however, comes at the cost of deadlock-freedom, a property which holds for the purely linear fragment. In this talk, I report on recent work that makes up for this deficiency and introduces a type system of linear and shared session types in which the adjoint modalities are complemented with possible worlds to rule out cyclic dependencies between acquires and synchronizations. I distill the key abstractions to reason about cyclic dependencies and the key invariants enforced by the type system to guarantee deadlock-freedom. Time permitted, I report on ongoing work that also uses possible world modalities for type-based verification of program properties of interest.
Bio: Stephanie Balzer is a research faculty in the Principles of Programming group in the Computer Science Department at Carnegie Mellon University. Stephanie obtained her PhD from ETH Zurich under the supervision of Thomas R. Gross. In her PhD work, Stephanie developed the sequential relationship-based programming language Rumer and an invariant-based verification technique for Rumer. Stephanie’s current work focuses on the development of type systems and logics for verifying properties of concurrent programs.
Speaker: Zoe Paraskevopoulou (Northeastern University)
Title: Compositional Optimizations for CertiCoq
Abstract: In this talk I will present the verified, optimizing middle-end pipeline for CertiCoq, a compiler from Gallina (Coq’s specification language) to C. The middle-end optimizes and closure-converts an untyped functional intermediate language (ANF or CPS) to a subset of that language without nested functions, which can easily be code-generated to low-level languages. The pipeline is a sequence of small, efficient transformation passes that are implemented and verified in Coq. Our novel refactoring of these transformations allows us to express more complex optimizations as a composition of small passes that have simpler implementations, simpler specifications, and simpler proofs.
The pipeline comes with an end-to-end theorem that covers both whole-program and separate compilation, even when different modules are compiled with different optimizations (using the same intermediate languages). We accomplish this lightweight compositional compiler correctness using a new technique to compose logical-relation proofs. Additionally, we use a novel technique to prove divergence preservation — even for transformations that reduce the number of steps the programs take.
Speaker: Paul Downen (University of Oregon)
Title: Kinds Are Calling Conventions: Intensional Static Polymorphism
Abstract: System F has served as the workhorse for compiling typed programming
languages for many years. It provides a logical foundation for
polymorphism (i.e., generics) in programming languages. When extended
with common basic features (like data types), System F serves as a
practical core language used en route during the compilation process.
Many convenient, complex, user-facing features given to programmers
can be desugared into basic primitives — expressed in System F —
which greatly aids in optimizations and lower-level code generation.
And yet, from the perspective of systems programming, System F is
impractical. Systems languages enable programmers to write efficient
software by giving them fine-grained control over bare-metal
implementation details used in the machine, such as the layout of data
structures in memory, or the way in which they are passed to and from
functions. Sadly, these kind of important intensional details seem
incompatible with System F’s polymorphism: modern machines have many
specialized instructions, registers, etc., for working with different
types of primitives, but real generic code must work the same way with
truly anything.
In this talk, I’ll present a long line of work, begun almost 30 years
ago, for reconciling the tension between machine primitives and System
F’s static polymorphism. The goal is the development of intermediate
languages — the midway point in modern compiler pipeline between
source code and target assembly — which are useful for distilling
complex programming languages as well as enabling compiler-driven
optimizations. Throughout the past three decades, approaches have
been taken to improve optimizations by extending System F with
low-level details about how data is represented (such as boxed or
unboxed) and functions are called (such as by-value or by-reference),
which requires refinements to its notion of static polymorphism. And
I will show you how, in the end, they all reach the same conclusion:
kinds are calling conventions.
Speaker: Justin Hsu (UW)
Title: A Separation Logic for Probabilistic Independence
Abstract: Probabilistic independence is a basic concept for describing the result of random sampling—a fundamental operation in all probabilistic programs—and for reasoning about groups of random variables. Nevertheless, existing verification methods handle independence poorly, if at all. We will introduce a probabilistic separation logic called PSL, where separation models probabilistic independence, based on a new, probabilistic model of the logic of bunched implications (BI). The program logic PSL is capable of verifying information-theoretic security of cryptographic constructions for several well-known tasks, including private information retrieval, oblivious transfer, secure multi-party addition, and simple oblivious RAM, while reasoning solely in terms of independence and uniformity. If time permits, we will also discuss ongoing work for reasoning about conditional independence.
Speaker: Mirai Ikebuchi (MIT)
Title: Homological Methods in Rewriting
Abstract: It is well-known that some equational theories such as groups or boolean algebras can be defined by fewer equational axioms than the original axioms. However, it is not easy to determine if a given set of axioms is the smallest or not. In this talk, we will see a way to find a lower bound of the number of axioms. The inequality that gives the lower bound is obtained by analyzing the algebraic structure, called the homology group, associated with the given equational theory. I will explain how equational theories and rewriting systems relate to abstract algebra, what homology groups in general settings are like, and what the homology groups of equational theories give us.
Speaker: Ben Greenman (Northeastern University)
Title: Complete Monitoring for Gradual Types
Abstract: In a gradual language, type soundness guarantees the safety of typed code; when untyped code fails to respect types, a runtime check finds the discrepancy. As for untyped code, type soundness makes no promises. Soundness does not protect untyped code from mistakes in type specifications and unwarranted blame.
What protects untyped code? To address the asymmetry, we adapt complete monitoring from the contract world to gradual typing. Complete monitoring leads to a guarantee that catches problems with faulty type specifications and helps tell apart the many designs in the gradual typing literature.
Speaker: Assaf Kfoury (BU)
Title: First-Order Term Rewriting (compressed tutorial)
Abstract: Term rewriting is an important computational model with applications in software engineering, declarative programming, and automated theorem proving. In term rewriting, computation is achieved by directed equations and pattern matching. In this tutorial we present basic notions and results, including confluence (weak and strong), normalization (weak and strong), and various other related properties and how they interact. We conclude with a very brief exposition of critical pairs and completion procedures. Throughout we aim to stress the deep connections between equational reasoning and term rewriting. We precisely define all these notions and accompany them with numerous motivating examples.
This tutorial provides a partial background for Mirai Ikebuchi’s lecture on November 3: Homological Methods in Rewriting.
Speaker: Jonathan Protzenko (Microsoft Research)
Title: Latest advances in scaling cryptographic verification in F*
Abstract: Project Everest is a large-scale verification effort that aims to verify an entire TLS stack from the ground up. In the journey to a fully verified protocol, several projects have gained a life of their own. In particular, all of the core cryptographic components are now packaged in a library called EverCrypt, which offers vectorized algorithms, assembly optimized versions, and high-level APIs that offer multiplexing, agility and automatic CPU autodetection.
In this talk, I will give an overview of EverCrypt and Project Everest. I will then reflect on the lessons we have learned since the first version of our cryptographic library nearly 5 years ago, and how we managed to scale up to 17 algorithms and nearly 40 implementations. The talk will cover language techniques and general proof design and engineering.
Speaker: Ankush Das (Carnegie Mellon University)
Title: Resource-Aware Session Types for Digital Contracts
Abstract: While there exist several successful techniques for supporting programmers in deriving static resource bounds for sequential code, analyzing the resource usage of message-passing concurrent processes poses additional challenges. To meet these challenges, this talk presents an analysis for statically deriving worst-case bounds on the computational complexity of message-passing processes, respectively. The analysis is based on novel resource-aware session types that describe resource contracts by allowing both messages and processes to carry potential and amortize cost. The talk then applies session types to implement digital contracts. Digital contracts are protocols that describe and enforce execution of a contract, often among mutually distrusting parties. Programming digital contracts comes with its unique challenges, which include describing and enforcing protocols of interaction, analyzing resource usage and tracking linear assets. The talk presents the type-theoretic foundations of Nomos, a programming language for digital contracts whose type system addresses the aforementioned domain-specific requirements. To express and enforce protocols, Nomos is based on shared binary session types rooted in linear logic. To control resource usage, Nomos uses resource-aware session types and automatic amortized resource analysis, a type-based technique for inferring resource bounds. To track assets, Nomos employs a linear type system that prevents assets from being duplicated or discarded. The talk concludes with future work directions on designing an efficient implementation for Nomos and making it robust to attacks from malicious entities.
Bio:
Ankush Das is a final year PhD student at Carnegie Mellon University. He is advised by Prof. Jan Hoffmann. He is broadly interested in programming languages with a specific focus on resource analysis, session types and language design for smart contracts on the blockchain. He is the lead designer and developer of Nomos, a domain-specific language for implementing smart contracts based on resource-aware session types. In the past, he has worked jointly with Prof. Frank Pfenning and his advisor on designing resource-aware session types for parallel complexity analysis of concurrent programs implemented in a programming language called Rast. Before joining CMU, he worked as a Research Fellow at Microsoft Research, India with Akash Lal where he developed an efficient method to perform precise alias analysis for C and C++ programs for Windows driver modules to automatically infer safe null pointer dereferences. He completed his undergraduate at IIT Bombay, India in 2014 where he worked with Prof. Supratik Chakraborty and Prof. Akshay S on deciding termination of linear loop programs.
Spring-Summer 2020
Below is a list of seminar dates for Spring-Summer 2020 with information on the speakers:
| Date | Speaker | Talk Title |
| Jan 28 | Alley Stoughton (Boston University) |
You Sank My Battleship! A Case Study in Secure Programming |
| Feb 4 | Chris Casinghino (Draper Labs) |
A Language for Programmable Hardware Security |
| Feb 11 | Ugo Dal Lago (University of Bologna) |
Differential Program Semantics |
| Feb 18 | Riyadh Baghdadi (MIT) |
Building Compilers for High Performance Code Generation |
| Feb 25 | Maximiliam Algehed (Chalmers University) | Simple Noninterference from Parametricity |
| Mar 3 | No Talk | No Talk |
| Mar 10 | Spring Break | |
| Mar 17 | Mark Lemay (Boston University) |
Dependent Types to Support Continuous Offline Testing |
| Mar 24 | Aaron Bembenek (Harvard University) |
Formulog: Datalog for SMT-based Static Analysis |
| Mar 31 | No Talk | No Talk |
| Apr 7 | Marco Gaboardi (Boston University) |
Bounded Linear Logic and Metric Interpretation |
| Apr 14 | No Talk | No Talk |
| Apr 21 | Joseph Tassarotti (Boston College) |
Verifying Concurrent Randomized Programs |
| Apr 28 | Eric Koskinen (Stevens Institute of Technology) |
Reducing Commutativity Verification to Reachability with Differencing Abstractions |
| May 5 | Aleks Nanevski (Imdea Software Institute) |
Type and proof structures for concurrency – part 1 |
| May 12 | Aleks Nanevski (Imdea Software Institute) |
Type and proof structures for concurrency – part 2 |
| May 19 | Arthur Azevedo de Amorim (Carnegie Mellon University) |
Reconciling Noninterference and Gradual Typing |
| May 26 | Aaron Weiss (Northeastern University) |
Oxide: The Essence of Rust |
| June 2 | Anitha Gollamudi (Harvard University) |
Information Flow Control for Distributed Trusted Execution Environments |
| June 9 | Stephen Chang (Northeastern University) |
Improving Software Development via (Typed) Language Tailoring |
| June 16 | Paolo Perrone (MIT) |
Monads, partial evaluations, and rewriting |
| June 23 | Michael Greenberg (Pomona College) |
Executable Formal Semantics for the POSIX Shell |
| June 30 | Anindya Banerjee (NSF) |
Incorrectness Logic |
| July 7 | Anindya Banerjee (NSF) |
Incorrectness Logic |
Abstracts
Speaker: Alley Stoughton (BU)
Title: You Sank My Battleship! A Case Study in Secure Programming
Abstract: We report on a case study in secure programming, focusing on the design, implementation and auditing of programs for playing the board game Battleship. We begin by precisely defining the security of Battleship programs, borrowing ideas from theoretical cryptography. We then consider three implementations of Battleship: one in Concurrent ML featuring a trusted referee; one in Haskell/LIO using information flow control to avoid needing a trusted referee; and one in Concurrent ML using access control to avoid needing such a referee. All three implementations employ data abstraction in key ways.
Based upon:
* Alley Stoughton, Andrew Johnson, Samuel Beller, Karishma Chadha, Dennis Chen, Kenneth Foner, Michael Zhivich:
You Sank My Battleship!: A Case Study in Secure Programming. PLAS@ECOOP 2014: 2
Speaker: Chris Casinghino (Draper Labs)
A Language for Programmable Hardware Security
Abstract: Hardware security mechanisms have struggled to keep up with the rapidly changing security landscape. Hardware is time-consuming to design, and its fixed nature makes it challenging to adapt to new threats. Modern tagged architectures solve this problem by enforcing general software-defined security policies. Policies define what information is stored in the tags and what rules the architecture enforces relative to this information (e.g., data tagged as confidential should not be sent over the network). However, this introduces new questions: What tools should we use to build these software-defined policies? How can we be confident that these policies enforce the security and safety properties we are interested in? This talk examines these questions in the context of a general-purpose security mechanism that extends existing processors with software-defined tag processing. We describe the language we use to define tag-based policies, and related research.
Speaker: Ugo Dal Lago (University of Bologna)
Differential Program Semantics
Abstract: Giving meaning to programs through axiomatic, denotational, and operational semantics is one of the main goals of theoretical computer science since its early days. Traditionally, program semantics is built around notions of program equivalence and refinement, based on which verification and transformation techniques can be justified. More and more often, however, programs are substituted with approximately equivalent programs, or verified against imprecise specifications. Program semantics has started dealing with program differences only in recent years, through the interpretation of programs in metric spaces. We give a brief survey about the state of the art on program semantics, and argue about the inadequacy of metrics as a way to deal with program differences. We thus point at a few preliminary results on a new kind of differential program semantics: logical relations, bisimilarity, and game semantics.
Speaker: Riyadh Baghdadi (MIT)
Building Compilers for High Performance Code Generation
Abstract: This talk is about building compilers for high performance code generation. It has three parts. The first part is about Tiramisu (http://tiramisu-compiler.org/), a polyhedral compiler designed for generating highly efficient code for multicores and GPUs. It is the first polyhedral compiler that can match the performance of highly hand-optimized industrial libraries such as Intel MKL and cuDNN. The second part is about applying Tiramisu to accelerate deep learning (DNN) inference. In comparison to other DNN compilers, Tiramisu has two unique features: (1) it supports sparse DNNs; and (2) it can express and optimize general RNNs (Recurrent Neural Networks). The third part will present recent work on the problem of automatic code optimization. In particular, it will focus on using deep learning to build a cost model to explore the search space of code optimizations.
Speaker: Maximiliam Algehed (Chalmers University)
Simple Noninterference from Parametricity
Abstract: We revisit the connection between parametricity and noninterference. Our primary contribution is a proof of noninterference for a polyvariant variation of the Dependency Core Calculus of in the Calculus of Constructions. The proof is modular: it leverages parametricity for the Calculus of Constructions and the encoding of data abstraction using existential types. This perspective gives rise to simple and understandable proofs of noninterference from parametricity. All our contributions have been mechanised in the Agda proof assistant.
Speaker: Mark Lemay (Boston University)
Dependent Types to Support Continuous Offline Testing
Speaker: Aaron Bembenek (Harvard University)
Formulog: Datalog for SMT-based Static Analysis
Many static analyses are based around satisfiability modulo theories (SMT) solving; examples include symbolic execution, refinement type checking, and forms of model checking. This talk presents Formulog, a domain-specific language that makes it possible to write a range of SMT-based static analyses in a way that is both close to their formal specifications and amenable to high-level optimizations and efficient evaluation. Formulog is an extension of the logic programming language Datalog with a first-order fragment of ML and mechanisms for representing and reasoning about SMT formulas; a novel type system supports the construction of expressive formulas, while ensuring that neither normal evaluation nor SMT solving goes wrong. Our case studies demonstrate that a diverse range of SMT-based analyses can naturally and concisely be encoded in Formulog, and that — thanks to this encoding — high-level Datalog-style optimizations can be automatically and advantageously applied to these analyses.
Speaker: Marco Gaboardi (Boston University)
Bounded Linear Logic and Metric Interpretation
In this talk I will present the basic ideas of linear logic (in its intuitionistic version), for then connecting them with the idea of bounded linear logic. I will then show how we can give to bounded linear logic an interesting metric interpretation.
Speaker: Joseph Tassarotti (Boston College)
Verifying Concurrent Randomized Programs
Despite continued progress in program verification, many fundamental data structures and algorithms remain difficult to verify. Challenges arise when programs use concurrency or randomization because these effects lead to non-deterministic behavior. Although many specialized logics have been developed to reason about programs that use either concurrency or randomization, most can only handle the use of one of these features in isolation. However, many common concurrent data structures are randomized, making it important to consider the combination.
This talk will describe Polaris, a logic for reasoning about programs that are both concurrent and randomized. Polaris combines ideas from three separate lines of work: (1) Varacca and Winskel’s denotational model of non-determinism and probability, (2) Barthe et al.’s approach to probabilistic relational reasoning via couplings, and (3) higher-order concurrent separation logic, as realized in the Iris verification framework.
Bio: Joseph Tassarotti is an assistant professor at Boston College. Previously, he was a postdoctoral associate in the Parallel and Distributed Operating Systems group at MIT. He received his Ph.D. from Carnegie Mellon University, where he was advised by Robert Harper.
Speaker: Eric Koskinen (Stevens Institute of Technology)
Reducing Commutativity Verification to Reachability with Differencing Abstractions
Commutativity of data structure methods is of ongoing interest, with roots in the database community. In recent years commutativity has been shown to be a key ingredient to enabling multicore concurrency in contexts such as parallelizing compilers, transactional memory, speculative execution and, more broadly, software scalability. Despite this interest, it remains an open question as to how a data structure’s commutativity specification can be verified automatically from its implementation.
I will describe our recent work on techniques to automatically prove the correctness of method commutativity conditions from data structure implementations. We introduce a new kind of abstraction that characterizes the ways in which the effects of two methods differ depending on the order in which the methods are applied, and abstracts away effects of methods that would be the same regardless of the order. I’ll then discuss a novel algorithm that reduces the problem to reachability, so that off-the-shelf program analysis tools can perform the reasoning necessary for proving commutativity. Finally, I’ll describe CityProver: a proof-of-concept commutativity verifier and some experimental results on ADTs such as a memory cell, counter, two-place Set, array-based stack, queue, and a rudimentary hash table. I’ll conclude with a discussion of what makes a data structure’s commutativity provable with today’s tools and what needs to be done to prove more in the future.
Arxiv: https://arxiv.org/abs/2004.08450
Joint work with Kshitij Bansal
Speaker: Aleks Nanevski (Imdea Software Institute)
Type and proof structures for concurrency
The main challenge of concurrent software verification has always been in achieving modularity, i.e., the ability to divide and conquer the correctness proofs with the goal of scaling the verification effort.
Types are a formal method well-known for its ability to modularize programs, and in the case of dependent types, the ability to modularize and scale complex mathematical proofs.
In this talk I will present our recent work towards reconciling dependent types with shared memory concurrency, with the goal of achieving modular proofs for the latter. Applying the type-theoretic paradigm to concurrency has lead us to view separation logic as a type theory of state, and has motivated novel abstractions for expressing concurrency proofs based on the algebraic structure of a resource and on structure-preserving functions (i.e., morphisms) between resources.
Speaker: Arthur Azevedo de Amorim (Carnegie Mellon University)
Reconciling Noninterference and Gradual Typing
One of the standard correctness criteria for gradual typing is the dynamic gradual guarantee, which ensures that loosening type annotations in a program does not affect its behavior in arbitrary ways. Though natural, prior work has pointed out that the guarantee does not hold of any gradual type system for information-flow control. Toro et al.’s GSL Ref language, for example, had to abandon it to validate noninterference.
We show that we can solve this conflict by avoiding a feature of prior proposals: type-guided classification, or the use of type ascription to classify data. Gradual languages require run-time secrecy labels to enforce security dynamically; if type ascription merely checks these labels without modifying them (that is, without classifying data), it cannot violate the dynamic gradual guarantee. We demonstrate this idea with GLIO, a gradual type system based on the LIO library that enforces both the gradual guarantee and noninterference, featuring higher-order functions, general references, coarse-grained information-flow control, security subtyping and first-class labels. We give the language a domain-theoretic semantics, using Pitts’ framework of relational structures to prove noninterference and the dynamic gradual guarantee.
Speaker: Aaron Weiss (Northeastern University)
Oxide: The Essence of Rust
Rust claims to advance industrial programming by bridging the gap between
low-level systems programming and high-level application
programming. At the heart of the argument that this enables programmers to build
more reliable and efficient software is the borrow checker — a novel
approach to ownership which aims to balance type system expressivity with
usability. And yet, to date there is no core type system that captures Rust’s
notion of ownership and borrowing, resulting in no foundation for research on
Rust to build upon.
In this work, we set out to capture the essence of this model of ownership by
developing a type systems account of Rust’s borrow checker. To that end, we
present Oxide, a formalized programming language close to source-level
Rust (but with fully-annotated types). This presentation takes a new view of
lifetimes as an approximation of the provenances of references,
and our type system is able to automatically compute this information through a
substructural typing judgment. We then provide the first syntactic proof of type
safety for borrow checking using progress and preservation. Oxide is a
simpler formulation of borrow checking — including recent features such as
non-lexical lifetimes — that we hope researchers will be able to use as
the basis for work on Rust.
Speaker: Anitha Gollamudi (Harvard University)
Information Flow Control for Distributed Trusted Execution Environments
Distributed applications cannot assume that their security policies will be enforced on untrusted hosts. Trusted execution environments (TEEs) combined with cryptographic mechanisms enable execution of known code on an untrusted host and the exchange of confidential and authenticated messages with it. TEEs do not, however, establish the trustworthiness of code executing in a TEE. Thus, developing secure applications using TEEs requires specialized expertise and careful auditing. This paper presents DFLATE, a core security calculus for distributed applications with TEEs. DFLATE offers high-level abstractions that reflect both the guarantees and limitations of the underlying security mechanisms they are based on. The accuracy of these abstractions is exhibited by asymmetry between confidentiality and integrity in our formal results: DFLATE enforces a strong form of noninterference for confidentiality, but only a weak form for integrity. This reflects the asymmetry of the security guarantees of a TEE: a malicious host cannot access secrets in the TEE or modify its contents, but they can suppress or manipulate the sequence of its inputs and outputs. Therefore DFLATE cannot protect against the suppression of high-integrity messages, but when these messages are delivered, their contents cannot have been influenced by an attacker.
Joint work with Owen Arden and Stephen Chong.
Speaker: Stephen Chang (Northeastern University)
Improving Software Development via (Typed) Language Tailoring
Programmers intuitively understand that specialized programming
languages make them more productive. Thus, unsurprisingly, there has
been a recent explosion of new specialized languages, many created by
software companies seeking to benefit from this productivity increase.
Despite all the new languages, however, programmers still waste effort
fighting their language each time they sit down to program, since it
is infeasible for any language to be perfectly suited for every task. Or
is it?
In this talk, I argue that this wasted effort would be better directed
towards tailoring the language to be indeed exactly what the
programmer needs. I then explain how a programmer’s tools—namely,
their programming language—can support this approach to programming.
Finally, I will present a new framework for creating tailorable
*typed* languages in this manner. The tutorial will show how the
framework makes it straightforward to implement type rules that are
modular and customizable, and can even be combined into a large system
like a proof assistant.
Speaker: Paolo Perrone (MIT)
Monads, partial evaluations, and rewriting
Monads can be interpreted as encoding formal expressions, or formal operations in the sense of universal algebra. We give a construction which formalizes the idea of “evaluating an expression partially”: for example, “2+3” can be obtained as a partial evaluation of “2+2+1”. This construction can be given for any monad, and it is linked to the famous bar construction, of which it gives an operational interpretation: the bar construction induces a simplicial set, and its 1-cells are partial evaluations.
We study the properties of partial evaluations for general monads. We prove that whenever the monad is weakly cartesian, partial evaluations can be composed via the usual Kan filler property of simplicial sets, of which we give an interpretation in terms of substitution of terms.
In terms of rewritings, partial evaluations give an abstract reduction system which is reflexive, confluent, and transitive whenever the monad is weakly cartesian.
For the case of probability monads, partial evaluations correspond to what probabilists call conditional expectation of random variables.
This is part of a work in progress on a general rewriting interpretation of the bar construction.
Joint work with Tobias Fritz (Perimeter Institute for Theoretical Physics, Canada).
References: arXiv:1810.06037 and www.paoloperrone.org/phdthesis.pdf
Speaker: Michael Greenberg (Pomona College)
Executable Formal Semantics for the POSIX Shell
The POSIX shell is a widely deployed, powerful tool for managing
computer systems. The shell is the expert’s control panel, a necessary
tool for configuring, compiling, installing, maintaining, and deploying
systems. Even though it is powerful, critical infrastructure, the POSIX
shell is maligned and misunderstood. Its power and its subtlety are a
dangerous combination.
We define a formal, mechanized, executable small-step semantics for the
POSIX shell, which we call Smoosh. We compared Smoosh against seven
other shells that aim for some measure of POSIX compliance (bash, dash,
zsh, OSH, mksh, ksh93, and yash). Using three test suites—the POSIX test
suite, the Modernish test suite and shell diagnosis, and a test suite of
our own device—we found Smoosh’s semantics to be the most conformant to
the POSIX standard. Modernish judges Smoosh to have the fewest bugs
(just one, from using dash’s parser) and no quirks. To show that our
semantics is useful beyond yielding a conformant, executable shell, we
also implemented a symbolic stepper to illuminate the subtle behavior of
the shell.
Smoosh will serve as a foundation for formal study of the POSIX shell,
supporting research on and development of new shells, new tooling for
shells, and new shell designs.
This talk will refine and extend my POPL 2020 talk with technical detail
on the POSIX shell itself, on Smoosh’s implementation, and on future
directions.
This is joint work with Austin J. Blatt, now an engineer at Puppet Labs.
Speaker: Anindya Banerjee (NSF)
Incorrectness Logic
This talk presents Peter O’Hearn’s paper “Incorrectness
Logic” (POPL 2020). In contrast to Hoare logic, incorrectness logic is
an underapproximating program logic in which one can reason
compositionally about the presence of bugs. An incorrectness triple
[p]C[epsilon:q] with presumption p, result q, and exit condition
epsilon says: every state in the result can be reached –normally
or erroneously–from some state in the presumption. The talk will
include the verification of various examples presented in O’Hearn’s
paper.