Roadmap for an F* type checker in lambda-prolog

Target

Create an external type checker for the F* language.

Benefits

• Increased confidence in F*
• Better understanding of its type system
• A reference implementation of F* type inference algorithm

Optional Benefits

• Logical specification of a future new F* type inference algorithm
• Establish new development approach in functional programming languages (LSDP - Logical specification driven programming)

Members

• Tomer Libal
• Keith Cannon

Method

Incrementally create different type systems and type checking algorithms in lambda-prolog in order to cover bigger and bigger subsets of F

• Use testing extensively
• Use documentation extensively
• document everything in the wiki
• Use ELPI for the implementation
• Follow closely the techniques used in the development of the CIC type system on the ELPI cic branch

Timeframe

During the internship of Keith Cannon in the Prosecco team of Inria, Paris. 1/4/2017-30/9/2017

Roadmap

• Programming in ELPI of STLC (simply typed lambda calculus) and a type checking algorithm for it
• learn ELPI
• understand CIC code
• establish testing/documentation skills
• document progress and required resources/papers in this wiki
• replace ground terms with variables and check possibility of type inference
• Programming in ELPI of a simple Hoare logic
• understand the type system
• implement it in ELPI
• further reading here
• use it to type check/infer examples (check with Catalin?)
• Extend with dependent types, sub-types, etc.