Are the terms and the types of Martin-Löf type theory described by context-free grammars? Have such grammars been written down somewhere?
Generally, there will be one context-free grammar for both types and terms, and judgements will be used to identify those expressions which are types and which expressions are terms of a particular type.
This has been written down many, many times. For a pretty typical example, you could look at Abel, Coquand and Dybjer's LICS 2007 paper, Normalization by Evaluation for Martin-Löf Type Theory with Typed Equality Judgements.