POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States
Mon 20 Jan 2025 17:10 - 17:20 at Duck, Duck Goose - Session 4 Chair(s): Vitor Santos Costa

Logic programming allows structuring code in terms of predicates or relations, rather than functions. Although logic programming languages present advantages in terms of declarativeness and conciseness, the introduction of static types has not become part of most popular logic programming languages, increasing the difficulty of testing and debugging of logic programming code. This paper demonstrates how to implement logic programming in Haskell, thus empowering logic programs with types, and functional programs with relations or predicates. We do so by combining three ideas. First, we use extensible types to generalize a type by a parameter type function. Second, we use a sum type as an argument to introduce optional variables in extensible types. Third, we implement a unification algorithm capable of working with any data structure, provided that certain operations are implemented for the given type. We demonstrate our proposal via a series of increasingly complex examples inspired by educational texts in logic programming, and leverage the host language’s features to make new notation convenient for users, showing that the proposed approach is not just technically possible but also practical.

Mon 20 Jan

Displayed time zone: Mountain Time (US & Canada) change

16:00 - 17:30
Session 4PADL at Duck, Duck Goose
Chair(s): Vitor Santos Costa University of Porto, Portugal
16:00
30m
Talk
MOLA: A Runtime Verification Engine Factory by (Meta-)interpreting Embedded DSLs
PADL
Felipe Gorostiaga IMDEA Software Institute, Martin Ceresa IMDEA Software Institute, César Sánchez IMDEA Software Institute
16:30
30m
Talk
Checking Concurrency Coding Rules
PADL
Lars-Åke Fredlund Universidad Politécnica de Madrid, Ángel Herranz Universidad Politécnica de Madrid, Julio Mariño Universidad Politécnica de Madrid
17:00
10m
Talk
Can Logic Programming Be Liberated from Predicates and Backtracking? (Lightning talk)
PADL
Michael Hanus Kiel University
17:10
10m
Talk
Logic Programming with Extensible Types (Lightning talk)
PADL
Ivan Perez NASA Ames Research Center, Ángel Herranz Universidad Politécnica de Madrid, P: Julio Mariño Universidad Politécnica de Madrid