Speaker: Michael Arntzenius (Birmingham) Title: Type inference for monotonicity Abstract: A function is monotone if increasing its input can't decrease its output. It can be useful to guarantee certain functions in a program are monotone. For example, iterating a monotone map on a semilattice satisfying the ascending chain condition will find its least fixed point; many algorithms are concisely expressed this way, including shortest paths, NFA equivalence, many static analyses, and CYK parsing. As another example, recent work in distributed programming (eg. "Consistency as Logical Monotonicity") has connected monotonicity with eventual consistency. I present a work-in-progress bidirectional type inference algorithm for a simply-typed lambda calculus where types denote preorders and all functions are monotone. Non-monotonicity is handled with modal types, but surprisingly, these types need no explicit constructors or destructors; they can be entirely inferred -- I hope. The crucial techniques are: 1. annotating variables with their modalities, which form a semiring; 2. taking advantage of adjunctions in the underlying semantics; 3. being very careful about subtyping.