The simply-typed λ-calculus, with only function types, is strongly normalizing, and its program equivalence relation is decidable: unlike in more advanced type system with polymorphism or effects, the natural "syntactic" equivalence (βη-equivalence) corresponds to natural "semantic" equivalence (observational or contextual equivalence), and is decidable. Adding product types (pairs) is easy and preserves these properties, but sums (disjoint unions) are, surprisingly, harder. It is only in 1995 that Neil Ghani proved that the equivalence in presence of sums is decidable, and the situation in presence of the empty type (zero-ary sum) was unknown.
We propose an equivalence algorithm for sums and the empty type that takes inspiration from a proof-theoretic technique, named "focusing", designed for proof search. The exposition will be introductory; I will present the difficulties caused by sums and the empty type, present some of the existing approaches for sums in the literature, introduce focusing, and give a high-level intuition of our saturation-based algorithm and its termination argument. No previous knowledge of focusing is assumed. I expect some familiarity with typed lambda-calculi, but will recall all concepts used (for example, βη-equivalence) during the talk.
Gabriel Scherer ("gasche") is a post-doctoral researcher at Northeastern University, Boston, working with Amal Ahmed on formal aspects multi-language programming systems.
Relational program verification is a variant of program verification where one can reason about two programs and as a special case about two executions of a single program on different inputs. Relational program verification can be used for reasoning about a broad range of properties: information flow security, relative cost, sensitivity or continuity, differential privacy, etc. In a higher-order setting, relational program verification can be achieved using relational refinement type systems, a form of refinement types where assertions have a relational interpretation. Relational refinement type systems excel at relating structurally equivalent terms but provide limited support for relating terms with very different structures.
In this talk, he will present a logic, called Relational Higher Order Logic (RHOL), for proving relational properties of a simply typed λ-calculus with inductive types and recursive definitions. RHOL retains the type-directed flavor of relational refinement type systems but achieves greater expressivity through rules which simultaneously reason about the two terms as well as rules which only contemplate one of the two terms. He will present some of the property of RHOL, some examples and sound embeddings for several existing relational type systems. He will then briefly discuss two extensions of the basic RHOL for guarded recursion and for probabilistic programs.
Joint work with Alejandro Aguille, Gilles Barthe, Deepak Garg, and Pierre-Yves Strub
Marco Gaboardi is an assistant professor at the University at Buffalo, SUNY. Previously, he was a faculty at the University of Dundee, Scotland. He received his PhD from the University of Torino, Italy, and the Institute National Polytechnique de Lorraine, France. He was a visitor scholar at the University of Pennsylvania and at Harvard’s CRCS center, and recipient of a EU Marie Curie Fellowship. His research is in programming language design and implementation, and in differential privacy.
Faculty Host: Jan Hoffmann
Enumeration of graphs on surfaces (or "maps") is an active topic of research in combinatorics, with links to wide-ranging domains such as algebraic geometry, knot theory, and mathematical physics. In the last few years, it has also been found that map enumeration is related to the combinatorics of lambda calculus, with various well-known families of maps in 1-to-1 correspondence with various natural families of linear lambda terms. In the talk I will begin by giving a brief survey of these enumerative connections, then use those to motivate a closer look at the surprisingly rich topological and algebraic properties of linear lambda calculus.
Noam Zeilberger is a Birmingham Fellow in the School of Computer Science at the University of Birmingham. Previously, he held postdoctoral positions in France (Inria Saclay, Université Paris 7), Spain (IMDEA Madrid), and New Jersey (IAS Princeton), after receiving his PhD from CMU in 2009. He is interested in all aspects of logic and its interactions with mathematics and computer science.
Faculty Host: Robert Harper
In this talk, I will present my work on reasoning about concurrent programs with the Verified Software Toolchain (VST). Separation logic extends Hoare logic with ideas of memory and ownership, used to model the behavior of heap-manipulating programs. Permissions on memory are a natural way of thinking about both sequential and concurrent programs, but concurrency also brings its own challenges: how do threads communicate? Who owns a shared data structure? How can we account for relaxed memory models and low-level atomic operations? Using ideas from the newest generation of concurrent separation logics, we can come up with consistent reasoning principles for both lock-based and lock-free programs, and prove the correctness of non-blocking communication protocols and data structures. These proofs are both formalized in Coq and connected to working C code.
William Mansky is a postdoc at Princeton University working with Andrew Appel on verifying concurrent C programs. He received his PhD from the University of Illinois at Urbana-Champaign under Elsa Gunter, and spent two years working with Steve Zdancewic on the Verified LLVM (Vellvm) project. His research interests include interactive theorem proving, program semantics and correctness, compiler correctness, and concurrency.
Faculty Host: Limin Jia
Program sensitivity measures how robust a program is to small changes in its input, and is a fundamental notion in domains ranging from differential privacy to cyber-physical systems. A natural way to formalize program sensitivity is in terms of metrics on the input and output spaces, requiring that an r-sensitive function map inputs that are at distance d to outputs that are at distance at most r * d. Program sensitivity is thus an analogue of Lipschitz continuity for programs. Reed and Pierce introduced Fuzz, a functional language with a linear type system that can express program sensitivity. They show soundness operationally, in the form of a metric preservation property. Inspired by their work, we study program sensitivity and metric preservation from a denotational point of view. In particular, we introduce metric CPOs, a novel semantic structure for reasoning about computation on metric spaces, by endowing CPOs with a compatible notion of distance. This structure is useful for reasoning about metric properties of programs, and specifically about program sensitivity. We demonstrate metric CPOs by giving a model for the deterministic fragment of Fuzz.
Arthur Azevedo is graduate student in the Computer and Information Science department at the University of Pennsylvania since 2011. I work with Benjamin Pierce. My main research area is programming languages and verification. I was involved in the project of SAFE, a clean-slate computer environment aimed at security and correctness, helping with its design and specification. I am currently working on bringing some of the hardware tagging infrastructure that we developed for SAFE to more conventional processor designs, formally verifying that the mechanism can be used for enforcing interesting security policies.
Faculty Host: Jan Hoffmann
As capabilities, technology readiness and autonomy of unmanned aircraft matures, increasingly important aspects that come into consideration are these of correctness, failsafe-ness, robustness and health management. Furthermore, debugging and analysis of complex systems is an important part of development activities. Runtime monitoring of relevant properties and system requirements is a key technique to support such concepts. A suitable monitoring approach for a cyber-physical system has to be efficient and capable of supervising various specifications, possibly relating different data sources and data history. In this paper we present a formal approach for log-analysis and monitoring for the DLR ARTIS framework using a tool for the stream-based specification language LOLA, currently developed at Saarland University, for the runtime monitoring of formal specifications. The formal language is based on the concepts of linear temporal logic but is actually more expressive, for example it is possible to calculate probabilities instead of Boolean values. The formal methodology of runtime monitoring is introduced in the context of system health management, and application scenarios are detailed. The monitoring tool and its formal specification language LOLA is briefly described and the integration into the DLR ARTIS framework, phase one offline monitoring, and phase two online monitoring, is shown. Finally, examples show the benefits of using LOLA within the framework.
Florian-Michael Adolf has worked almost 15 years as a roboticist and got actively involved with many different challenges in perception, learning, planning and control. For example, he started working with camera-based object detection and autonomous transportation before he was working on real-time bision based soccer playing behaviors for a team of autonomous soccer robots (aka RoboCup). After he received my M.Sc. in Autonomous Systems in 2006, he specialized my research work in real-time sampling-based motion planning for unmanned rotocraft. Florian leads team of highly motivated researchers since 2013, who improve his initial work towards other unmanned aircraft types as well as the complex task of validation and verification thereof. Florian's daily work comprises not only technical and research work, but also international meetings with related special interest groups. But in order to keep his "feet on the ground", he tries to balance between theoretical and practical work as! well as related committee efforts. Through his work, he contributes to a better understanding as well as a feasibility analysis of approaches from various disciplines; i.e. an overall system perspective rather than a sole disciplinary one.
Sebastian Schirmer received his M.Sc. in Computer Science from Saarland University in 2016. During his studies as a research assistant he implemented the formal language LOLA that is used for monitoring approaches across different applications. With his thesis he achieved to augment athe unmanned rotorcraft guidance and control software framework with formal methods using LOLA. In particular, he applied monitoring to support the offline log-file analysis as well as online capabilities in order to enrich the information of the overall system states. This way he was able to analyze the system for assurance purposes "in-time". In 2017, he joined the German Aerospace Center (DLR) to continue working on Formal Methods and other Model-based assurance methods for unmanned aircraft.
Probabilistic couplings are a standard mathematical abstraction for reasoning about two distributions. In formal verification, they are often called probabilistic liftings. While these two concepts are quite related, the connection has been little explored. In fact, probabilistic couplings and liftings are a powerful, compositional tool for reasoning about probabilistic programs. I will give a brief survey of different uses of probabilistic liftings, and then show how to use these ideas in the relational program logic pRHL.
Joint with Gilles Barthe, Thomas Espitau, Benjamin Gregoire, and Pierre-Yves Strub.
Justin Hsu is a final year graduate student at the University of Pennsylvania, advised by Benjamin Pierce and Aaron Roth. His research interests span formal verification and theoretical computer science, including verification of randomized algorithms, differential privacy, and game theory.
Faculty Host: Matt Fredrikson
It's tempting to think that machine instructions are atomic updates to a global mutable state, of register and memory values. In the sequential world that's a good model, but concurrent contexts expose a slew of more interesting behaviour. We set out to understand real multiprocessor semantics in 2007, to give a basis for software verification. We're still not done, but we now have credible operational models for much of what goes on. I'll talk about some key points of this, including our experimental investigation and validation, the Lem and Sail metalanguages for expressing the semantics, our interactions with processor vendors, especially IBM and ARM, and work with the CHERI team on secure hardware and software. It's impacted hardware testing, architecture design, and high-level language design along the way.
This is part of the REMS project, aiming to apply semantics to improve the quality of mainstream computer systems; REMS also includes work on the C language and C/C++ concurrency model, on ELF linking, on POSIX filesystems, on the TCP and TLS network and security protocols, on the CakeML verified compiler, and on program logics. I'll start with a quick overview of REMS.
This is joint work with Shaked Flur, Susmit Sarkar, Kathryn E. Gray, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Ali Sezgin, Gabriel Kerneis, Dominic Mulligan, Anthony Fox, Robert Norton-Wright.
Peter Sewell is a Professor of Computer Science at the University of Cambridge Computer Laboratory. He held an EPSRC Leadership Fellowship from 2010-2014 and a Royal Society University Research Fellowship from 1999-2007; he took his PhD in Edinburgh in 1995, supervised by Robin Milner, after studying in Cambridge and Oxford. His research aims to build rigorous foundations for the engineering of real-world computer systems, to make them better-understood, more robust, and more secure.
Faculty Host: Robert Harper
Rust is a new systems-programming language that is becoming increasingly popular. It aims to combine C++'s focus on zero-cost abstractions with numerous ideas that emerged first in academia, most notably affine and region types ("ownership and borrowing") and Haskell's type classes ("traits"). One of the key goals for Rust is that it does not require a garbage collector.
In this talk, I'll give a brief overview of Rust's key features, with a focus on the type system. I'll talk about how we leverage a few core features to offer a variety of APIs -- ranging from efficient collections to various styles of parallel programming -- while still guaranteeing memory safety and data-race freedom.
Nicholas Matsakis is a senior researcher at Mozilla research and a member of the Rust core team. He has been working on Rust for four years and did much of the initial work on its type system and other core features. He has also done work in several just-in-time compilers as well as building high-performance networking systems. He did his undergraduate study at MIT, graduating in 2001, and later obtained a PhD in 2011, working with Thomas Gross at ETH Zurich.
Faculty Host: Stephanie Balzer
In this talk I will present Hazelnut, a structure editor based on a small bidirectionally typed lambda calculus extended with holes and an internal notion of a cursor. Existing structure editors only guarantee a weak syntactic well-formedness. Hazelnut goes one step further: the possible edit actions maintain static well-definedness. Naively, this prohibition on ill-typed edit states would force the programmer to construct terms in a rigid outside-in manner. To avoid this problem, the semantics of edit actions automatically places terms assigned a type that is inconsistent with the expected type inside a hole. This safely defers the type consistency check until the programmer finishes constructing the term inside the hole.
Hazelnut is a foundational type-theoretic account of typed structure editing, rather than an end-user tool itself. To that end, I will describe how Hazelnut's rich metatheory, which is fully mechanized in Agda, guides the definition of an extension to the calculus. I will also discuss future work considering plausible evaluation strategies for terms with holes, and reveal connections with gradual typing and contextual modal type theory. Finally, I will discuss how Hazelnut's semantics lends itself to implementation as a functional reactive program in js_of_ocaml.
Hazelnut is joint work with Cyrus Omar, Michael Hilton, Jonathan Aldrich, and Matthew Hammer.
Ian Voysey received his Bachelor's degree in Computer Science and Discrete Mathematics and Logic from Carnegie Mellon University in 2010. He helped to develop the introductory functional programming courses there, and won the inaugural A. Nico Habermann Educational Service Award for that work. His research interests are in mechanized proof, proof theory, and type theory. He is currently a Research Programmer at Carnegie Mellon University.
Faculty Host: Jonathan Aldrich