• View
• Edit
• History
• Print

Infer

Every problem that is interesting is also soluble. David Deutsch

• Thesis on InvarGenT: lukstafi-phd-thesis.pdf Δ.
• Technical slides on InvarGenT: invargent-slides.pdf Δ.
• Layman slides on InvarGenT: invargent-simple-slides.pdf Δ.

Implementation of versions 2.0.X completed.

These unpublished articles can serve as historical snapshots of formal presentation of the project.

• invargent2012.pdf Δ formalizes both the type system and constraint solving by abduction, but does not cover existential types.
• invargent2013.pdf Δ focuses on the type system.
• Project at: https://github.com/lukstafi/invargent, in particular InvarGenT manual.

Literature that directly influenced this work:

• Vincent Simonet and Francois Pottier, A constraint-based approach to guarded algebraic data types. (initial constraint generation)
• Martin Sulzmann, Tom Schrijvers and Peter J. Stuckey, Type Inference for GADTs via Herbrand Constraint Abduction (how to “solve” implications)
• Sergey Berezin, Vijay Ganesh, and David L. Dill, An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic (how to eliminate variables from linear inequalities)
• Kenneth Knowles, Cormac Flanagan, Type reconstruction for general refinement types

Other literature that seemed relevant at an early stage:

• Enric Rodriguez-Carbonell, Deepak Kapur, Automatic Generation of Polynomial Loop Invariants
• M. Maher, Abduction of Linear Arithmetic Constraints
• Deepak Kapur, Automatically Generating Loop Invariants Using Quantifier Elimination

There is much more of related literature, mostly more recent, but it has not influenced InvarGenT directly.