IMO Paul Tarau has some good stuff in this area, e.g.: "On a uniform representation of combinators, arithmetic, lambda terms and types", Paul Tarau https://dl.a

IMO Paul Tarau has some good stuff in this area, e.g.: "On a uniform representation of combinators, arithmetic, lambda terms and types", Paul Tarau https://dl.acm.org/doi/10.1145/2790449.2790526 https://dl.acm.org/doi/10.1145/2790449.2790526 Abstract: > A uniform representation, as binary trees with empty leaves, is given to expressions built with Rosser's X-combinator, natural numbers, lambda terms and simple types. Type inference, normalization of combinator expressions and lambda terms in de Bruijn notation, ranking/unranking algorithms and tree-based natural numbers are described as a literate Prolog program. > With sound unification and compact expression of combinatorial generation algorithms, logic programming is shown to conveniently host a declarative playground where interesting properties and behaviors emerge from the interaction of heterogenous but deeply connected computational objects.