Towards Tagless Interpretation of Stratified System F (Extended Abstract)
summary
An intrinsically typed, tagless interpreter for a stratified fragment of System F is formalized in Agda: types carry natural-number levels and map to Set_l so quantifiers range only over lower levels, yielding a direct set theoretic semantics and an implementation of type meaning, function spaces and type variables. The development reuses a single environment for term and type bindings, must extend equality machinery at set Omega, and assumes dependent extensionality in a few proofs. All lemmas drop to simple ML fragments with minor changes, and work toward logical relations and adequacy is underway.
AI-written summary · about
chapters (12)
- 0:00Stratified System F formalization
- 1:45Predicative fragment and polymorphism
- 3:50Set-theoretic semantics in Agda
- 5:59Encoding System F Omega in Agda
- 8:06Intrinsically typed expressions
- 10:17Challenges with Set Omega proofs
- 12:26Extending calculus with polymorphism
- 13:55Stratified polymorphism with ordinals
- 14:37Applying results to ML
- 15:18Logical relations for stratified F
- 16:02Summary and future work
- 16:22Q&A
related talks
42mFunctional interpreters and you
31mDependent tagless final
01h 05mAll the Languages Together
18mQualifying System F-sub
14mType-Sensitive Algebraic Macros
18mThe Essence of Generalized Algebraic Data Types
16mIntriniscly-Typed Interpretation of Linear Languages
16mTowards formally secure compilation of verified F* programs against unverified ML(…)