§ Uniform proofs, focused proofs, polarization, logic programming

• Focusing and synthetic rules: http://requestforlogic.blogspot.com/2010/09/focusing-and-synthetic-rules.html
• girard statement about proofs as time; https://mathoverflow.net/a/179258/123769
• Focused proof
• Polarity in type theory: https://existentialtype.wordpress.com/?s=polarity
• PhD thesis of Noam Zeilberger, polarity: http://www.cs.cmu.edu/~noam/thesis.pdf