[TYPES] Localizing Hypotheses?
Gershom B
gershomb at gmail.com
Mon Mar 2 18:06:54 EST 2015
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
More information about the Types-list
mailing list