Theorem proving for untyped constructive -calculus: implementation and application

DOI10.1093/JIGPAL/9.1.83zbMath0970.68160OpenAlexW2026352253MaRDI QIDQ2708310

Allan Ramsay

Publication date: 24 October 2001

Published in: Logic Journal of IGPL (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/jigpal/9.1.83

zbMATH Keywords

\(\lambda\)-calculustheorem proverhighly intensional logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

This page was built for publication: Theorem proving for untyped constructive  -calculus: implementation and application