  In recent years, the interest in using proof assistants to formalise and
reason about mathematics and programming languages has grown. Type-logical
grammars, being closely related to type theories and systems used in functional
programming, are a perfect candidate to next apply this curiosity to. The
advantages of using proof assistants is that they allow one to write formally
verified proofs about one's type-logical systems, and that any theory, once
implemented, can immediately be computed with. The downside is that in many
cases the formal proofs are written as an afterthought, are incomplete, or use
obtuse syntax. This makes it that the verified proofs are often much more
difficult to read than the pen-and-paper proofs, and almost never directly
published. In this paper, we will try to remedy that by example.
  Concretely, we use Agda to model the Lambek-Grishin calculus, a grammar logic
with a rich vocabulary of type-forming operations. We then present a verified
procedure for cut elimination in this system. Then we briefly outline a CPS
translation from proofs in the Lambek-Grishin calculus to programs in Agda. And
finally, we will put our system to use in the analysis of a simple example
sentence.
