λProlog, Church'ün Basit Tip Teorisi (Simple Theory of Types) tarzında, yüksek mertebeden sezgisel mantığa dayalı bir mantık programlama dilidir. Bu güçlü mantıksal temel, λProlog'a modüler programlama, soyut veri tipleri, yüksek mertebeden programlama ve sözdizimindeki bağlı değişkenlerin işlenmesi için lambda-ağaç sözdizimi yaklaşımı gibi mantıksal olarak desteklenen kavramlar sunar. λProlog uygulamaları, basit tipli lambda terimlerini ve yüksek mertebeden birleştirmenin (unification) alt kümelerini destekler. Sonuç olarak, λProlog, yüksek mertebeden soyut sözdizimini (HOAS) doğrudan destekleyen dünyanın ilk programlama dili olmuştur.
λProlog, ilk olarak 1980'lerin sonlarında tasarlanmış ve uygulanmış olsa da (ilk dağıtılan sürümü 1988'de Prolog ile yazılmıştır), özellikle meta-programlama alanında yeni uygulamalar ve geliştirmelerle dile olan ilgi devam etmektedir. Dilin ve uygulamalarının belgelerine çeşitli kaynaklardan ulaşılabilir. Dale Miller, λProlog'un arkasındaki ispat teorisinin (ve onun doğrusal mantık uzantılarının) ayrıntılı olarak açıklandığı "Proof Theory and Logic Programming: Computation as Proof Search" adlı bir kitap yazmıştır.
Abella, ilişkilerle endüktif ve koendüktif akıl yürütmeyi kullanmanın yeni yollarına dayanan etkileşimli bir teorem ispatlayıcısıdır ve bağlama sahip nesneleri manipüle eden spesifikasyonlar hakkında akıl yürütmek için oldukça uygundur. λProlog kod örnekleri Teyjus dağıtımında, "Programming with Higher-Order Logic" kitabından bir alıntıda ve küçük bir koleksiyonda bulunabilir. ELPI uygulamasının OCaml ile yazılmış olması ve OCaml'in JavaScript'e derlenebilmesi sayesinde, λProlog programlarını bir web tarayıcısında çalıştırmak mümkündür; örneğin, çevrimiçi MLTS uygulamasını inceleyebilirsiniz.
λProlog, yüksek mertebeden mantık programlama yetenekleri ve özellikle yüksek mertebeden soyut sözdizimi (HOAS) desteğiyle programlama dilleri araştırmalarında önemli bir yere sahiptir.