Progress tracking of converting Twelf examples to Beluga:

alloc-sem       Simply Typed Lambda-Calculus with a small-step, allocation semantics
                (Brigitte, Part 1 done; )

arith           Associativity and commutativity of unary addition (done)

ccc             Cartesian-closed categories [incomplete]
                (Renaud, Brigitte, Part 1 done)

church-rosser   The Church-Rosser theorem for untyped lambda-calculus 
		(Brigitte, part 1 done)


compile         Various compilers starting from Mini-ML
                cls (Brigite, Part 1: done
                              Part 2: completeness  done, soundness: to do)
                cpm (Brigitte, Part 1: done (sources.cfg)
                               Part 2: soundness done, 
                                       completeness done,
                                       equivalence of soundness and completeness proof omitted
                                       (test.cfg)
                    )
                cps (Brigitte, Part 1 done)
                cxm (Brigitte, done)
                debruijn  (Brigitte, Part 1 done ; Part 2: attempt can be found in examples)
                debruijn1 (Brigitte, Part 1 done ; 
                                     Part 2: Bisimulation proof both directions done)

cpsocc          CPS conversion and stack-based machines [in progress]
                (Brigitte, Part 1 done)

cut-elim        Cut elimination for intuitionistic and classical logic
                ( Brigitte, part 1,  intuitionistic part 2 done )

fol             Simple theorems in first-order logic
	        (Brigitte, part 1 done, part 2 done)


guide           Examples from Users' Guide
                (Brigitte, part 1 done)


handbook        Examples from article in Handbook of Automated Reasoning
                (Brigitte, part 1 done)

incll           Meta-interpreter for int. non-commutative linear logic

kolm            Kolmogorov translation from classical to intuitionistic logic
                (Brigitte, part 1 done)


fj              The soundness of Featherweight Java

lp              Logic programming, uniform derivations
		(NOTE: Needs typing annotation for isc_all in uni_sound.elf 
                       we need to add this to our implementation.
		 )
		(Brigitte part 1 done)

lp-horn         Horn fragment of logic program
                (Brigitte part 1 done)

mini-ml         Mini-ml, type preservation and related theorems
                (Brigitte part 1 done, part 2 done)

modal           Examples of encoding modal logics in Twelf
                (Joshua)

polylam         Polymorphic lambda-calculus
		(Brigitte part 1 done)

prop-calc       Natural deduction and Hilbert propositional calculus
                (Brigitte part 1 done; )

small-step      Brief tutorial on proving progress and preservation in Twelf
                 - lam.elf      
                 - system-f.elf 
                 - system-f-iso.elf
		 (Brigitte part 1 done , part 2 done)


tapl-ch13       A formalization of Chapter 13 from "Types and Programming Languages"
                (Joshua) 


------------------------------------------------
In Twelf-1-5 we only find:

arith/				   ccc/
church-rosser/			   compile/
cpsocc/				   cut-elim/
fol/				   guide/
handbook/			   incll/
kolm/				   lp-horn/
lp/				   mini-ml/
polylam/			   prop-calc/
tabled/				   units/