logic  programming 
aggregates 
deduction, proof, or argument  program, expression, or term 
proposition or formula  type or specification, i.e. abstraction of what the program does 
constructive proof of a formula α  program of type α 
constructs 
proof (with a parcel of hypotheses)  functional term 
premise or hypothesis  free name 
valid argument  typable term 
sound argument, i.e. valid argument with correct premises  typable term whose free names refer to builtin values, e.g. a library function 
sequent  named context 
treelike structure of a natural deduction proof  abstract syntax tree of program 
conjunction of propositions  cartesian product of types 
disjunction of propositions  disjoint union of types 
negation of a proposition, ¬A, or A⇒⊥ 

deduction of proposition A as copy of an available hypothesis  variable (reference) of type A 
deduction ending with &introduction rule  pair expression 
deduction ending with &elimination rule  expression selecting first or second 
deduction ending with ⇒introduction rule  lambda expression 
deduction ending with ⇒elimination rule  application expression 
Pierce's law ((α ⇒ β) ⇒ α) ⇒ α 
call/cc 
interpretations 
A formula is the set of its possible deductions.  
intuitionistic meaning of a proposition what is required in order to prove a proposition  
intuitionistic meaning of a connective (e.g. &) or of a proof of a proposition based on a connective i.e. a converter of proofs  function 
proposition P is provable  type P is inhabited by some term 
constructive proof of α⇒β 
A “constructive” program of type α→β takes inputs of type α to outputs of type β. 
classical proof of α⇒β 
A “classical” program of type α→β given an input of classical type α may jump to another context. Otherwise it will return a classical value of type β to the current context. Context jumps may lurk in values. 
transformations 
normalization/simplifying a proof  normalization/execution/evaluation of a term 
classical logic embedded into constructive logic 
cps (continuation passing style) program transformation 
systems 
constructive/intuitionistic logic  typed lambda calculus 
second order constructive logic  quantification over types (System F) 
linear logic  linear type systems 
sound proof procedure, i.e. provable formulas are valid  type system that is safe/sound, i.e. Evaluation of a welltyped term whose free names are resolved will either terminate or continue without error. 