Skip to content
No description, website, or topics provided.
Branch: thesisVersion
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.

The implementation accompanying the thesis "Improving Error Messages for Dependent Types with Constraint Based Unification", by Joseph Eremondi.

This code is a mismash of three existing projects:

Notable modules include:

  • ConstraintBased, a type-checking procedure generates constraints to be solved
  • Constraint, where LambdaPi constraints and values are converted into Gundry-McBride form
  • PatternUnify.Tm, where we define a value-form Lambda Calculus
  • PatternUnify.Context, where we define the Gundry-McBride metacontext and operations on it
  • PatternUnify.Unify, where the actual Gundry-McBride algorithm is implemented
  • Top.Implementation.TypeGraph.Standard, the main type-graph implementation
  • Top.Implementation.TypeGraph.DefaultHeuristics, where we implement a few heuristics used in error generation
You can’t perform that action at this time.