PPDP 

08:30
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. 
08:30
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. 
09:00
PPDP: Contributed Talks #1
[Chair:
Magnus Madsen • Location:
HZ 10 (third floor, Hörsaalzentrum)]
09:00
Cosette: Symbolic Execution for JavaScript
José Fragoso Santos, Petar Maksimović, Théotime Grohens, Julian Dolby and Philippa Gardner We present a new framework for trustworthy, compositional symbolic execution of JavaScript programs. Its aim is to provide generalpurpose symbolic analysis and assist developers in the testing of their code: the developer writes symbolic tests for which we provide concrete countermodels. We follow a new, general methodology for designing compositional program analyses for dynamic languages and prove that the underlying symbolic execution is sound and does not generate false positives. We establish additional trust by using the theory to precisely guide the implementation and by thorough testing. We apply our framework to wholeprogram symbolic testing of realworld JavaScript libraries and compositional debugging of separation logic specifications of JavaScript programs. 09:30
Verse: An EDSL for cryptographic primitives
Abhishek Dang and Piyush Kurur Cryptographic primitives need highspeed 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 lowlevel language embedded in Coq designed specifically to generate assembly language programs for cryptographic primitives. Despite being a lowlevel language, the programming experience is markedly highlevel: • 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. 
09:00
PPDP: Contributed Talks #1
[Chair:
Magnus Madsen • Location:
HZ 10 (third floor, Hörsaalzentrum)]
09:00
Cosette: Symbolic Execution for JavaScript
José Fragoso Santos, Petar Maksimović, Théotime Grohens, Julian Dolby and Philippa Gardner We present a new framework for trustworthy, compositional symbolic execution of JavaScript programs. Its aim is to provide generalpurpose symbolic analysis and assist developers in the testing of their code: the developer writes symbolic tests for which we provide concrete countermodels. We follow a new, general methodology for designing compositional program analyses for dynamic languages and prove that the underlying symbolic execution is sound and does not generate false positives. We establish additional trust by using the theory to precisely guide the implementation and by thorough testing. We apply our framework to wholeprogram symbolic testing of realworld JavaScript libraries and compositional debugging of separation logic specifications of JavaScript programs. 09:30
Verse: An EDSL for cryptographic primitives
Abhishek Dang and Piyush Kurur Cryptographic primitives need highspeed 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 lowlevel language embedded in Coq designed specifically to generate assembly language programs for cryptographic primitives. Despite being a lowlevel language, the programming experience is markedly highlevel: • 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. 
10:00
Coffee Break
[Location:
2nd floor, Hörsaalzentrum]

10:00
Coffee Break
[Location:
2nd floor, Hörsaalzentrum]

