- 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