Hello, I have just added Mendori, an experimental implementation of a logical framework with dependently typed records, to the CVS repository. The code is still buggy and unstable, but it might be of interest to some of you. Jeff Polakow JST CREST researcher AIST Research Center for Verification and Semantics email: j-polakow at aist.go.jp