• Dana Fisman (Ben-Gurion University of the Negev)

Title: A normalized edit distance on finite and infinite words
Abstract: Robustness in formal verification refers to the question: given a system S satisfying a specification Phi, how likely is it that S will still satisfy Phi, even in the presence of errors disrupting its normal behavior. The formal definition typically assumes some error model and some distance function measuring distance between words (describing computations) and languages. To define robustness for reactive systems which are modeled by infinite words, a notion of distance between infinite words is required.

A common distance between finite words w1 and w2 is the edit (Levenstein) distance, that provides the minimal number of edit operations (substitute, delete or insert) that is required to transform w1 into w2. But how can it be enhanced to account for infinite words? Can we find a definition that is both intuitive and satisfies the requirements of a metric? Can it be computed at least for the case of ultimately periodic words? Efficiently? And what about computing the distance between languages of infinite words (say represented by Büchi automata)?

In this talk we will see that all the questions above can be answered positively. The distance function enabling this is termed ω-NED and it is a natural extension of NED, the normalized edit distance between finite words. In the quest for answering these questions we stumbled upon the fact that while it was known that NED does not satisfy the triangle inequality for arbitrary weights, the question whether it satisfies the triangle inequality when weights are uniform was open. We managed to close this gap by proving that it does, and build on this for proving the above results.

The talk is based on joint works with Joshua Grogin, Oded Margalit and Gera Weiss.

• Delia Kesner (Universite Paris Cite and Institut Universitaire de France)

Title: Embedding Quantitative Properties of Call-by-Name and Call-by-Value into Call-by-Push-Value
Abstract: This talks explores how the (untyped and typed) theories of Call-by-Name (CBN)and Call-by-Value (CBV) can be unified in a more general framework provided by Call-by-Push-Value (CBPV). Indeed, we first present an untyped CBPV-like calculus, called lambda-bang, which encodes untyped CNB and CBV, both from a static and a dynamic point of view. We then explore these encodings in a typed framework, specified by quantitative (aka non-idempotent intersection) types. Three different (quantitative) properties are discussed. The first one is related to upper bounds for reduction lengths, the second one concerns exact measures for reduction lengths and sizes of normal forms, and the last one is about the inhabitation problem. In all these cases, explained and discussed in the talk, the (quantitative) property for CBN/CBV is inherited from the corresponding one in the lambda-bang calculus.