MaudeTypedLog: A Typed Interpreter for Prolog in Maude

Abstract

Prolog is traditionally thought of as an untyped logic programming language, although there are queries that result in a type error. Several attempts of statically introducing a type discipline in Prolog have been made but they have not been widely adopted. We use Maude to implement a typed unification algorithm and use it as the basis for an interpreter for Prolog called MaudeTypedLog. This interpreter follows the Typed SLD-resolution operational semantics for logic programming, that makes it possible to detect type errors in both programs and queries dynamically.

In Proceedings LSFA 2026, arXiv:2607.15904