Fixpoints for the masses: programming with first-class Datalog constraints

Magnus Madsen, Ondrej Lhoták

Publikation: Bidrag til bog/antologi/rapport/proceedingKonferencebidrag i proceedingsForskningpeer review

Abstract

Datalog is a declarative logic programming language that has been used in a variety of applications, including big-data analytics, language processing, networking and distributed systems, and program analysis. In this paper, we propose first-class Datalog constraints as a mechanism to construct, compose, and solve Datalog programs at run time. The benefits are twofold: We gain the full power of a functional programming language to operate on Datalog constraints-as-values, while simultaneously we can use Datalog where it really shines: to declaratively express and solve fixpoint problems. We present an extension of the lambda calculus with first-class Datalog constraints, including its semantics and a type system with row polymorphism based on Hindley-Milner. We prove soundness of the type system and implement it as an extension of the Flix programming language.

OriginalsprogEngelsk
TitelProceedings of the ACM on Programming Languages
Antal sider28
Vol/bind4
ForlagAssociation for Computing Machinery
Publikationsdato13 nov. 2020
UdgaveOOPSLA
DOI
StatusUdgivet - 13 nov. 2020
NavnACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages and Applications

Fingeraftryk

Dyk ned i forskningsemnerne om 'Fixpoints for the masses: programming with first-class Datalog constraints'. Sammen danner de et unikt fingeraftryk.

Citationsformater