Stephanie Weirich posted the slides from her presentation at PLPV 2010 about Trellys. You can find them here. We are currently hard at work on the design of the core language. I expect it will be completed sometime this spring. Part of the challenge is sifting through the rich existing literature on type theory, to extract features that will be useful for very expressive programming (with general recursion, which type theory does not handle so naturally up to now), while discarding the features that are more appropriate for formalized logic and mathematics (e.g., features giving the languages profound proof-theoretic strength).