TutorialFestPOPL 2018

POPL 2018 TutorialFest will be on Monday, 8 January 2018.

This year POPL TutorialFest will consist of 8 tutorials (4 in the morning and 4 in the afternoon) of 3 hours each.

Morning Session

• Message-Passing Concurrency and Substructural Logics. Slides - Live-coded examples - as a zip file. Frank Pfenning, Carnegie Mellon University.
• Code Obfuscation - a Hacking view on program analysis and understanding. Slides. Roberto Giacobazzi, University of Verona and IMDEA SW Institute.
• Equational reasoning for probabilistic programming. Handout. Chung-chieh Shan, Indiana University.
• Programming and Reasoning with Infinite Data in Isabelle/HOL. Tutorial material Mathias Fleury, MPI-INF and Andreas Lochbihler, ETH Zurich and Andrei Popescu, Middlesex University London.

Afternoon Session

• Introduction to Algebraic Program analysis. Slides 1 (Kincaid) - Slides 2 (Reps) - Zachary Kincaid, Princeton University and Thomas Reps, University of Wisconsin.
• Computational Higher Type Theory. Slides - Robert Harper and Carlo Angiuli, Carnegie Mellon University.
• Iris - A Modular Foundation for Higher-Order Concurrent Separation Logic. Code Jacques-Henri Jourdan, LRI, CNRS, Univ. Paris Sud and Robbert Krebbers, Delft University.
• One Weird Trick: Relational Interpreters for Program Synthesis. Code - William E. Byrd, Gregory Rosenblatt, University of Alabama at Birmingham.

Abstracts and Biosketches

Message-Passing Concurrency and Substructural Logics. Frank Pfenning, Carnegie Mellon University.

Functional programming has been revolutionized by our understanding of its connection to intuitionistic logic and type theory. In this tutorial we report on the progress of a long-term effort to provide a similar logical underpinning for message-passing concurrent programming. We show how substructural logics give rise to session types characterizing communication, and how substructural proofs can be interpreted as processes. Program examples will focus on recent progress on incorporating sharing of resources, such as shared queues, the classic dining philosophers problem, and a representation of the untyped asynchronous pi-calculus.

Biographical Information

Frank Pfenning is Joseph F. Traub Professor and Head of the Computer Science Department at Carnegie Mellon University. He obtained his PhD in Mathematics at Carnegie Mellon University in 1987. He served as trustee and president of CADE, chaired several conferences and program committees including FoSSaCS 2013, LICS 2008, CADE 2007, and RTA 2006, and served on the editorial board of TCS, JAR, and JSC, and was named Fellow of the ACM in 2015. His current research interests include expressive type systems for functional, concurrent, and logic programming languages, computer security, logical frameworks, and automated deduction.

Code Obfuscation - a Hacking view on program analysis and understanding. Roberto Giacobazzi, University of Verona and IMDEA SW Institute.

The tutorial is intended to present the most recent achievements in code protecting methods and technologies, ranging from code obfuscation to tamper proofing technique, in a programming languages way. The battle scenario involves attackers intended to extract information by reverse engineering the code, and protecting code transformations modelled as distorted compilers devoted to inhibit these attacks. Attacks are inhibited by maximising imprecision in all attempts made by the attacker to exploit control and data- flow of the obscured code. After a brief survey on the state of the art in the field, we introduce a model for code obfuscation which is general enough to include generic automated static and dynamic attacks. Protecting transformations are then systematically and formally derived as distorted compilers, obtained by specialising a suitably distorted interpreter for the given programming language with respect to the source code to protect. Interestingly this distortion corresponds precisely to defeat the potency of the expected attacker, which is itself an interpreter and whose potency consists in its ability to extract a complete and precise view of program’s execution.

Biographical Information

Roberto Giacobazzi received the Ph.D. in Computer Science from the University of Pisa in 1993. From 1993 to 1995 he had a Post Doctoral Research position at Laboratoire d’Informatique (LIX), Ecole Polytechnique (Paris) in the equipe Cousot. From 1995 to 1998 he was (tenured) Assistant Professor in Computer Science at the University of Pisa. From 1998 to 2000 he was Associate Professor at the University of Verona. From May 2000 until now he is Full Professor in Computer Science at the University of Verona. The research interests of Roberto Giacobazzi include abstract interpretation, static program analysis, semantics of programming languages, program verification, abstract model-checking, program transformation and optimisation, digital asset protection, code obfuscation, software watermarking and lattice theory. In the last 10 years he has been visiting scientist at: MSR, U. of Louisiana, IMDEA SW Institute, Irdeto Corp. Canada, U. of Melbourne, Ecole Normale Supériéure, Imperial College, U. of Manoa, and U. Complutense de Madrid.

