Every problem that is interesting is also soluble. David Deutsch

• Thesis on InvarGenT: Attach:lukstafi-phd-thesis.pdf.
• Technical slides on InvarGenT: Attach:invargent-slides.pdf.
• Layman slides on InvarGenT: Attach: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.

• Attach:invargent2012.pdf formalizes both the type system and constraint solving by abduction, but does not cover existential types.
• Attach: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. [1] (initial constraint generation)
• Martin Sulzmann, Tom Schrijvers and Peter J. Stuckey, Type Inference for GADTs via Herbrand Constraint Abduction [2] (how to “solve” implications)
• Sergey Berezin, Vijay Ganesh, and David L. Dill, An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic [3] (how to eliminate variables from linear inequalities)
• Kenneth Knowles, Cormac Flanagan, Type reconstruction for general refinement types [4]

Other literature that seemed relevant at an early stage:

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

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

Copyright © 2005–2006 the Main wiki and its authors