Registration [Location: 2nd floor, Hörsaalzentrum]
The registration desk will be opened from 8:30 a.m. It is located in the second floor of the building while the conference room (lecture hall HZ 10) is in the third floor of the building.
PPDP: Contributed Talks #1 [Location: HZ 10 (third floor, Hörsaalzentrum)]
José Fragoso Santos, Petar Maksimović, Théotime Grohens, Julian Dolby and Philippa Gardner
Verse: An EDSL for cryptographic primitives
Abhishek Dang and Piyush Kurur
Cryptographic primitives need high-speed implementations that are also resistant to side channel attacks. The absolute control over instructions and registers that such implementations demand makes assembly language programming a necessity. In this article, we describe Verse, a typed low-level language embedded in Coq designed specifically to generate assembly language programs for cryptographic primitives. Despite being a low-level language, the programming experience is markedly high-level: • The type system of Verse is rich enough to even prevent errors in array indexing and endian conversion. • Being embedded in Coq, we have at our disposal Gallina, the underlying functional programming language, as a macro assembler for code generation, and Ltac, the tactic language, as an automation tool for proof obligations inherent to our type system. We also provide a generic framework to formulate semantic aspects of Verse. This framework has value beyond providing an interpretation of Verse in Coq. We demonstrate this versatility by using it to localise uninitialised/clobbered variable use, and arithmetic overflows.
Coffee Break [Location: 2nd floor, Hörsaalzentrum]
PPDP: Honour and Memory of Martin Hofmann [Location: HZ 10 (third floor, Hörsaalzentrum)]
We sadly note that one of our pc members and friends, Martin Hofmann, died in January during a mountain trip close to Nikko, Japan. He is missed dearly. The session is a brief remembrance on his behalf.
Remembering Martin Hofmann: Nick Benton - Semantic Equivalence Checking for HHVM Bytecode (Invited Talk)
We describe a semantic differencing tool used to compare the bytecode generated by two different compilers for Hack/PHP at Facebook. The tool is a prover for a simple relational logic for low-level code and is used in testing, allowing developers to focus on semantically significant differences between the outputs of the old and new compilers.
PPDP: Contributed Talks #2 [Location: HZ 10 (third floor, Hörsaalzentrum)]
Nondeterministic Manifest Contracts
Yuki Nishida and Atsushi Igarashi
We study a manifest contract system-a typed calculus of higher-order contracts where contracts are tightly integrated into a refinement type system-for a functional language with nondeterministic choice. The extension is not trivial, especially in the presence of dependent function types, because a naive extension would lead to inconsistent type equivalence, which makes contract information in refinement types meaningless. To solve the problem, we propose a new kind of nondeterministic choice called coordinated choice, in which each occurrence of a choice operator is given a name and choices of the same name coordinately take the same branch. We introduce the notion of orthant that helps both intuitive understanding and the development of formal semantics of the new choice. We formalize a manifest contract system λ^H||Φ using the coordinated choice and show its basic properties of progress, type preservation, and contract satisfaction, the last of which states correctness of contracts in refinement types.
An Internalist Approach to Correct-by-Construction Compilers
Alberto Pardo, Emmanuel Gunther, Miguel Pagano and Marcos Viera
In this paper we present a methodology to organize the construction of a correct compiler, taking advantage of the power of full dependently type systems. The basic idea consists of decorating the abstract syntax of languages with their semantics, allowing to express the correctness of the compiler at type level. We show our methodology in a first small example and then explore how it can be promoted to more realistic languages, realizing that our internalistic approach is feasible for defining a correct-by-construction compiler from an imperative language with general recursion to a stack based intermediate language. We also show how this methodology can be combined with the externalist approach, compiling from the intermediate language to an assembly-like low level code and separately proving its correctness.
Lunch Break [Location: Mensa Casino]
PPDP: Invited Talk [Location: HZ 10 (third floor, Hörsaalzentrum)]
Calculating Distributions (Invited Talk)
The ways we reason about probability distributions and explore their applications have been naturally shifting: away from thoughtful proving with definitions using first principles, and towards mechanical calculation with expressions using derived principles. This talk reviews three useful operations on distributions that we have started to express using equational derivations and even to automate as program transformations. These operations are (1) to recognize a density function as belonging to a known distribution family, (2) to eliminate an unused random variable by summation or integration, and (3) to disintegrate a joint measure into a marginal and a conditional measure. It is thus promising to support probabilistic reasoning by drawing techniques from both programming languages and computer algebra. Ongoing challenges include how to handle a wide variety of container data types and generating programs, and how human guidance should interact with machine assistance.
Coffee Break [Location: 2nd floor, Hörsaalzentrum]
PPDP: Most Influential Paper 10-year Award and Contributed Talks #3 [Location: HZ 10 (third floor, Hörsaalzentrum)]
Most influential paper 10-year award: Programming with proofs and explicit contexts
Brigitte Pientka and Joshua Dunfield
On Intersection Types and Probabilistic Lambda Calculi
Flavien Breuvart and Ugo Dal Lago
We define two intersection type systems for the pure, untyped, probabilistic lambda-calculus, and prove that type derivations precisely reflect the probability of convergence of the underlying term. We first define a simple system of oracle intersection types in which derivations are annotated by binary strings and the probability of termination can be computed by combining all the different possible annotations. Although inevitable due to recursion theoretic limitations, the fact that (potentially) infinitely many derivations need to be considered is of course an issue when seeing types as a verification methodology. We thus develop a more complex system: the monadic intersection type system. In this second system, the probability of termination of a term is shown to be the least upper bound of the weights of its type derivations.
Sequential and Parallel Improvements in a Concurrent Functional Programming Language
Manfred Schmidt-Schauss, David Sabel, and Nils Dallmeyer
We propose a model for measuring the runtime of concurrent programs by the minimal number of evaluation steps. The focus of this paper are improvements, which are program transformations that improve this number in every context, where we distinguish between sequential and parallel improvements, for one or more processors, respectively. We apply the methods to CHF, a model of Concurrent Haskell extended by futures allowing declarative implementations of concurrent programs. The language CHF is a typed higher-order functional language with concurrent threads, monadic IO and MVars as synchronizing variables. We show that all deterministic reduction rules and several further useful program transformations are sequential and parallel improvements.
Pattern Matching and Fixed Points: Resources Types and Strong Call-By-Need
Pablo Barenbaum, Eduardo Bonelli and Kareem Mohamed
Resource types are types that statically quantify some aspect of program execution. They come in various guises; this paper focusses on a manifestation of resource types known as non-idempotent intersection types. We use them to characterize weak normalisation for a type-erased lambda calculus for the Calculus of Inductive Construction (λe), as introduced by Gregoire and Leroy. The λe calculus consists of the lambda calculus together with constructors, pattern matching and a fixed-point operator. The characterization is then used to prove the completeness of a strong call-by-need strategy for λe. This strategy operates on open terms: rather than having evaluation stop when it reaches an abstraction, as in weak call-by-need, it computes strong normal forms by admitting reduction inside the body of abstractions and substitutions. Moreover, argument evaluation is by-need: arguments are evaluated when needed and at most once. Such a notion of reduction is of interest in areas such as partial evaluation and proof-checkers such as Coq.