README

This is the full Agda development which accompanies the paper draft
“Constructive Galois Connections: Taming the Galois Connection Framework for
Mechanized Metatheory” by Darais and Van Horn.

- Prelude.agda: 
  - Sets up a basic standard library.
- Poset.agda:
  - Develops posets, monotonic functions, monotonic powersets, and a
    calculational “proof mode”
- Poset/GaloisConnection.agda:
  - Develops classical, Kleisli and constructive Galois connections, and their
    metatheory properties like soundness and completeness.
- CDGAI.agda:
  - Develops Cousot's “The Calculational Design of a Generic Abstract
    Interpreter” for arithmetic expressions.
  - CDGAI/EnvAbstraction.agda     -- Abstraction for environments
  - CDGAI/ZAbstraction.agda       -- Abstraction for integers
  - CDGAI/ASyntax.agda            -- Arithmetic Syntax
  - CDGAI/ASemantics.agda         -- Arithmetic Semantics
  - CDGAI/AExpAbstract.agda       -- The calculated generic arithmetic abstract interpreter
  - CDGAI/BSyntax.agda            -- Comparison Syntax
  - CDGAI/BSemantics.agda         -- Comparison Semantics
  - CDGAI/BSemanticsAbstract.agda -- The calculated generic comparison abstract interpreter
  - CDGAI/BSyntax.agda            -- Command Syntax
  - CDGAI/BSemantics.agda         -- Command Semantics
  - CDGAI/BSemanticsAbstract.agda -- The calculated generic command abstract interpreter
- AGT.agda:
  - Develops the simply typed metatheory from Garcia, Clark and Tanter's
    “Abstracting Gradual Typing”.
  - AGT/Precise.agda  -- The initial precise type system with subtyping
  - AGT/Gradual.agda  -- The derived gradual type system with subtyping

Typechecking CDGAI.agda and AGT.agda will trigger typechecking the whole
development, which we provide a command for in the Makefile. To typecheck the
development run:

    make

We are using Agda version 2.5.3