Infer

* Draft of my thesis on InvarGenT: [[Attach:lukstafi-phd-thesis.pdf]].

Draft of my 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]].

Draft of my thesis on InvarGenT: [[Attach:lukstafi-phd-thesis.pdf]]
The thesis is not yet submitted.

* 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.

* [[http://pauillac.inria.fr/~fpottier/biblio/pottier.html | Vincent Simonet and Francois Pottier, '''A constraint-based approach to guarded algebraic data types.''']] [5] (initial constraint generation)

* [[http://www.kennknowles.com/research/knowles-flanagan.esop.07.type.pdf | Kenneth Knowles, Cormac Flanagan, '''Type reconstruction for general refinement types''']] (that type-checking and type inference are separate things)

Implementation of version 1.1 completed.

Implementation of v1.2 with @@min@@ and @@max@@ relations in @@num@@:
(:progress 45:)

* Project at: [[https://github.com/lukstafi/invargent]].

(:progress 2:)

(:progressbar 32:)

(:progressbar 02:)

(:progressbar 2:)

* 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.

* These unpublished articles can serve as historical snapshots of formal presentation of the project: [[Attach:invargent2012.pdf]], [[Attach:invargent2013.pdf]].

* Article introducing the theoretical underpinnings of the project: [[Attach:invargent2012.pdf]].
* [[http://ii.uni.wroc.pl/~lukstafi/pubs/ | Technical reports / manuscripts]].

Implementation progress: (:progress 93:)

Other relevant literature:
* [[http://www.lsi.upc.edu/~erodri/ | Enric Rodriguez-Carbonell, Deepak Kapur, '''Automatic Generation of Polynomial Loop Invariants''']] (how to infer polynomial function invariants, work in progress) detection of loop invariants by abstract interpretation turns out to be very relevant
* [[http://www.cse.unsw.edu.au/~mmaher/pubs/cp/linear_abdn_revised.pdf | M. Maher, '''Abduction of Linear Arithmetic Constraints''']] (this is what the program actually does)
* [[http://www.cs.unm.edu/~kapur/mypapers/aca2004.pdf | Deepak Kapur, '''Automatically Generating Loop Invariants Using Quantifier Elimination''']] (I'll use this solution for linear inequalities, I haven't decided about polynomials yet)

Implementation progress: (:progress 88:)

Implementation progress: (:progress 82:)

Implementation progress: (:progress 77:)

Implementation progress: (:progress 73:)

Implementation progress: (:progress 65:)

Implementation progress: (:progress 55:)

Implementation progress: (:progress 40:)

Implementation progress: (:progress 38:)

Implementation progress: (:progress 30:)

Implementation progress: (:progress 27:)

Implementation progress: (:progress 20:)

Implementation progress: (:progress 17:)

Implementation progress: (:progress 10:)

[[http://ii.uni.wroc.pl/~lukstafi/pubs/ | Manuscripts with my results.]]

OUTDATED. The project will have a dedicated site soon.

The first version of my project which hasn't got name yet, is codenamed HMG Arith. It is not HMG(Arith) actually, because it doesn't have type annotations on recursive definitions. No type annotations at all. This is unofficial revision 0.1 of HMG Arith, work in progress, avoid the flood of diagnostic information by directing stderr to /dev/null.

[[Attach:hmg_arith.tar.gz]]

Relevant literature I'm reading now:

||  1|| v0.1.1|| multiple definitions|| simple|| done [[~lukstafi]] July 20, 2008, at 01:15 PM

|| 13|| v0.1.1|| mutual recursion|| difficult|| done [[~lukstafi]] August 15, 2008, at 10:26 PMlukstafi

|| 13|| v0.1.1|| mutual recursion|| difficult|| in progress

|| 41|| v0.1.2|| simplify accounting of local variables|| simple|| in progress
|| 39|| v0.1.2|| rewrite invariant generation code (simplify representations)|| medium|| in progress

|| 41|| v0.1.2|| simplify accounting of local variables|| simple|| waiting

||  1|| v0.1.1|| multiple definitions|| simple|| done [[~lukstafi]]

||  1|| v0.1.1|| multiple definitions|| simple|| in progress
||  2|| v0.1.1|| nested "non-crossing" definitions|| simple|| in progress

||  5|| v0.1.1|| cleaned-up output|| simple|| waiting

|| 39|| v0.1.2|| rewrite invariant generation code (simplify representations)|| medium|| waiting

|| 39|| v0.2.0|| rewrite invariant generation code (simplify representations)|| medium|| waiting

|| 15|| v0.3.1|| return-type-nested existential quantification|| difficult|| waiting
|| 16|| v0.3.2|| Haskell-like syntax input (and more complete OCaml syntax)|| medium|| waiting
|| 17|| v0.3.2|| Haskell source code generation|| medium|| waiting
|| 18|| v0.3.2|| OCaml source code generation|| medium|| waiting
|| 29|| v0.3.2|| handle and transfer comments (also: full types as comments)|| simple|| waiting
|| 30|| v0.3.2|| extend testsuite to run the examples|| simple|| waiting
|| 32|| v0.3.3|| source-level transformation to flatten (move out) non-mutual-recursive local definitions|| simple|| waiting
|| 33|| v0.3.3|| user type annotations in expressions|| simple|| waiting
|| 34|| v0.3.4|| user constraint annotations on defined functions|| medium|| waiting

|| 27|| v0.2.0|| check for exhaustiveness of patterns|| medium|| waiting

|| 35|| v0.2.0|| add multiplication back to the arithmetic domain|| simple|| waiting

|| 25|| v0.5.0|| first class polymorphism (annotation-free)|| perhaps possible|| waiting
|| 26|| v0.6.0|| type definition reconstruction and refinement|| perhaps possible|| waiting

||  1|| v0.1.1|| multiple definitions|| simple|| waiting
||  2|| v0.1.1|| nested "non-crossing" definitions|| simple|| waiting
||  3|| v0.1.1|| pattern implication|| medium|| waiting

|| 13|| v0.3.0|| mutual recursion|| difficult|| waiting
|| 14|| v0.3.1|| polynomial constraints|| difficult|| waiting
|| 15|| v0.3.2|| return-type-nested existential quantification|| difficult|| waiting
|| 16|| v0.3.3|| Haskell-like syntax input (and more complete OCaml syntax)|| medium|| waiting
|| 17|| v0.3.3|| Haskell source code generation|| medium|| waiting
|| 18|| v0.3.3|| OCaml source code generation|| medium|| waiting
|| 29|| v0.3.3|| handle and transfer comments (also: full types as comments)|| simple|| waiting
|| 30|| v0.3.3|| extend testsuite to run the examples|| simple|| waiting

||  8|| v0.4.1|| quicksort with order detection|| simple|| waiting

||  7|| v0.4.1|| [[#choice]] operator for user constraints|| medium|| waiting

!!! The [[#choice]] operator

|| 16|| v0.3.3|| Haskell-like syntax input|| medium|| waiting

|| 30|| v0.3.3|| extend testsuite to run the examples|| waiting

||  7|| v0.2.0|| [[#choice]] operator|| medium|| waiting

|| 23|| v0.4.2|| Datalog domain (with saturation)|| medium|| waiting
|| 24|| v0.4.3|| equational theories domain (with completion)|| difficult|| waiting

The "Choice" logical connective "lifts the pattern-matching semantics to the logic of annotations", allows for overloading of logical senses of values. [@choice(a1==>b1, ..., an==>bn)@] means [@a1==>b1 /\ ... /\ an==>bn@] but is only admissible when [@a1 \/ ... \/ an@].

||  7|| v0.2.0|| disjunctions in user constraints|| simple|| waiting

||  1|| v0.2|| multiple definitions|| simple|| waiting
||  2|| v0.2|| nested "non-crossing" definitions|| simple|| waiting
||  3|| v0.2|| pattern implication|| medium|| waiting
||  4|| v0.2|| by-hand marked dead code|| medium|| waiting
||  5|| v0.2|| cleaned-up output|| simple|| waiting
||  6|| v0.2|| disjunctions in user constraints|| simple|| waiting
||  7|| v0.2|| existential quantification detection bugs|| medium|| waiting
||  8|| v0.2|| exact generation of inequalities by "quantifier elimination"|| difficult|| waiting
||  9|| v0.2|| enumeration of dark shadow in Fourier-Motzkin|| medium|| waiting
|| 10|| v0.3|| mutual recursion|| difficult|| waiting
|| 11|| v0.3|| polynomial constraints|| difficult|| waiting
|| 12|| v0.3|| return-type-nested existential quantification|| difficult|| waiting
|| 13|| v0.3|| Haskell-like syntax input|| medium|| waiting
|| 14|| v0.3|| Haskell source code generation|| medium|| waiting
|| 15|| v0.3|| OCaml source code generation|| medium|| waiting
|| 16|| v0.4|| domain for lattices|| difficult|| waiting
|| 17|| v0.4|| domain for reals|| medium|| waiting
|| 18|| v0.4|| Datalog domain (with saturation)|| difficult|| waiting
|| 19|| v0.4|| equational theories domain (with completion)|| difficult|| waiting
|| 20|| v0.5|| first class polymorphism (annotation-free)|| perhaps possible|| waiting
|| 21|| v0.6|| type definition reconstruction and refinement|| perhaps possible|| waiting

|| 18|| v0.4|| Datalog domain|| difficult|| waiting
|| 19|| v0.5|| first class polymorphism (annotation-free)|| perhaps possible|| waiting
|| 20|| v0.6|| type definition reconstruction and refinement|| perhaps possible|| waiting

||%border=1

||  #|| v0.2|| multiple definitions|| simple|| waiting
||  #|| v0.2|| nested "non-crossing" definitions|| simple|| waiting
||  #|| v0.2|| pattern implication|| medium|| waiting
||  #|| v0.2|| by-hand marked dead code|| medium|| waiting
||  #|| v0.2|| cleaned-up output|| simple|| waiting
||  #|| v0.2|| disjunctions in user constraints|| simple|| waiting
||  #|| v0.2|| existential quantification detection bugs|| medium|| waiting
||  #|| v0.2|| exact generation of inequalities by "quantifier elimination"|| difficult|| waiting
||  #|| v0.3|| mutual recursion|| difficult|| waiting
||  #|| v0.3|| polynomial constraints|| difficult|| waiting
||  #|| v0.3|| return-type-nested existential quantification|| difficult|| waiting
||  #|| v0.4|| domain for lattices|| difficult|| waiting
||  #|| v0.4|| domain for reals|| medium|| waiting
||  #|| v0.4|| Datalog domain|| difficult|| waiting
||  #|| v0.5|| first class polymorphism (annotation-free)|| perhaps possible|| waiting
||  #|| v0.6|| type definition reconstruction and refinement|| perhaps possible|| waiting



Plans for future versions:
* more domains, the next one being lattices (partial orders with the minimum and maximum operators), later: reals, and user-defined rule-based (like in bottom-up logic programming)
* existential quantification (if introduced before first class polymorphism, then still nested in any return part of a type (always-right on function arrows path into the type): this is needed for types that are already inferred)
* first class polymorphism (universal and existential quantifiers nested in types) inspired by MLF


Bugs:
# binary_multiply.gadt: result should be existentially quantified

Further plans:
# domain of lattices (medium-to-difficult)
# domain of real numbers (simple-to-medium)
# enumeration of dark shadow on Fourier satisfiability (medium)
# factoring-out the code for domains -- plug-in architecture (medium-to-difficult) (small priority)
# rule-based saturation domain (medium-to-difficult)
# first-class polymorphism (difficult)
# export to compilable languages (medium)

* [[http://www.cs.unm.edu/~kapur/mypapers/aca2004.pdf | Deepak Kapur, '''Automatically Generating Loop Invariants Using Quantifier Elimination''']] (I eliminate branch-local variables anyway, so I could use this technique where appropriate)

* [[http://www.cs.unm.edu/~kapur/mypapers/aca2004.pdf | Deepak Kapur, '''Automatically Generating Loop Invariants Using Quantifier Elimination''']] (I eliminate branch-local variables anyway, so I could use this technique where appropriate)

* [[http://www.cs.unm.edu/~kapur/mypapers/aca2004.pdf | Deepak Kapur, '''Automatically Generating Loop Invariants Using Quantifier Elimination''']] (this is also what the program does)

* [[http://pauillac.inria.fr/~fpottier/biblio/pottier.html | Vincent Simonet and Francois Pottier '''A constraint-based approach to guarded algebraic data types.''']] [5] (initial constraint generation)
* [[http://citeseer.ist.psu.edu/henglein91type.html |  Fritz Henglein '''Type Inference with Polymorphic Recursion''']] (how to apply to type inference and solve semi-unification)
* [[http://www.cs.mu.oz.au/~sulzmann/manuscript/gadt-short.ps | Martin Sulzmann, Tom Schrijvers and Peter J. Stuckey '''Type Inference for GADTs via Herbrand Constraint Abduction''']] (how to "solve" implications)
* [[http://verify.stanford.edu/PAPERS/BGD03.ps | 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)
* [[http://www.kennknowles.com/research/knowles-flanagan.esop.07.type.pdf | Kenneth Knowles, Cormac Flanagan '''Type reconstruction for general refinement types''']] (that type-checking and type inference are separate things)

* [[http://www.lsi.upc.edu/~erodri/ | '''Automatic Generation of Polynomial Loop Invariants''']] (how to infer polynomial function invariants, work in progress) detection of loop invariants by abstract interpretation turns out to be very relevant

* [[http://www.cs.unm.edu/~kapur/mypapers/aca2004.pdf | Automatically Generating Loop Invariants Using Quantifier Elimination]] (this is also what the program does)

* [[http://www.cs.unm.edu/~kapur/mypapers/aca2004.pdf | Automatically Generating Loop Invariants Using Quantifier Elimination]] (this is also what the program does, in a limited form)

More literature:
* [[http://www.kennknowles.com/research/knowles-flanagan.esop.07.type.pdf | Kenneth Knowles, Cormac Flanagan '''Type reconstruction for general refinement types''']] (that type-checking and type inference are separate things)

# polished output (medium)

# factoring-out the code for domains -- plug-in architecture (medium-to-difficult)

* [[http://citeseerx.ist.psu.edu/viewdoc/summary;jsessionid=457D868A1C122657FAAE4EB004FEA2DA?cid=4503934 | Kenneth Knowles, Cormac Flanagan '''Type reconstruction for general refinement types''']] (that type-checking and type inference are separate things)
* [[http://www.cs.washington.edu/homes/deibel/papers/cse503-loop-invariants/cse503-loop-invariants.pdf | Katherine Deibel '''On the Automatic Detection of Loop Invariants''']] (that function invariants can actually be reconstructed)

Literature:
* [[http://pauillac.inria.fr/~fpottier/biblio/pottier.html | Vincent Simonet and Francois Pottier '''A constraint-based approach to guarded algebraic data types.''']] [5]
* [[http://citeseerx.ist.psu.edu/viewdoc/summary;jsessionid=457D868A1C122657FAAE4EB004FEA2DA?cid=4503934 | Kenneth Knowles, Cormac Flanagan '''Type reconstruction for general refinement types''']]
* [[http://citeseer.ist.psu.edu/henglein91type.html |  Fritz Henglein '''Type Inference with Polymorphic Recursion''']]
* [[http://verify.stanford.edu/PAPERS/BGD03.ps | Sergey Berezin, Vijay Ganesh, and David L. Dill '''An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic''']]

* more domains, the next one being lattices (partial orders with the minimum and maximum operators)
* existential quantification (if introduced before first class polymorphism, then still nested at least in any return part of a type (always-right on function arrows path into the type)

* [[http://pauillac.inria.fr/~fpottier/biblio/pottier.html | Vincent Simonet and Francois Pottier. '''A constraint-based approach to guarded algebraic data types.''']] [5]
* [[http://citeseerx.ist.psu.edu/viewdoc/summary;jsessionid=457D868A1C122657FAAE4EB004FEA2DA?cid=4503934 | Kenneth Knowles, Cormac Flanagan '''Type reconstruction for general refinement types.''']]
* [[http://citeseer.ist.psu.edu/henglein91type.html |  Fritz Henglein '''Type Inference with Polymorphic Recursion''']]

* [[http://pauillac.inria.fr/~fpottier/biblio/pottier.html | Vincent Simonet and François Pottier. '''A constraint-based approach to guarded algebraic data types.''']] [5]

The first version of my project which hasn't got name yet, is codenamed HMG Arith. It is not HMG(Arith) actually, because it doesn't have type annotations on recursive definitions. No type annotations at all. This is revision 0.1 of HMG Arith. The natural numbers domain constraints reconstruction is very slow, resulting in the @@split@@ function capability inference time being 1m10s on my computer. Revision 1.0 of HMG Arith is planned to be reasonably fast, or if that cannot be achieved, as fast as possible ;-)