Theorem proving for untyped constructive \(\lambda\)-calculus: Implementation and application
scientific article