Type Based Terminaison
During the internship of Fernando Pastawski, we have introduced a polymorphic λ-calculus (CIC^) that features inductive types and enforces termination of recursive definitions through typing. Then, we have defined a sound and complete type inference algorithm that computes a set of constraints to be satisfied for terms to be typable, and shows that constraint satisfiability can be decided efficiently.A simple version of the polymorphic calculus (F^) is presented toghether with a type inference algorithm in this publication.
Outstanding issues wich allow establishing the theory for (CIC^), a dependent type system enforcing termination are presented in this extended article.
This is my implementation of a version of CIC^ (pronounce CIC sombrero), where I pay attention to minimize the set of constraints returned.
The best way to understand the syntax is to read the files in directory "exemples"
- In file "nat.cic" some examples on nat:
- plus, minus, min, max
- two versions of ackerman
- log2
- Some counterexemples
- In the file "quicksort.cic" a more complexe example:
- Definition and proof of quicksort !!!