Assorted notes on logic and lambda-calculus

The goal of these notes is (usually) to crystallize the ideas behind some basic theorems in a "minimalistic" and self-contained way, using few pages and no advanced technology.

• Weak evaluation strategies in the lambda-calculus
  
• Basic propositional logic
  
• Continuation passing style translation
  
• Weak normalization of the simply typed lambda-calculus
  
• Strong normalization of the simply typed lambda-calculus
  
• Decidability of head normalization for RPSs
  
• Substitution lemma with de Bruijn indices
  
• Friedman's translation
  
• Completitud de deducción natural para lógica proposicional clásica
  
• Notas sobre verificacionismo computacional