Journal: May & June - shaolintl/fstar-type-checker GitHub Wiki

Reflection

Tasks

• Implement simple example programs to be type-checked in ELPI
• Thoroughly understand ELPI implementations of PTS'
• Post VC's from F* programs
• Update ELPI kernel to latest version

Technical Issues & Questions

• To think about: how to handle syntax/data types from F* in ELPI environment
• To think about: how to handle constraints which are usually passed to Z3 - rule for Z3?
• Unannotated/annotated F* terms
• F* dependencies/namespace issues

Skills Developed

• F* & ELPI Programming
• Tons learned in type theory/logic