Sequent combinators: a Hilbert system for the lambda calculus

This paper introduces a Hilbert system for lambda calculus called sequent combinators. Sequent combinators address many of the problems of Hilbert systems, which have led to the more widespread adoption of natural deduction systems in computer science. This suggests that Hilbert systems, with their more uniform approach to meta-variables and substitution, may be a more suitable framework than lambda calculus for type theories and programming languages.

• Type: Journal
• Year: 2000
• Where: MSCS
• Authors: Healfdene Goguen, Jean Goubault-Larrecq
• Keywords: Hilbert Systems, Lambda Calculus, MSCS 2000, Sequent Combinators