Journal: May & June

Jump to bottom

Keith Reilly Patrick Cannon edited this page Jun 18, 2017 · 1 revision

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