Post PhD Dule work in progress:

• There are several papers inside my Ph.D. waiting to be let out. I'd gladly welcome collaboration in tidying up, extending and publishing the results. Below are some paper ideas and drafts.
• In this paper about anonymous (co)inductive types inside modules we should disregard polymorphism via polytypism and insert a sketch of formal semantics.
• Analyze in which cases polymorphism via polytypism actually works and why. No need to stick to Dule here.
• Compare the lambda calculi with labels developed for OCaml with my calculus.
• Compare my categorical notation for the core language with lambda calculi with explicit substitutions. Find extensions or typed versions of Curien's Categorical Combinators and compare with my reduction system. However, as soon as (co)inductive combinators enter the arena, this is probably too much work (too large theories).
• Compare my LCC categories with Context Categories and their generalizations. Try to axiomatize my almost-2-categories and/or compare them with others. Present my 2-categorical setup with mixed variance as a 2-dimensional doctrine and/or co-Kleisli category, etc. Perhaps wait for axioms in module specifications, as they will require an indexed category, a fibration or another scary thing on top of all my current stuff, anyway.
• Show that in some (most?) papers and books about lambda calculus the theory of coproducts is not as strong as categorical theory, despite some papers and books claiming otherwise. My theory is OK, probably due to explicit substitutions/categorical composition and verification by adjunctions.
• Try to sensibly describe Dule as an ongoing project in module system design, and provide some more rationale for the design decisions and comparison with other ideologies.
• Sell the (co)inductive modules somehow. Perhaps allow folds over the modules' types, first. Anyway, before that, write a paper about the Simple Category of Modules; an update of the one I presented at IFL2007. Perhaps the nicest thing in there, is the representation of sharing equations as limits (with the proof that enough limits exist).
• Revisit the countless open problems listed in the Final Remarks section of my Ph.D. Some of them are easy, others look almost done... :)