[TYPES] Localizing Hypotheses?

Gershom B <[email protected]>
Newsgroups gmane.comp.science.types
Message-ID <CAM8RHpE7ciE4qAPQa1Zad098GsNA8Afv-1sUi-4M_Spau7kC1w@mail.gmail.com>
[ 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
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.