paper announcement

• To: types@dcs.gla.ac.uk
• Subject: paper announcement
• From: dam@ai.mit.edu (David McAllester)
• Date: Thu, 20 Jan 94 13:31:10 EST
• Approved: types@dcs.gla.ac.uk

There is a (somewhat) new paper available by anonymous ftp in the
file ftp.ai.mit.edu:/pub/dam/strong.ps

Here is a title and abstract

A Proof of Strong Normalization for $F_2$, $F_\omega$, and Beyond.

by D. McAllester, J, Kucan, and D. Otth
(dam@ai.mit.edu, kucan@theory.lcs.mit.edu, Otth@theory.lcs.mit.edu)

{\abstract{ We present a new kind of proof of strong normalization for
$F_2$. The proof establishes invariants of the inference rules by
defining an appropriate semantics for the type assertions and showing
that the inference rules are sound relative to this semantics.  Strong
normalization is then a simple corollary of soundness. The proof
easily generalizes to more complex typing systems like $F_\omega$. We
also explore extensions of $F_\omega$ for which the proof holds. We
argue that the new proof technique is more natural and can be more
easily used as a general method for proving properties of reduction in
a variety of typing systems. }}

• Prev: categorical treatment of F_omega?
• Next: Intuitionistic Sets and Ordinals (paper by FTP)
• Index(es):
  • Main
  • Thread