Logic and declarative programming is often and successfully used as parts of desktop and server applications. We value the declarative techniques because it is easier to write programs that relate closely to the specification (or even write compilable specifications) and show their correctness. Declarative programming has found its place in most computer science curricula in some form (often Haskell and Prolog) as well. But especially in logic programming the applications often are theoretical or only used as part of a larger system. The parts that interact with the outside world are usually written in an imperative fashion. For embedded systems, where rule-based interaction with the outside world is often the majority of the application, declarative programming is an avenue not well explored.

Microlog is a specific dialect of Datalog closely related to the Dedalus language that includes IO operations. Our declarative language Microlog is a language that allows us to model both program state and side effects in a declarative manner. Based on Datalog, Microlog has strong foundations in relational algebra and logic. As we do not allow ad-hoc queries or a dynamic extensional database, we can split our logic program into disjoint parts; the parts that provably use finite memory over time are compiled into finite state machines while the residual program is evaluated with a naive algorithm that is optimized to use as little memory as possible. Our goal is to declaratively program microcontrollers and give static safety guarantees for data-driven interactive programs on microcontrollers

Publications and Related Work

Our Publications

Related Work

Language and Semantics

microlog is a variant of Datalog. Every predicate has an additional implicit argument that represents time.
A normal datalog rule (deductive rule) p(a1,a2,..) :- q(a1,a2,..). actually means a deduction in the current timestamp: p(T,a1,a2,..) :- q(T,a1,a2,..).
Inductive rules p(a1,a2,..)@next :- q(a1,a2,..). actually means a deduction in the next timestamp: p(S,a1,a2,..) :- q(T,a1,a2,..), successor(T,S).
In inductive rules, we addionally allow a call to an external source of computation.

Static Analysis (Memory Restriction and Safety Guarantees)

We have different approaches of giving static guarantees about microlog programs. Our current focus are safety guarantees.

Runtime and Compilation

Our current compiler is written in Haskell and translates Microlog programs to C with a runtime that executes the rules in every state. Partial programs that can be represented as finite state machines are compiled that way.

Example programs with an Arduino and Lego EV3 runtime. Some programs show specific optimizations or transformations (toy), while others show specific application. The example programs have last been compiled {{microlog.update}}.

Choose Program:
Choose Setting:
Choose Template