[Pl-seminar] 4/14 Seminar: Magnus Madsen, From Datalog to Flix: A Declarative Language for Fixed Points on Lattices

[Daniel Patterson]

NOTE: Due to a scheduling issue, this seminar will be held starting at
*1:30pm*, rather than our normal time.

NUPRL Seminar presents

Magnus Madsen
University of Waterloo
Host: Frank Tip

1:30-3:00PM
Friday, April 14th 2017
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)


>From Datalog to Flix: A Declarative Language for Fixed Points on Lattices

Abstract:
We present FLIX, a declarative programming language for
specifying and solving least fixed point problems, particularly
static program analyses. FLIX is inspired by Datalog and
extends it with lattices and monotone functions. Using FLIX,
implementors of static analyses can express a broader range
of analyses than is currently possible in pure Datalog, while
retaining its familiar rule-based syntax.
We define a model-theoretic semantics of FLIX as a natural
extension of the Datalog semantics. This semantics captures
the declarative meaning of FLIX programs without imposing
any specific evaluation strategy. An efficient strategy is
semi-naïve evaluation which we adapt for FLIX. We have
implemented a compiler and runtime for FLIX, and used it
to express several well-known static analyses, including the
IFDS and IDE algorithms. The declarative nature of FLIX
clearly exposes the similarity between these two algorithms.

This work has previously been presented at PLDI 2016.
The talk will cover some of that material as well as recent developments.


Bio:
The speaker is a post doctoral fellow at the University of Waterloo.
-------------- next part --------------
HTML attachment scrubbed and removed