[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
In the course notes for Automated Theorem Proving (2004) [1], Pfenning describes the introduction of contexts in a Natural Deduction system as "Localizing Hypotheses" (see section 2.3). I cannot find many other examples of this terminology. Is this just a felicitous turn of phrase, or is there literature that makes the connection explicit to familiar notions of localization in, for example, algebraic, category-theoretic, or topos-theoretic settings? [1] http://www.cs.cmu.edu/~fp/courses/atp/handouts/ch2-natded.pdf Thanks, Gershom
