> if we were to distill this dissertation into their key ideas, it would be these: > Model monotonicity with modal types. Datalog can be summarized as relation

> if we were to distill this dissertation into their key ideas, it would be these: > Model monotonicity with modal types. Datalog can be summarized as relational algebra plus stratified recursive queries. Modulo implementation subtleties, relational algebra embeds straightforwardly in a functional language via finite sets and set comprehensions. We have shown that stratified recursive queries also embed nicely, so long as we locate our semantics in Poset to capture compositional reasoning about monotonicity. The main difficulty is the interaction of monotone and non-monotone functions; this arises from the discreteness comonad □, and can be handled with a simple modal type system. > To find fixed points faster, incrementalize! Finding a fixed point by iteration involves repeatedly changing a function’s input to match its changing output. Doing this naïvely is asymptotically inefficient; to do it efficiently, we must efficiently propagate changes. This is not only the essence of seminaïve evaluation in Datalog, but an instance of a greater problem of automatic incremental computation. Prior work on the incremental λ-calculus shows that incremental computation can be achieved in higher-order languages; we have extended it to Datafun and shown that by modifying it to consider only increasing changes, it gives rise to seminaïve evaluation.