Open vjovanov opened 9 years ago
Define formal proof. Are you going to write code in theorem provers? Because otherwise it's not formal according to PL people.
Yes, Sandro says it is addictive so I want to try it over the break.
System F or System Fsub? Subtyping doesn't play nice with recursive structural types.
@sstucki which one do you have?
So we can not prove our calculus sound in 4 days, however, we can state what we want to prove and provide a link to the repo where we have formal poofs in progress.
BTW, @sstucki is working on a System F with recursive types. I think we can pick it up from there and guide his proofs towards inline.