"Nested proof search as reduction in the Lambda-calculus."

Nicolas Guenot (2011)
a service of  Schloss Dagstuhl - Leibniz Center for Informatics