TAL-GC proofs (in ascii)

• Language definition
• Preservation, progress
• Termination
• Draft submission (pdf), errata:
  • Section 5, expression/coercion termination: C |- e:t should be C |- e1:t, and C |- c:t should be C |- c1:t
  • Figure 6, last two lines: should say !(t^\circ G H R M) and !(u^\circ G H M) (i.e. the "!" was omitted)
• Annotated garbage collector (a single text file wrapped in a Windows installer file)

Feb 21, 2006: posted annotated garbage collector.

Linear aliasing proofs (in ascii)

• CC0
• CC1
• CC2
• LC
• Linear F-omega
• LC+nonlinear capabilities (for complete collection)
• CC/CCL
• CC/SLL

(Some of the linear F-omega proof is written in ML; contact me if you'd like a copy of the ML code.)

Sep 1, 2005: posted CC,CC1,CC2,LC,Linear F-omega, LC+nc.

Oct 20, 2005: added CC/CCL and CC/SLL; renamed CC to CC0.