Some not-completely-throwaway Agda stuff of mine.
- dfa.agda — Proof that regular languages are closed on union and intersection.
- lambda-mu.agda — Formalization of Parigot's λμ calculus.
- mutate.agda — Formalization of mutable state, as described in Wouter Swierstra's dissertation.
- pactran.agda — Correctness of the package transform by Rivest (1997).