ΛProlog: Logic programming in higher-order logic
Summary
ΛProlog is a logic programming language built on higher-order intuitionistic logic, enabling higher-order abstract syntax and meta-programming. The article surveys major implementations (ELPI, Teyjus, Makam), along with documentation and tooling (Abella prover) around λProlog and HOAS, with references and learning resources. It serves as a technical overview suitable for researchers and developers interested in logic programming and formal methods.