Equational reasoning for probabilistic programming. Chung-chieh Shan, Indiana University.

Equations on programs are used to express domain knowledge, verify correctness, and improve performance, by people such as programmers and by tools such as compilers. It turns out that equations on probabilistic programs are a particularly good way to express Bayesian inference, verify distribution correctness, and improve sampler performance. In this way, this tutorial will introduce the mathematical reasoning principles that practitioners of probabilistic reasoning use to turn declarative models into efficient algorithms. These principles include integration and conjugacy, density and conditioning, and detailed balance.

Biographical Information

Chung-chieh Shan is an assistant professor of computer science at Indiana University. He is an avid researcher and wishful user of probabilistic programming languages who always tries to line up executable formalisms and the human concepts they represent.

Programming and Reasoning with Infinite Data in Isabelle/HOL. Mathias Fleury, MPI-INF and Andreas Lochbihler, ETH Zurich Andrei Popescu, Middlesex University London.

Recently we have endowed the proof assistant Isabelle/HOL with a powerful framework for programming with, and reasoning about, infinite objects such as streams and infinite-depth trees. It implements the paradigm of total/productive coprogramming, and is based on a modular design of coinductive datatypes. The tutorial will present this framework through examples taken from the field of programming languages.

Biographical Information

Mathias Fleury is a PhD student at MPI-INF, supervised by Jasmin Blanchette and Christoph Weidenbach. He works on the Isabelle formalization of logical systems and programming languages.

Andreas Lochbihler is a senior researcher at ETH Zurich, working on formalized programming languages and cryptography. He developed Isabelle’s widely used Coinductive library. He proved correct a compiler for a large subset of concurrent Java and built the CryptHOL framework for cryptographic security proofs. Both projects rely heavily on codatatypes and total corecursive programming.

Andrei Popescu is a senior lecturer at the Middlesex University London, working on proof assistant foundations and infrastructure and on information flow security. He designed and developed Isabelle’s codatatype and corecursion mechanisms jointly with Jasmin Blanchette and Dmitriy Traytel, and the confidentiality-verified conference management system CoCon.

Introduction to Algebraic Program analysis. Zachary Kincaid, Princeton University and Thomas Reps, University of Wisconsin.

Material from POPL 2018 tutorial ``Introduction to Algebraic Program Analysis'' (Z. Kincaid and T. Reps):
+ Part 1 (Kincaid)
+ Part 2 (Kincaid)
+ Part 3 (Reps)
+ Part 4 (Kincaid)

The purpose of program analysis is to over-approximate the run-time behavior of programs. The classical method for analyzing programs is iterative program analysis, in which one begins with some property that over-approximates (just) the initial states of the program, and repeatedly transforms the property until converging upon a property that over-approximates all of the reachable states of the program. An alternative to iterative program analysis is algebraic program analysis, in which the space of program properties forms an algebraic structure, and one computes a property that over-approximates the executions of a program by breaking it into smaller parts, analyzing each part, and then using the operations of the algebraic structure to combine the results into a property that over-approximates the execution of the whole program. The purpose of this tutorial is to provide an introduction to algebraic program analysis, and teach participants how to design program analyses in the algebraic style. The first part of the tutorial will introduce the algebraic framework, following Tarjan’s path-expression method for intraprocedural analysis. We will motivate algebraic program analysis with compositional recurrence analysis, which computes numerical loop invariants over an expressive abstract domain without requiring a widening operator. The second part of the tutorial will cover recent work on interprocedural algebraic program analysis. We will focus on a family of techniques that take inspiration from Newton’s method for finding roots of real-valued functions to compute solutions to interprocedural program-analysis problems.

Biographical Information

Zachary Kincaid is an assistant professor in the Department of Computer Science at Princeton University. Kincaid’s research focuses on program analysis and automated theorem proving. He received his Ph.D. in Computer Science from the University of Toronto in 2016. His Ph.D. disser- tation on analysis of multi-threaded programs received Honorable Mention for the ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award.

