Journal: April - shaolintl/fstar-type-checker GitHub Wiki

Reflection

Bullet points for later use in expository format in final essay

• How do academics, moreover researchers, measure their sense of productivity?
• Appreciating an idea is far above merely having some cognitive understanding, and nothing replaces time and experience

Tasks for the Month

Insert in order of dependency

• Write type checker in ELPI for limited type systems like the Lambda-pi system here
• Study "Dependent Types" chapter from Advanced Topics in Types and Programming Languages (Pierce et al.) also Part 6 in introductory text
• Fully type check the following F* program by extending this proof using the type checking rules of micro-F* and EMF*.

val simple: x:int{x>=0} -> Tot int                                                                                                            
let rec simple n =
  if n = 0 then 1 else n + (simple (n - 1))

• Compare type systems in the aforementioned Pierce chapter with the rules seen in F*
• probably beginning May & onward Compile subset of F* into LP

Technical Issues & Questions

• ELPI: Run-time context expansion and evaluation
• ELPI: type annotations with "of" predicate vs. type declaration

Skills Developed

• OCaml and data structures
• Implementing elementary type systems in ELPI