From Datalog to Flix: A Declarative Language for Fixed Points on Lattices
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 meaning of Flix programs without imposing any specific evaluation strategy, allowing for different Flix solvers. We have implemented a prototype compiler frontend 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 strong connections between these two algorithms.
Wed 15 JunDisplayed time zone: Tijuana, Baja California change
15:30 - 17:00 | |||
15:30 30mTalk | Configuration Synthesis for Programmable Analog Devices with Arco Research Papers Sara Achour Massachusetts Institute of Technology, USA, Rahul Sarpeshkar MIT, Martin C. Rinard Massachusetts Institute of Technology, USA Media Attached | ||
16:00 30mTalk | From Datalog to Flix: A Declarative Language for Fixed Points on Lattices Research Papers Magnus Madsen University of Waterloo, Ming-Ho Yee University of Waterloo, Ondřej Lhoták University of Waterloo DOI Media Attached | ||
16:30 30mTalk | Latte: A Language, Compiler, and Runtime for Elegant and Efficient Deep Neural Networks Research Papers Leonard Truong UC Berkeley / Intel Labs, Raj Barik Intel Labs, Ehsan Totoni Intel Labs, Hai Liu Intel Labs, Chick Markley UC Berkeley, Armando Fox UC Berkeley, Tatiana Shpeisman Intel Labs Media Attached |