  Galois connections are a foundational tool for structuring abstraction in
semantics and their use lies at the heart of the theory of abstract
interpretation. Yet, mechanization of Galois connections using proof assistants
remains limited to restricted modes of use, preventing their general
application in mechanized metatheory and certified programming.
  This paper presents constructive Galois connections, a variant of Galois
connections that is effective both on paper and in proof assistants; is
complete with respect to a large subset of classical Galois connections; and
enables more general reasoning principles, including the "calculational" style
advocated by Cousot.
  To design constructive Galois connections we identify a restricted mode of
use of classical ones which is both general and amenable to mechanization in
dependently-typed functional programming languages. Crucial to our metatheory
is the addition of monadic structure to Galois connections to control a
"specification effect." Effectful calculations may reason classically, while
pure calculations have extractable computational content. Explicitly moving
between the worlds of specification and implementation is enabled by our
metatheory.
  To validate our approach, we provide two case studies in mechanizing existing
proofs from the literature: the first uses calculational abstract
interpretation to design a static analyzer; the second forms a semantic basis
for gradual typing. Both mechanized proofs closely follow their original
paper-and-pencil counterparts, employ reasoning principles not captured by
previous mechanization approaches, support the extraction of verified
algorithms, and are novel.
