plum-umd / cgc
Licence: other
Constructive Galois connections
Stars: ✭ 29
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
Note that the project description data, including the texts, logos, images, and/or trademarks,
for each open source project belongs to its rightful owner.
If you wish to add or remove any projects, please contact us at [email protected].