2026/07/18 by Enrique Gallifa-Tronch, João Barbosa, J M Barbosa +1
Computer Science · #Logic, programming, and type systems #Logic, Reasoning, and Knowledge #Formal Methods in Verification
paper · pdf · doi:10.4204/eptcs.449.7
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.