References. The Formulae-as-Types Notion of Construction (Howard, 1980) Tags: Type theory, logic, propositional logic.