Thomas Reps is the J. Barkley Rosser Professor & Rajiv and Ritu Batra Chair in the Computer Sciences Department of the University of Wisconsin, which he joined in 1985. He is also President and co-founder of GrammaTech, Inc. Reps is the author or co-author of four books and more than one hundred ninety-five papers describing his research. His work has concerned a wide variety of topics, including dataflow analysis, abstract interpretation, program slicing, pointer analysis, model checking, computer security, code instrumentation, the use of program profiling in software testing and incremental algorithms. Professor Reps received his Ph.D. in Computer Science from Cornell University in 1982. His Ph.D. dissertation received the 1983 ACM Doctoral Dissertation Award. Reps has also been the recipient of an NSF Presidential Young Investigator Award (1986), a Packard Fellowship (1988), a Humboldt Research Award (2000), and a Guggenheim Fellowship (2000). He is also an ACM Fellow (2005). In 2013, Reps was elected a foreign member of Academia Europaea. Reps has held visiting positions at the Institut National de Recherche en Informatique et en Automatique (INRIA) in Rocquencourt, France (1982-83), the University of Copenhagen, Denmark (1993-94), the Consiglio Nazionale delle Ricerche in Pisa, Italy (2000-2001), and the Universit ́e Paris Diderot-Paris 7 (2007-2008).

Computational Higher Type Theory. Robert Harper and Carlo Angiuli, Carnegie Mellon University.

Computational type theory is a semantic formulation of dependent type theory that starts with a programming language equipped with a deterministic operational semantics and derives types as specifications of program behavior. Thus, a type is a program specification, two types are exactly equal only if they specify the same behavior, and a program inhabits a type if it behaves according to specification, and two programs are exactly equal as elements of a type when they exhibit the same specified behavior. The range of possible programs is open-ended in that no specification precludes the existence of any program, and the forms of type that may be considered are unlimited, the presence of one type never interfering with another. Among the types are those arising from logic, including the usual connectives and quantifiers. From the logical perspective computational type theory is a theory of truth, not a theory of formal proof, thereby providing a direct realization of Brouwer’s program of intuitionistic foundations for mathematics. The role of formalisms is strictly secondary, and never imposes definitional limits on the theory. Whereas computational type theory is consistent with the familiar constructs of formal type theory, it is both possible and advantageous to consider proof theories, such as refinement logics, that lie outside the scope of formal type theory. As mentioned, computational type theory has its roots in Brouwer’s program of intuitionistic mathematics in which the truth of a proposition is identified with the existence of a construction (program) that obeys the proposition as a specification. This perspective was developed by Martin-Loef in his paper “Constructive Mathematics and Computer Programming”, and was developed more fully by Constable and his co-workers in the NuPRL type theory and proof assistant. More recently, computational type theory has been extended by the authors to account for higher-dimensional phenomena (as suggested by Hofmann, Streicher, Moerdijk, Berg, Warren, Awodey, and Voevodsky), such as the identification of equivalent types, or the formation of abstract higher-dimensional objects in type theory.

The purpose of this tutorial is to present the semantics of computational higher type theory, and to relate the semantics to its implementation in the RedPRL proof development system.

Biographical Information

Robert Harper is a professor of Computer Science at Carnegie Mellon University, where he has been on faculty since 1988. He is author of the textbook Practical Foundations for Programming Languages (Cambridge, 2016).

Carlo Angiuli is a PhD student in Computer Science at Carnegie Mellon, working under the direction of Robert Harper on the semantic foundations of computational higher type theory.

Iris - A Modular Foundation for Higher-Order Concurrent Separation Logic. Jacques-Henri Jourdan, LRI, CNRS, Univ. Paris Sud and Robbert Krebbers, Delft University.

Iris is a framework for higher-order concurrent separation logic, which has been implemented in the Coq proof assistant and deployed very effectively in a wide variety of verification projects. These projects include but are not limited to: verification of fine-grained concurrent data structures, logical-relations for relational reasoning, program logics for relaxed memory models, program logics for object capabilities, and a safety proof for a realistic subset of the Rust programming language. In this tutorial, you will learn how use the Iris framework to reason about concurrent programs. This tutorial will be hands-on: we will use the Coq implementation of Iris to mechanize our proofs. It is recommended to come with Coq and Iris pre-installed on your machine so that you can play with Iris yourself.

Biographical Information

