[Prev][Next][Index][Thread]

Natural Deduction vs. Sequenzen systems



Thank you for the elucidation of this difference.  On the other hand, the
"typical" usage I have seen is

Gamma |- M:t

where Gamma ranges over "sets of type hypotheses" or sometimes "maps from
variable symbols to types" (or typeschemes), the language about Gamma being a
set or (finite) map is intended to embrace the missing structural rules.

Keeping track of the sets of assumptions in such an explicit way seems
important if the system is to be easily mechanizable.

What would you call this kind of formulation?


Mitchell Wand
College of Computer Science
Northeastern University
360 Huntington Avenue #161CN
Boston, MA 02115

CSNet:  wand@corwin.ccs.northeastern.edu