TODO List

[Drup]

Software engineering

• Add tests
• Implement a proper notion of printing environment
• Use proper logging
• Plug together the unification and the database again

Science

• Make sure the returned unifiers are minimal
• Add rigid variables

Indexation:

• Head
• Nb of arguments ("Equal" or "At least")
• Variances of constants
• Term indexing:
  To Read:
  • http://wwwlehre.dhbw-stuttgart.de/~sschulz/PAPERS/Schulz2013-FVI.pdf
  • Fingerprint Indexing for Paramodulation and Rewriting

[Drup]

Reading list and/or references

• [RDC]: Di Cosmo (Roberto). - Isomorphisms of types: from
  lambda-calculus to information retrieval and language
  design. - Birkhauser, 1994.

• [Rit90] Mikael Rittri. Retrieving library identifiers by
  equational matching of types in 10th Int. Conf. on Automated
  Deduction. Lecture Notes in Computer Science, 449, July
  1990.

• [Rit91] Mikael Rittri. Using types as search keys in func-
  tion libraries. Journal of Functional Programming, 1(1):71-
  89, 1991.

Unification

• [Rit93] Mikael Rittri. Retrieving library functions by
  unifying types modulo linear isomorphism. RAIRO Theoretical
  Informatics and Applications, 27(6):523-540, 1993.

• [DJ90]

• Equality [SE94]

With modules

• [Mul; ZW93] ADC96; ADCD97

Serialization

To speed up database deserialization, we could use a format
that allows random access in an mmap datastructure.
Example of such formats:

• Cap'n Proto (OCaml implementation: capnp)
• Flatbuffer (No OCaml implementation)