λProlog, un lenguaje de programación lógico desarrollado a finales de la década de 1980, está experimentando un inesperado resurgimiento en la comunidad tecnológica. Basado en la lógica intuicionista de orden superior, λProlog se destaca por su sólida base lógica, que permite características avanzadas como programación modular, tipos de datos abstractos y programación de orden superior. Originalmente implementado en Prolog en 1988, el lenguaje fue pionero en el soporte de sintaxis abstracta de orden superior (HOAS).
Este resurgimiento se debe, en parte, a su utilidad en meta-programación y a la aparición de nuevas implementaciones y aplicaciones. El interés se ve impulsado por herramientas como Abella, un teorema probador interactivo, y su capacidad para ejecutarse en navegadores web gracias a su implementación en OCaml. El libro “Proof Theory and Logic Programming” de Dale Miller, investigador en Lix (Polytechnique), proporciona una descripción detallada de la teoría de la prueba detrás de λProlog. Aunque relativamente desconocido, el lenguaje está encontrando nuevos adeptos y aplicaciones en diversos campos.