Iris is a collaborative effort between MPI-SWS (Germany), Aarhus University (Denmark), and Delft University of Technology (The Netherlands). The first session (theory) will be delivered by Jacques-Henri Jourdan and the second session (Coq) will be delivered by Robbert Krebbers. Jacques-Henri is a former post-doc researcher of the Max Planck Institute for Software Systems (MPI-SWS) in Saarbrucken, Germany, in the Foundations of Programming Group. He is now a CNRS researcher in Laboratoire de Recherche en Informatique in University Paris-Sud, France. Robbert Krebbers is an assistant professor at Delft University of Technology, Delft, The Netherlands.

One Weird Trick: Relational Interpreters for Program Synthesis. William E. Byrd, Gregory Rosenblatt, University of Alabama at Birmingham.

In an ideal world we would directly express the operational semantics or type judgements of a programming language as a high-level executable semantics. We could then perform tasks like program synthesis or type inference/type inhabitation by writing queries with variables representing “holes” in a program or a type, and letting an advanced reasoning system efficiently fill in those holes. This is the promise and challenge of relational programming, a pure form of constraint logic programming. Over the past dozen years we and our colleagues have experimented with this approach, using the relational programming language miniKanren (http://minikanren.org/). In the past two years we have applied a variety of optimizations and heuristics to the relational interpreters we use to encode an operational semantics, speeding up some synthesis queries by 9 orders of magnitude. This speed up allows us to synthesize small but interesting higher-order and recursive Racket programs, as shown in our 2017 ICFP Pearl (‘A unified approach to solving seven programming problems’, Byrd, Ballantyne, Rosenblatt, Might https://dl.acm.org/citation.cfm?id=3110252&CFID=813013760&CFTOKEN=84163595).

In this tutorial we will show how we write and extend an interpreter for a Turing-complete subset of Racket as a relation in miniKanren, and then use this relational interpreter for program synthesis. Participants will follow along in the Racket version of miniKanren, and will write their own recursive miniKanren relations, including their own relational interpreter (and relational type inferencer, time allowing). We will also discuss the philosophy of relational programming, and describe open research problems in using relational interpreters for program synthesis. We assume participants have a basic knowledge of functional programming. Familiarity with writing simple interpreters will be helpful, but is not required. No knowledge of miniKanren, relational/logic programming, or program synthesis is assumed.

Biographical Information

William Byrd is a research scientist at the University of Alabama at Birmingham. He is one of the creators of the miniKanren relational programming language, and co-author of The Reasoned Schemer, 2nd ed., with Dan Friedman, Jason Hemann, and Oleg Kiselyov. He has spent the past decade writing relational interpreters in miniKanren to perform program synthesis.

Gregory Rosenblatt is a research programmer at the University of Alabama at Birmingham. For the last year he has worked with Will Byrd on the Barliman prototype synthesis tool, which uses the relational interpreter technology explored in this tutorial (https://github.com/webyrd/Barliman). Applying various optimizations and heuristics to Barliman’s relational interpreter, Greg sped up some synthesis queries by many orders of magnitude, as will be described in the tutorial.

Talks

Call for tutorials

The 45th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2018) will be held in Los Angeles, USA.

POPL provides a forum for the discussion of fundamental principles and important innovations in the design, definition, analysis, transformation, implementation and verification of programming languages, programming systems, and programming abstractions.

Tutorials for POPL 2018 are solicited on any topic relevant to the POPL community. In particular, tutorials describing emerging topics or novel tools have been especially successful in the past.

Tutorials will be held on Monday January 8, 2016 (two days before the main conference and the day before PLMW). The expected length of a tutorial is 3 hours and, depending on the schedule, there might be the option to repeat it in the morning and in the afternoon.

Submission details

Deadline for submission: 01 September 2017 Notification of acceptance: 15 September 2017

A tutorial proposal should provide the following information.

• Tutorial title • Presenter(s), affiliation(s), and contact information • 1-3 page description (for evaluation). This should include the objectives, topics to be covered, presentation approach, target audience, prerequisite knowledge, and if the tutorial was previously held, the location (i.e. which conference), date, and number of attendees if available.
• 1-2 paragraph abstract suitable for tutorial publicity. • 1 paragraph biography suitable for tutorial publicity.

Proposal must be submitted in pdf or txt form by email to the associated events chair Marco Gaboardi (gaboardi at buffalo.edu).

The organizers may also solicit tutorials directly, as has been common in the past.