Natural Deduction vs. Sequenzen systems

• To: majrh%PYRAMID.SWANSEA.AC.UK@MITVMA.MIT.EDU
• Subject: Natural Deduction vs. Sequenzen systems
• From: Mitchell Wand <wand%corwin.ccs.northeastern.edu@RELAY.CS.NET>
• Date: Tue, 31 May 88 21:59:02 EDT
• Cc: types@THEORY.LCS.MIT.EDU
• In-Reply-To: majrh's message of 31 May 1988 15:48:46-GMT-0:00 <8805311616.AA02106@THEORY.LCS.MIT.EDU>

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

• Prev: No Subject
• Next: specification logic and call by name
• Index(es):
  • Main
  • Thread