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).