/gradual-typing-in-agda

Formalizations of Gradually Typed Languages in Agda

Primary LanguageAgda

gradual-typing-in-agda

Formalizations of Gradually Typed Languages in Agda

Inventory

  • Labels.agda: Definition of blame labels.

  • Types.agda: Definition of gradual types and operators on them, such as precision, consistency, etc.

  • Variables.agda: Definition of variables as de Bruijn indices.

  • GTLC.agda: Syntax and type system of the Gradually Typed Lambda Calculus with pairs and sums.

  • GTLC-materialize.agda: A version of the GTLC that uses the materialize rule (subsumption with precision) instead of using the consistency relation.

  • PreCastStructure.agda: A record definition PreCastStruct that abstracts the representation of a cast. It includes a type constructor Cast for casts, operations on casts (e.g. dom and cod) and categories of casts (Active, Inert, Cross). This record definition does not depend on the definition of terms.

  • CastStructure.agda: contains two record definitions: the CastStruct record and the EfficientCastStruct. The CastStruct record extends PreCastStruct with an applyCast operation that applies an active cast to a value to produce a term. The EfficientCastStruct record also extends PreCastStruct with an applyCast operation, but also includes a compose operation for compressing two casts into a single cast.

  • ParamCastCalculus.agda: Syntax and type system (it is intrinsically typed) for the Parameterized Cast Calculus.It is parameterized over a type constructor Cast. This includes the definition of substitution.

  • ParamCastAux.agda: defines Value, Frame, plug, the wrapper reductions based on the idea of eta expansion, and proves a canonical forms lemma for type dynamic. This module is parameterized over a PreCastStruct.

  • ParamCastReduction.agda: Reduction rules and proof of type safety for the Parameterized Cast Calculus, parameterized over a CastStruct.

  • EfficientParamCastAux.agda: defines SimpleValue, Value, and proves a canonical forms lemma for type dynamic. This module is parameterized over PreCastStruct.

  • EfficientParamCasts.agda: A space-efficient reduction relation for the parameterized cast calculus. This module requires a compose function for casts, so it is parameterized over EfficientCastStruct. This module includes a proof of progress.

  • GTLC2CC.agda: Compilation of the GTLC to the Parameterized Cast Calculus. The compilation is type preserving.

  • GroundCast.agda: Type safety of λB (Siek, Thiemann, Wadler 2015). ("lazy UD" of Siek, Garcia, and Taha 2009)

  • GroundCoercion.agda: Type safety of λC (Siek, Thiemann, Wadler 2015). ("lazy UD" of Siek, Garcia, and Taha 2009)

  • EfficientGroundCoercions.agda: Type safety of λS (Siek, Thiemann, Wadler 2015). ("lazy UD" of Siek, Garcia, and Taha 2009)

  • SimpleCast.agda: Type safety of the cast calculus of Siek and Taha (2006). (Called "partially-eager D" by Siek, Garcia, and Taha 2009).

  • SimpleFunCast.agda: The same as above but casts between function types are values.

  • SimpleCoercions.agda: Type safety for the cast calculus of Siek and Taha (2006) again, but the calculus is expressed with coercions.

  • LazyCast.agda: Type safety for the "lazy D" calculus (Siek, Garcia, and Taha 2009).

  • LazyCoercions.agda: Type safety for the "lazy D" calculus, with casts represented as coercions.

  • AGT.agda: A space-efficient version of the GTLC inspired by Abstracting Gradual Typing (Garcia, Clark, and Tanter 2016). This is also closely related to the threesomes of Siek and Wadler (2011).

  • AbstractMachine.agda: A space-efficient abstract machine. It's a variant of the SECD machine with optimized tail calls. It's parameterized with respect to casts.

  • GroundMachine.agda: The abstract machine instantiated with the coercions from λS. ("lazy UD")

  • HyperCoercions: A alternative to λS that optimizes the coercion representation by removing indirections. ("lazy UD")

  • EquivCast: Proof of equivalence (simulation) between two instances of the Parameterized Cast Calculus.

  • EquivLamBLamC: Proof that λC simulates λB, by insantiating the above EquivCast module.

  • ForgetfulCast: Inspired by Greenberg's forgetful contracts. (UNDER CONSTRUCTION)