10:30
PPDP: Honour and Memory of Martin Hofmann
[Chair:
Philippa Gardner • 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: Semantic Equivalence Checking for HHVM Bytecode (Invited Talk)
Nick Benton 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 lowlevel code and is used in testing, allowing developers to focus on semantically significant differences between the outputs of the old and new compilers. 
10:30
PPDP: Honour and Memory of Martin Hofmann
[Chair:
Philippa Gardner • 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: Semantic Equivalence Checking for HHVM Bytecode (Invited Talk)
Nick Benton 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 lowlevel code and is used in testing, allowing developers to focus on semantically significant differences between the outputs of the old and new compilers. 
11:15
PPDP: Contributed Talks #2
[Chair:
Philippa Gardner • Location:
HZ 10 (third floor, Hörsaalzentrum)]
11:15
Nondeterministic Manifest Contracts
Yuki Nishida and Atsushi Igarashi We study a manifest contract systema typed calculus of higherorder contracts where contracts are tightly integrated into a refinement type systemfor 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. 11:45
An Internalist Approach to CorrectbyConstruction 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 correctbyconstruction 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 assemblylike low level code and separately proving its correctness. 
11:15
PPDP: Contributed Talks #2
[Chair:
Philippa Gardner • Location:
HZ 10 (third floor, Hörsaalzentrum)]
11:15
Nondeterministic Manifest Contracts
Yuki Nishida and Atsushi Igarashi We study a manifest contract systema typed calculus of higherorder contracts where contracts are tightly integrated into a refinement type systemfor 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. 11:45
An Internalist Approach to CorrectbyConstruction 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 correctbyconstruction 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 assemblylike low level code and separately proving its correctness. 
12:15
Lunch Break
[Location:
Mensa Casino]

12:15
Lunch Break
[Location:
Mensa Casino]

14:00
PPDP: Invited Talk
[Chair:
Peter Thiemann • Location:
HZ 10 (third floor, Hörsaalzentrum)]
Calculating Distributions (Invited Talk)
ChungChieh Shan 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. 
14:00
PPDP: Invited Talk
[Chair:
Peter Thiemann • Location:
HZ 10 (third floor, Hörsaalzentrum)]
Calculating Distributions (Invited Talk)
ChungChieh Shan 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. 
15:00
Coffee Break
[Location:
2nd floor, Hörsaalzentrum]

15:00
Coffee Break
[Location:
2nd floor, Hörsaalzentrum]

15:30
PPDP: Most Influential Paper 10year Award and Contributed Talks #3
[Chair:
Anton Setzer • Location:
HZ 10 (third floor, Hörsaalzentrum)]
15:30
Most influential paper 10year award: Programming with proofs and explicit contexts
Brigitte Pientka and Joshua Dunfield 16:00
On Intersection Types and Probabilistic Lambda Calculi
Flavien Breuvart and Ugo Dal Lago We define two intersection type systems for the pure, untyped, probabilistic lambdacalculus, 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. 16:30
Sequential and Parallel Improvements in a Concurrent Functional Programming Language
Manfred SchmidtSchauss, 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 higherorder 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. 
15:30
PPDP: Most Influential Paper 10year Award and Contributed Talks #3
[Chair:
Anton Setzer • Location:
HZ 10 (third floor, Hörsaalzentrum)]
15:30
Most influential paper 10year award: Programming with proofs and explicit contexts
Brigitte Pientka and Joshua Dunfield 16:00
On Intersection Types and Probabilistic Lambda Calculi
Flavien Breuvart and Ugo Dal Lago We define two intersection type systems for the pure, untyped, probabilistic lambdacalculus, 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. 16:30
Sequential and Parallel Improvements in a Concurrent Functional Programming Language
Manfred SchmidtSchauss, 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 higherorder 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. 
18:00
PPDP and LOPSTR Reception (Welcome Drink and Snacks)
[Location:
Cafe Sturm und Drang (ground floor, Hörsaalzentrum)]

18:00
PPDP and LOPSTR Reception (Welcome Drink and Snacks)
[Location:
Cafe Sturm und Drang (ground floor, Hörsaalzentrum)]

PPDP 

08:30
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 rooms (lecture halls HZ 10 and HZ 11) are in the third floor of the building.

08:30
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 rooms (lecture halls HZ 10 and HZ 11) are in the third floor of the building.

09:00
PPDP & LOPSTR: Joint Invited Talk
[Chair:
Peter Thiemann • Location:
HZ 10 (third floor, Hörsaalzentrum)]
Formal methods for JavaScript (Invited Talk)
Philippa Gardner We present a novel, unified approach to the development of compositional symbolic execution tools, which bridges the gap between traditional symbolic execution and compositional program reasoning based on separation logic. We apply our approach to JavaScript, providing support for full verification, wholeprogram symbolic testing, and automatic compositional testing based on biabduction. 
09:00
PPDP & LOPSTR: Joint Invited Talk
[Chair:
Peter Thiemann • Location:
HZ 10 (third floor, Hörsaalzentrum)]
Formal methods for JavaScript (Invited Talk)
Philippa Gardner We present a novel, unified approach to the development of compositional symbolic execution tools, which bridges the gap between traditional symbolic execution and compositional program reasoning based on separation logic. We apply our approach to JavaScript, providing support for full verification, wholeprogram symbolic testing, and automatic compositional testing based on biabduction. 
10:00
Coffee Break
[Location:
2nd floor, Hörsaalzentrum]

10:00
Coffee Break
[Location:
2nd floor, Hörsaalzentrum]

10:30
PPDP: Contributed Talks #4
[Chair:
Annette Bienusa • Location:
HZ 10 (third floor, Hörsaalzentrum)]
10:30
Certified Compilation of Financial Contracts
Danil Annenkov and Martin Elsman We present an extension to a certified financial contract management system that allows for templated declarative financial contracts and for integration with financial stochastic models through verified compilation into socalled payoff expressions. Such expressions readily allow for determining the value of a contract in a given evaluation context, such as contexts created for stochastic simulations. The templating mechanism is useful both at the contract specification level, for writing generic reusable contracts, and for reuse of code that, without the templating mechanism, needs to be recompiled for different evaluation contexts. We report on the effect of using the certified system in the context of a GPGPUbased Monte Carlo simulation engine for pricing various overthecounter (OTC) financial contracts. The full contractmanagement system, including the payofflanguage compilation, is verified in the Coq proof assistant and certified Haskell code is extracted from our Coq development along with Futhark code for use in a dataparallel pricing engine. 11:00
TwoPhase Dynamic Analysis of MessagePassing Go Programs based on Vector Clocks
Martin Sulzmann and Kai Stadtmüller Understanding the runtime behavior of concurrent programs is a challenging task. A popular approach is to establish a happensbefore relation via vector clocks. Thus, we can identify bugs and performance bottlenecks, for example, by checking if two conflicting events may happen concurrently. We employ a twophase method to derive vector clock information for a wide range of concurrency features that includes all of the messagepassing features in Go. The first instrumentation phase yields a runtime trace that contains all events that took place. The second trace replay phase carried out offline infers vector clock information. Trace replay operates on threadlocal traces. Thus, we can observe behavior that might result from some alternative schedule. Our approach is not tied to any specific language. We have built a prototype for the Go programming language and provide empirical evidence of the usefulness of our method. 11:30
Transformation of Combinatorial Optimization Problems Written in Extended SQL into Constraint Problems
Genki Sakanashi and Masahiko Sakai The combinatorial optimization is an important area, which gives one of the best solutions for our real problems. This paper focuses on an SQL style of declarative languages to ease descriptions of combinatorial optimization problems, and provides their solution method powered by stateoftheart CP/SMT solvers. From the semantic point of view, the search space of a combinatorial problem is given as a finite set of relations, and a solution is a relation in the set. Relations in the search space are filtered by constraints of the problem in similar to the filterfunction on lists in functional languages, and the remaining relations are solutions of the problem. According to this notion, we extended Structured Query Language (SQL) by introducing some operations on sets of relations: generating a set of relations, filtering a set of relations according to constraints, and selecting one of the optimum relations with respect to a goal function. Toward an effective implementation, a set of relations is represented as a pair of a relation containing variables with finite domains and constraints on variables. This enables to solve the target problem by CP/SMT solvers. We also give an experimental result on the graph vertex coloring problem. 
10:30
PPDP: Contributed Talks #4
[Chair:
Annette Bienusa • Location:
HZ 10 (third floor, Hörsaalzentrum)]
10:30
Certified Compilation of Financial Contracts
Danil Annenkov and Martin Elsman We present an extension to a certified financial contract management system that allows for templated declarative financial contracts and for integration with financial stochastic models through verified compilation into socalled payoff expressions. Such expressions readily allow for determining the value of a contract in a given evaluation context, such as contexts created for stochastic simulations. The templating mechanism is useful both at the contract specification level, for writing generic reusable contracts, and for reuse of code that, without the templating mechanism, needs to be recompiled for different evaluation contexts. We report on the effect of using the certified system in the context of a GPGPUbased Monte Carlo simulation engine for pricing various overthecounter (OTC) financial contracts. The full contractmanagement system, including the payofflanguage compilation, is verified in the Coq proof assistant and certified Haskell code is extracted from our Coq development along with Futhark code for use in a dataparallel pricing engine. 11:00
TwoPhase Dynamic Analysis of MessagePassing Go Programs based on Vector Clocks
Martin Sulzmann and Kai Stadtmüller Understanding the runtime behavior of concurrent programs is a challenging task. A popular approach is to establish a happensbefore relation via vector clocks. Thus, we can identify bugs and performance bottlenecks, for example, by checking if two conflicting events may happen concurrently. We employ a twophase method to derive vector clock information for a wide range of concurrency features that includes all of the messagepassing features in Go. The first instrumentation phase yields a runtime trace that contains all events that took place. The second trace replay phase carried out offline infers vector clock information. Trace replay operates on threadlocal traces. Thus, we can observe behavior that might result from some alternative schedule. Our approach is not tied to any specific language. We have built a prototype for the Go programming language and provide empirical evidence of the usefulness of our method. 11:30
Transformation of Combinatorial Optimization Problems Written in Extended SQL into Constraint Problems
Genki Sakanashi and Masahiko Sakai The combinatorial optimization is an important area, which gives one of the best solutions for our real problems. This paper focuses on an SQL style of declarative languages to ease descriptions of combinatorial optimization problems, and provides their solution method powered by stateoftheart CP/SMT solvers. From the semantic point of view, the search space of a combinatorial problem is given as a finite set of relations, and a solution is a relation in the set. Relations in the search space are filtered by constraints of the problem in similar to the filterfunction on lists in functional languages, and the remaining relations are solutions of the problem. According to this notion, we extended Structured Query Language (SQL) by introducing some operations on sets of relations: generating a set of relations, filtering a set of relations according to constraints, and selecting one of the optimum relations with respect to a goal function. Toward an effective implementation, a set of relations is represented as a pair of a relation containing variables with finite domains and constraints on variables. This enables to solve the target problem by CP/SMT solvers. We also give an experimental result on the graph vertex coloring problem. 
12:00
Lunch Break
[Location:
Mensa Casino]

12:00
Lunch Break
[Location:
Mensa Casino]

13:30
PPDP: Contributed Talks #5
[Chair:
Michael Hanus • Location:
HZ 10 (third floor, Hörsaalzentrum)]
13:30
Automatic reordering for dataflow safety of Datalog
Mistral Contrastin, Dominic Orchard and Andrew Rice Automatic Reordering for Dataflow Safety of Datalog Abstract: Clauses and subgoals in a Datalog program can be given in any order without affecting program meaning. However, practical applications of the language require the use of builtin or external predicates with particular dataflow requirements. These can be expressed as input or output modes on arguments. We describe a static analysis of moding for Datalog which can transform an illmoded program into a wellmoded program by reordering clause subgoals, satisfying dataflow requirements. We describe an incremental algorithm which efficiently finds a reordering if it exists. This frees the programmer to focus on the declarative specification of their program rather than on the implementation details of external predicates. We prove that our computed reorderings yield wellmoded programs (soundness) and that if a program can be made wellmoded, we compute a reordering to do so (completeness). 14:00
Improving Refutational Completeness of Relational Search via Divergence Test
Dmitri Rozplokhas and Dmitry Boulytchev We describe a search optimization technique for implementation of relational programming language miniKanren which makes more queries to converge. Specifically, we address the problem of conjunction noncommutativity. Our technique is based on a certain divergence criterion, which we use to trigger a dynamic reordering of conjuncts. We present a formal semantics of a miniKanrenlike language and prove that our optimization does not compromise already converging programs, thus, being a proper improvement. We also present the prototype implementation of the improved search and demonstrate its application for a number of realistic specifications. 14:30
Webbased Visualisation for Definite Clause Grammars using Prolog MetaInterpreters
Falco Nogatz, Jona Kalkus and Dietmar Seipel Definite Clause Grammars (DCGs) are a convenient way to describe lists in Prolog. They are a common mean to specify grammars for natural language processing and to parse formal languages. Despite its long history, tools dedicated to the development and debugging of DCGs are rare. In this paper, we present an interactive, webbased tool to visualise the execution of a DCG. To collect the required information from SWIProlog, we discuss several techniques, including metainterpreters, trace interceptors, and term expansions. 
13:30
PPDP: Contributed Talks #5
[Chair:
Michael Hanus • Location:
HZ 10 (third floor, Hörsaalzentrum)]
13:30
Automatic reordering for dataflow safety of Datalog
Mistral Contrastin, Dominic Orchard and Andrew Rice Automatic Reordering for Dataflow Safety of Datalog Abstract: Clauses and subgoals in a Datalog program can be given in any order without affecting program meaning. However, practical applications of the language require the use of builtin or external predicates with particular dataflow requirements. These can be expressed as input or output modes on arguments. We describe a static analysis of moding for Datalog which can transform an illmoded program into a wellmoded program by reordering clause subgoals, satisfying dataflow requirements. We describe an incremental algorithm which efficiently finds a reordering if it exists. This frees the programmer to focus on the declarative specification of their program rather than on the implementation details of external predicates. We prove that our computed reorderings yield wellmoded programs (soundness) and that if a program can be made wellmoded, we compute a reordering to do so (completeness). 14:00
Improving Refutational Completeness of Relational Search via Divergence Test
Dmitri Rozplokhas and Dmitry Boulytchev We describe a search optimization technique for implementation of relational programming language miniKanren which makes more queries to converge. Specifically, we address the problem of conjunction noncommutativity. Our technique is based on a certain divergence criterion, which we use to trigger a dynamic reordering of conjuncts. We present a formal semantics of a miniKanrenlike language and prove that our optimization does not compromise already converging programs, thus, being a proper improvement. We also present the prototype implementation of the improved search and demonstrate its application for a number of realistic specifications. 14:30
Webbased Visualisation for Definite Clause Grammars using Prolog MetaInterpreters
Falco Nogatz, Jona Kalkus and Dietmar Seipel Definite Clause Grammars (DCGs) are a convenient way to describe lists in Prolog. They are a common mean to specify grammars for natural language processing and to parse formal languages. Despite its long history, tools dedicated to the development and debugging of DCGs are rare. In this paper, we present an interactive, webbased tool to visualise the execution of a DCG. To collect the required information from SWIProlog, we discuss several techniques, including metainterpreters, trace interceptors, and term expansions. 
15:00
Break (No Coffee)
Use this break to walk from the conference location to the start of the city tour (Old Opera Frankfurt).

15:00
Break (No Coffee)
Use this break to walk from the conference location to the start of the city tour (Old Opera Frankfurt).

15:45
Social Event: Guided two hour city walk through the city centre of Frankfurt.
[Location:
The tour starts in front of the Old Opera Frankfurt]
This city walk through the old town centre (Römerberg) focuses on various aspects of Frankfurt's colourful history, including its role as electoral site of German kings and host city for the coronation ceremonies of Holy Roman emperors. Frankfurt's role as a free trade city and site of Germany's first national assembly, held right here at St Paul's Church in 1848, is also highlighted. The tour covers an abundance of significant events within the smallest of geographical areas. 
15:45
Social Event: Guided two hour city walk through the city centre of Frankfurt.
[Location:
The tour starts in front of the Old Opera Frankfurt]
This city walk through the old town centre (Römerberg) focuses on various aspects of Frankfurt's colourful history, including its role as electoral site of German kings and host city for the coronation ceremonies of Holy Roman emperors. Frankfurt's role as a free trade city and site of Germany's first national assembly, held right here at St Paul's Church in 1848, is also highlighted. The tour covers an abundance of significant events within the smallest of geographical areas. 
18:30
Conference Dinner
[Location:
Vinum Frankfurt]

18:30
Conference Dinner
[Location:
Vinum Frankfurt]

PPDP 

08:30
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 rooms (lecture halls HZ 10 and HZ 11) are in the third floor of the building. 
08:30
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 rooms (lecture halls HZ 10 and HZ 11) are in the third floor of the building. 
09:00
PPDP & LOPSTR: Joint Invited Talk
[Chair:
Peter Stuckey • Location:
HZ 10 (third floor, Hörsaalzentrum)]
Constrained Horn Clauses for Verification (Invited Talk)
Jorge Navas Developing scalable software verification tools is a very difficult task. First, due to the undecidability of the verification problem, these tools, must be highly tuned and engineered to provide reasonable efficiency and precision tradeoffs. Second, different programming languages come with very diverse assortments of syntactic and semantic features. Third, the diverse encoding of the verification problem makes the integration with other powerful solvers and verifiers difficult. This talk presents SeaHorn — an open source automated Constrained Horn clausebased reasoning framework. SeaHorn combines advanced automated solving techniques based on Satisfiability Modulo Theory (SMT) and Abstract Interpretation. SeaHorn is built on top of LLVM using its frontend(s) to deal with the idiosyncrasies of the syntax and it highly benefits from LLVM optimizations to reduce the verification effort. SeaHorn uses Constrained Horn clauses (CHC) which are a uniform way to formally represent a broad variety of transition systems while allowing many encoding styles of verification conditions. Moreover, the recent popularity of CHC as an intermediate language for verification engines makes it possible to interface SeaHorn with a variety of new and emerging tools. All of these features make SeaHorn a versatile and highly customizable tool which allows researchers to easily build or experiment with new verification techniques. 
09:00
PPDP & LOPSTR: Joint Invited Talk
[Chair:
Peter Stuckey • Location:
HZ 10 (third floor, Hörsaalzentrum)]
Constrained Horn Clauses for Verification (Invited Talk)
Jorge Navas Developing scalable software verification tools is a very difficult task. First, due to the undecidability of the verification problem, these tools, must be highly tuned and engineered to provide reasonable efficiency and precision tradeoffs. Second, different programming languages come with very diverse assortments of syntactic and semantic features. Third, the diverse encoding of the verification problem makes the integration with other powerful solvers and verifiers difficult. This talk presents SeaHorn — an open source automated Constrained Horn clausebased reasoning framework. SeaHorn combines advanced automated solving techniques based on Satisfiability Modulo Theory (SMT) and Abstract Interpretation. SeaHorn is built on top of LLVM using its frontend(s) to deal with the idiosyncrasies of the syntax and it highly benefits from LLVM optimizations to reduce the verification effort. SeaHorn uses Constrained Horn clauses (CHC) which are a uniform way to formally represent a broad variety of transition systems while allowing many encoding styles of verification conditions. Moreover, the recent popularity of CHC as an intermediate language for verification engines makes it possible to interface SeaHorn with a variety of new and emerging tools. All of these features make SeaHorn a versatile and highly customizable tool which allows researchers to easily build or experiment with new verification techniques. 
10:00
Coffee Break
[Location:
2nd floor, Hörsaalzentrum]

10:00
Coffee Break
[Location:
2nd floor, Hörsaalzentrum]

10:30
PPDP: Contributed Talks #6
[Chair:
Alberto Pardo • Location:
HZ 10 (third floor, Hörsaalzentrum)]
10:30
Declarative GUIs: Simple, Consistent, and Verified
Stephan Adelsberger, Anton Setzer and Eric Walkingshaw Graphical user interfaces (GUIs) are ubiquitous in realworld software and a notorious source of bugs that are difficult to catch through software testing. Model checking has been used to prove the absence of certain kinds of bugs, but model checking works on an abstract model of the GUI application, which might be inconsistent with its implementation. We present a library for developing directly verified, statedependent GUI applications in the dependently typed programming language Agda. In the library, the type of a GUI's controller depends on a specification of the GUI itself, statically enforcing consistency between them. Arbitrary properties can be defined and proved in terms of user interactions and state transitions. Our library connects to a custombuilt Haskell backend for declarative vectorbased GUI elements. Compared to an earlier version of our library built on an existing imperative GUI framework, the more declarative backend supports simpler definitions and proofs. As a practical application of our library to a safetycritical domain, we present a case study developed in cooperation with the Medical University of Vienna. The case study implements a healthcare process for prescribing anticoagulants, which is highly errorprone when followed manually. Our implementation generates GUIs from an abstract description of a dataaware business process, making our approach easy to reuse and adapt to other safetycritical processes. We prove medically relevant safety properties about the executable GUI application, such as that given certain inputs, certain states must or must not be reached. 11:00
Combinatorics of Explicit Substitutions
Maciej Bendkowski and Pierre Lescanne lambdaupsilon is an extension of the lambdacalculus which internalises the calculus of substitutions. In the current paper, we investigate the combinatorial properties of lambdaupsilon focusing on the quantitative aspects of substitution resolution. We exhibit an unexpected correspondence between the counting sequence for lambdaupsilon terms and famous Catalan numbers. As a byproduct, we establish effective sampling schemes for random lambdaupsilon terms. We show that typical lambdaupsilon terms represent, in a strong sense, nonstrict computations in the classic lambdacalculus. Moreover, typically almost all substitutions are in fact suspended, i.e., unevaluated, under closures. Consequently, we argue that lambdaupsilon is an intrinsically nonstrict calculus of explicit substitutions. Finally, we investigate the distribution of various redexes governing the substitution resolution in lambdaupsilon and investigate the quantitative contribution of various substitution primitives. 11:30
Schematic Polymorphism in the Abella Proof Assistant
Gopalan Nadathur and Yuting Wang The Abella interactive theorem prover has proven to be an effective vehicle for reasoning about relational specifications. However, the system has a limitation that arises from the fact that it is based on a simply typed logic: formalizations that are identical except in the respect that they apply to different types have to be repeated at each type. We develop an approach that overcomes this limitation while preserving the logical underpinnings of the system. In this approach object constructors, formulas and other relevant logical notions are allowed to be parameterized by types, with the interpretation that they stand for the (infinite) collection of corresponding constructs that are obtained by instantiating the type parameters. The proof structures that we consider for formulas that are schematized in this fashion are limited to ones whose type instances are valid proofs in the simply typed logic. We develop schematic proof rules that ensure this property, a task that is complicated by the fact that type information influences the notion of unification that plays a key role in the logic. Our ideas, which have been implemented in an updated version of the system, accommodate schematic polymorphism both in the core logic of Abella and in the executable specification logic that it embeds. Authors: 
10:30
PPDP: Contributed Talks #6
[Chair:
Alberto Pardo • Location:
HZ 10 (third floor, Hörsaalzentrum)]
10:30
Declarative GUIs: Simple, Consistent, and Verified
Stephan Adelsberger, Anton Setzer and Eric Walkingshaw Graphical user interfaces (GUIs) are ubiquitous in realworld software and a notorious source of bugs that are difficult to catch through software testing. Model checking has been used to prove the absence of certain kinds of bugs, but model checking works on an abstract model of the GUI application, which might be inconsistent with its implementation. We present a library for developing directly verified, statedependent GUI applications in the dependently typed programming language Agda. In the library, the type of a GUI's controller depends on a specification of the GUI itself, statically enforcing consistency between them. Arbitrary properties can be defined and proved in terms of user interactions and state transitions. Our library connects to a custombuilt Haskell backend for declarative vectorbased GUI elements. Compared to an earlier version of our library built on an existing imperative GUI framework, the more declarative backend supports simpler definitions and proofs. As a practical application of our library to a safetycritical domain, we present a case study developed in cooperation with the Medical University of Vienna. The case study implements a healthcare process for prescribing anticoagulants, which is highly errorprone when followed manually. Our implementation generates GUIs from an abstract description of a dataaware business process, making our approach easy to reuse and adapt to other safetycritical processes. We prove medically relevant safety properties about the executable GUI application, such as that given certain inputs, certain states must or must not be reached. 11:00
Combinatorics of Explicit Substitutions
Maciej Bendkowski and Pierre Lescanne lambdaupsilon is an extension of the lambdacalculus which internalises the calculus of substitutions. In the current paper, we investigate the combinatorial properties of lambdaupsilon focusing on the quantitative aspects of substitution resolution. We exhibit an unexpected correspondence between the counting sequence for lambdaupsilon terms and famous Catalan numbers. As a byproduct, we establish effective sampling schemes for random lambdaupsilon terms. We show that typical lambdaupsilon terms represent, in a strong sense, nonstrict computations in the classic lambdacalculus. Moreover, typically almost all substitutions are in fact suspended, i.e., unevaluated, under closures. Consequently, we argue that lambdaupsilon is an intrinsically nonstrict calculus of explicit substitutions. Finally, we investigate the distribution of various redexes governing the substitution resolution in lambdaupsilon and investigate the quantitative contribution of various substitution primitives. 11:30
Schematic Polymorphism in the Abella Proof Assistant
Gopalan Nadathur and Yuting Wang The Abella interactive theorem prover has proven to be an effective vehicle for reasoning about relational specifications. However, the system has a limitation that arises from the fact that it is based on a simply typed logic: formalizations that are identical except in the respect that they apply to different types have to be repeated at each type. We develop an approach that overcomes this limitation while preserving the logical underpinnings of the system. In this approach object constructors, formulas and other relevant logical notions are allowed to be parameterized by types, with the interpretation that they stand for the (infinite) collection of corresponding constructs that are obtained by instantiating the type parameters. The proof structures that we consider for formulas that are schematized in this fashion are limited to ones whose type instances are valid proofs in the simply typed logic. We develop schematic proof rules that ensure this property, a task that is complicated by the fact that type information influences the notion of unification that plays a key role in the logic. Our ideas, which have been implemented in an updated version of the system, accommodate schematic polymorphism both in the core logic of Abella and in the executable specification logic that it embeds. Authors: 
12:00
Lunch Break
[Location:
Mensa Casino]

12:00
Lunch Break
[Location:
Mensa Casino]

13:30
PPDP: Contributed Talks #7
[Chair:
Dietmar Seipel • Location:
HZ 10 (third floor, Hörsaalzentrum)]
13:30
Implicit Parameters for Logic Programming
Magnus Madsen and Ondřej Lhoták Implicit parameters allow programmers to omit certain arguments from function calls and have them automatically inferred by the compiler based on their types. At every call site, the compiler determines the values of the implicit parameters based on their declared types and the bindings currently in implicit scope. The programmer controls this mechanism in two ways: by adding bindings to the implicit scope, or by explicitly providing the implicit parameters for the function call. Implicit parameters are known from functional and objectoriented languages such as Haskell and Scala. In recent years, more languages have added support for implicit parameters, including Agda, Coq, and Idris. Implicit parameters have played an impressive role as the foundation for a broad range of language features such as type classes, capability and effect systems, software transactional memory, macros, and more. In this paper, we propose a design of implicit parameters for typed Horn clause based logic programming languages, such as Datalog and Prolog. We illustrate the usefulness of implicit parameters and show how they support logic programming in the large. We explore some of the differences that arise between implicit parameters in functional languages and in logic languages. 14:00
Verifying FailFree Declarative Programs
Michael Hanus Failed computations are a frequent problem in software system development. Some failures have external reasons (e.g., missing files) that can be caught by exception handlers. Many other failures have internal reasons, such as calling a partially defined operation with unintended arguments. In order to avoid the latter kind of failures, one can try to analyze the program at compile time for potential occurrences of these failures at run time. In this paper we present an approach to verify the absence of such failures in functional logic programs. Since programming with failures is a typical technique in logic programming, we are not interested to abandon partially defined operations at all. Instead, we want to verify conditions which ensure that operations can be executed without running into a failure. For this purpose, we propose to annotate operations with nonfail conditions that are verified at compile time with an SMT solver. For successfully verified programs, it is ensured that computations never fail provided that the nonfail condition of the main operation is satisfied. 14:30
Static Performance Guarantees for Programs with Runtime Checks
Maximiliano Klemen, Nataliia Stulova, Pedro LopezGarcia, Jose F. Morales and Manuel V. Hermenegildo Instrumenting programs for performing runtime checking of properties, such as regular shapes, is a common and useful technique that helps programmers detect incorrect program behaviors. This is specially true in dynamic languages such as Prolog. However, such runtime checks inevitably introduce runtime overhead (in execution time, memory, energy, etc.). Several approaches have been proposed for reducing this overhead, such as eliminating the checks that can statically be proved to always succeed, and/or optimizing the way in which the (remaining) checks are performed. However, there are cases in which it is not possible to remove all checks statically (e.g., open libraries which must check their interfaces, complex properties, unknown code, etc.) and in which, even after optimizations, these remaining checks may still introduce an unacceptable level of overhead. It is thus important for programmers to be able to determine the additional cost due to the runtime checks and compare it to some notion of admissible cost. The common practice used for estimating runtime checking overhead is profiling, which is not exhaustive by nature. Instead, we propose a method that uses static analysis to estimate such overhead, with the advantage that the estimations are functions parameterized by input data sizes. Unlike profiling, this approach can provide guarantees for all possible execution traces, and allows assessing how the overhead grows as the size of the input grows. Our method also extends an existing assertion verification framework to express “admissible” overheads, and statically and automatically checks whether the instru mented program conforms with such specifications. Finally, we present an experimental evaluation of our approach that suggests that our method is feasible and promising. 
13:30
PPDP: Contributed Talks #7
[Chair:
Dietmar Seipel • Location:
HZ 10 (third floor, Hörsaalzentrum)]
13:30
Implicit Parameters for Logic Programming
Magnus Madsen and Ondřej Lhoták Implicit parameters allow programmers to omit certain arguments from function calls and have them automatically inferred by the compiler based on their types. At every call site, the compiler determines the values of the implicit parameters based on their declared types and the bindings currently in implicit scope. The programmer controls this mechanism in two ways: by adding bindings to the implicit scope, or by explicitly providing the implicit parameters for the function call. Implicit parameters are known from functional and objectoriented languages such as Haskell and Scala. In recent years, more languages have added support for implicit parameters, including Agda, Coq, and Idris. Implicit parameters have played an impressive role as the foundation for a broad range of language features such as type classes, capability and effect systems, software transactional memory, macros, and more. In this paper, we propose a design of implicit parameters for typed Horn clause based logic programming languages, such as Datalog and Prolog. We illustrate the usefulness of implicit parameters and show how they support logic programming in the large. We explore some of the differences that arise between implicit parameters in functional languages and in logic languages. 14:00
Verifying FailFree Declarative Programs
Michael Hanus Failed computations are a frequent problem in software system development. Some failures have external reasons (e.g., missing files) that can be caught by exception handlers. Many other failures have internal reasons, such as calling a partially defined operation with unintended arguments. In order to avoid the latter kind of failures, one can try to analyze the program at compile time for potential occurrences of these failures at run time. In this paper we present an approach to verify the absence of such failures in functional logic programs. Since programming with failures is a typical technique in logic programming, we are not interested to abandon partially defined operations at all. Instead, we want to verify conditions which ensure that operations can be executed without running into a failure. For this purpose, we propose to annotate operations with nonfail conditions that are verified at compile time with an SMT solver. For successfully verified programs, it is ensured that computations never fail provided that the nonfail condition of the main operation is satisfied. 14:30
Static Performance Guarantees for Programs with Runtime Checks
Maximiliano Klemen, Nataliia Stulova, Pedro LopezGarcia, Jose F. Morales and Manuel V. Hermenegildo Instrumenting programs for performing runtime checking of properties, such as regular shapes, is a common and useful technique that helps programmers detect incorrect program behaviors. This is specially true in dynamic languages such as Prolog. However, such runtime checks inevitably introduce runtime overhead (in execution time, memory, energy, etc.). Several approaches have been proposed for reducing this overhead, such as eliminating the checks that can statically be proved to always succeed, and/or optimizing the way in which the (remaining) checks are performed. However, there are cases in which it is not possible to remove all checks statically (e.g., open libraries which must check their interfaces, complex properties, unknown code, etc.) and in which, even after optimizations, these remaining checks may still introduce an unacceptable level of overhead. It is thus important for programmers to be able to determine the additional cost due to the runtime checks and compare it to some notion of admissible cost. The common practice used for estimating runtime checking overhead is profiling, which is not exhaustive by nature. Instead, we propose a method that uses static analysis to estimate such overhead, with the advantage that the estimations are functions parameterized by input data sizes. Unlike profiling, this approach can provide guarantees for all possible execution traces, and allows assessing how the overhead grows as the size of the input grows. Our method also extends an existing assertion verification framework to express “admissible” overheads, and statically and automatically checks whether the instru mented program conforms with such specifications. Finally, we present an experimental evaluation of our approach that suggests that our method is feasible and promising. 
15:00
Coffee Break
[Location:
2nd floor, Hörsaalzentrum]

15:00
Coffee Break
[Location:
2nd floor, Hörsaalzentrum]

15:30
PPDP: Contributed Talks #8
[Chair:
David Sabel • Location:
HZ 10 (third floor, Hörsaalzentrum)]
15:30
Three Improvements to the TopDown Solver
Helmut Seidl and Ralf Vogler The local solver TD is a generic fixpoint engine which explores a given system of equations on demand. It has been successfully applied to the interprocedural analysis of procedural languages. The solver TD gains efficiency by detecting variable dependencies on the fly. This algorithm has been recently extended to deal with widening and narrowing as well. In particular, it has been equipped with an automatic detection of widening and narrowing points. That version, however, is only guaranteed to terminate under two conditions: only finitely many variables are encountered, and all righthand sides are monotonic. While the first condition is unavoidable, the second limits the applicability of the solver. Another limitation is that the solver maintains the current abstract values of all encountered variables in one datastructure  thus prohibiting interprocedural analyses to scale to larger programs. In the present paper, we therefore extend the topdown solver TD in three ways. First, we indicate how the restriction to monotonic righthand sides can be lifted. Then we show how the solver can be tuned to store abstract values only when it turns out to be inevitable. Finally, we also show how the solver can be extended to sideeffecting equation systems, which have successfully been applied to a seamless combination of contextsensitive with flowinsensitive analyses. 16:00
Lazy Abstraction for HigherOrder Program Verification
Taku Terao This paper proposes a lazy abstraction algorithm for verification of functional programs. The feature of lazy abstraction method is that the predicate abstraction and the model checking are fused, and that abstractions for unreachable configurations are pruned. We define an abstract semantics that characterizes the precision of the lazy abstraction algorithm, and prove the soundness of our verification method and the progress property of our abstraction refinement algorithm. We have implemented a prototype of our method, and confirmed through experiments that total efficiency of verification is improved, compared with previous eager abstraction methods. 16:30
An Infrastructure for Combining Domain Knowledge with Automated Theorem Provers
Sylvia Grewe, Sebastian Erdweg, André Pacak and Mira Mezini Computer science has seen much progress in the area of automated verification in the last decades. Yet, there are many domains where abstract strategies for verifying standard properties are wellunderstood by domain experts, but still not automated to a satisfactory degree. One example for such a domain are type soundness proofs. Being able to express domainspecific verification strategies using domainspecific terminology and concepts can help to narrow down this gap toward more automated verification. We present the requirements, design, and implementation of a configurable verification infrastructure that allows for expressing domain knowledge about proofs and for interfacing with existing automated theorem provers and solvers to verify individual proof steps. As an application scenario for our infrastructure, we present the development of a standard type soundness proof for a typed subset of SQL. 17:00
Pattern Matching and Fixed Points: Resources Types and Strong CallByNeed
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 nonidempotent intersection types. We use them to characterize weak normalisation for a typeerased 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 fixedpoint operator. The characterization is then used to prove the completeness of a strong callbyneed strategy for λe. This strategy operates on open terms: rather than having evaluation stop when it reaches an abstraction, as in weak callbyneed, it computes strong normal forms by admitting reduction inside the body of abstractions and substitutions. Moreover, argument evaluation is byneed: arguments are evaluated when needed and at most once. Such a notion of reduction is of interest in areas such as partial evaluation and proofcheckers such as Coq. 
15:30
PPDP: Contributed Talks #8
[Chair:
David Sabel • Location:
HZ 10 (third floor, Hörsaalzentrum)]
15:30
Three Improvements to the TopDown Solver
Helmut Seidl and Ralf Vogler The local solver TD is a generic fixpoint engine which explores a given system of equations on demand. It has been successfully applied to the interprocedural analysis of procedural languages. The solver TD gains efficiency by detecting variable dependencies on the fly. This algorithm has been recently extended to deal with widening and narrowing as well. In particular, it has been equipped with an automatic detection of widening and narrowing points. That version, however, is only guaranteed to terminate under two conditions: only finitely many variables are encountered, and all righthand sides are monotonic. While the first condition is unavoidable, the second limits the applicability of the solver. Another limitation is that the solver maintains the current abstract values of all encountered variables in one datastructure  thus prohibiting interprocedural analyses to scale to larger programs. In the present paper, we therefore extend the topdown solver TD in three ways. First, we indicate how the restriction to monotonic righthand sides can be lifted. Then we show how the solver can be tuned to store abstract values only when it turns out to be inevitable. Finally, we also show how the solver can be extended to sideeffecting equation systems, which have successfully been applied to a seamless combination of contextsensitive with flowinsensitive analyses. 16:00
Lazy Abstraction for HigherOrder Program Verification
Taku Terao This paper proposes a lazy abstraction algorithm for verification of functional programs. The feature of lazy abstraction method is that the predicate abstraction and the model checking are fused, and that abstractions for unreachable configurations are pruned. We define an abstract semantics that characterizes the precision of the lazy abstraction algorithm, and prove the soundness of our verification method and the progress property of our abstraction refinement algorithm. We have implemented a prototype of our method, and confirmed through experiments that total efficiency of verification is improved, compared with previous eager abstraction methods. 16:30
An Infrastructure for Combining Domain Knowledge with Automated Theorem Provers
Sylvia Grewe, Sebastian Erdweg, André Pacak and Mira Mezini Computer science has seen much progress in the area of automated verification in the last decades. Yet, there are many domains where abstract strategies for verifying standard properties are wellunderstood by domain experts, but still not automated to a satisfactory degree. One example for such a domain are type soundness proofs. Being able to express domainspecific verification strategies using domainspecific terminology and concepts can help to narrow down this gap toward more automated verification. We present the requirements, design, and implementation of a configurable verification infrastructure that allows for expressing domain knowledge about proofs and for interfacing with existing automated theorem provers and solvers to verify individual proof steps. As an application scenario for our infrastructure, we present the development of a standard type soundness proof for a typed subset of SQL. 17:00
Pattern Matching and Fixed Points: Resources Types and Strong CallByNeed
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 nonidempotent intersection types. We use them to characterize weak normalisation for a typeerased 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 fixedpoint operator. The characterization is then used to prove the completeness of a strong callbyneed strategy for λe. This strategy operates on open terms: rather than having evaluation stop when it reaches an abstraction, as in weak callbyneed, it computes strong normal forms by admitting reduction inside the body of abstractions and substitutions. Moreover, argument evaluation is byneed: arguments are evaluated when needed and at most once. Such a notion of reduction is of interest in areas such as partial evaluation and proofcheckers such as Coq. 