Abstract: When type systems detect legitimate program errors, they help to reduce the time spent debugging. Type systems catch errors in code that is not executed by the programmer. Proof generation capabilities of proof construction systems are based on type theor

Key words: Type system, Program verification, λ-calculus, Proof theory