This directory contains the current version of the Twelf proofs for
"Elaborating Intersection and Union Types", which first appeared at ICFP 2012.
An extended version was submitted to JFP, where one reviewer noticed
that Lemma 9 (Intersections/Pairs), "elab-sect" in elab-sect.elf,
was unnecessarily complicated.  I have replaced it with a simpler version.

To maintain hyperlinks from the ICFP paper, the old version remains at

  http://www.cs.cmu.edu/~......./intcomp/

but is now of only historical interest.  [That link no longer works -Jana, 2021]

(The only changes are to elab-sect.elf, which is substantially simpler,
and consistency.elf, which is very slightly simpler.)

--Jana Dunfield
  2013-08-18