Cgc

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