Specifying Languages

Jaro Reinders

I’ll be talking about how to specify languages type theoretically in Agda, instead of the usual specification in terms of sets of strings. Conal Elliot has demonstrated how to do this for regular languages. We will be taking a look at context-free and perhaps also data-dependent languages. Fixed points are an important technique I use to accomplish this, but encoding them in Agda is difficult. This research is very much work in progress; I will discuss the complications I have encountered and potential solutions.

---

Previous: | Formalizing "Weakest preconditions in fibrations"
Next: