# Reference for context-free grammar for Martin-Löf type theory

Are the terms and the types of Martin-Löf type theory described by context-free grammars? Have such grammars been written down somewhere?

• Will all the strings produced by this grammar be typeable? Can't I write something like $a\to b$ where $a$ and $b$ are both terms? – neinoa Apr 26 at 13:38
• @MartinBerger but then I could also declare my formal language to be all finite sequences of $\Pi, \Sigma, \mathbf{0}, \mathbf{1}$ etc. and just typecheck that right? Is there say a context-sensitive grammar that is guaranteed to generate typeable things? – neinoa Apr 26 at 17:37
• @neinoa Yes, that't a viable approach. It's called generate-and-filter. It tends not to be very effective, since almost all finite sequences over the alphabet $\{\Pi, \Sigma, ...\}$ are not typable. I imagine that typable terms have asymptotic density 0. However, you can 'read typing rules backwards' and generate only typable terms. – Martin Berger Apr 26 at 17:57