tag:blogger.com,1999:blog-11162230.post6114645721109977066..comments2018-05-16T14:31:48.407-07:00Comments on Jeremy Siek: Revisiting "well-typed programs cannot go wrong"Jeremy Siekhttps://plus.google.com/115359947417709201623noreply@blogger.comBlogger1125tag:blogger.com,1999:blog-11162230.post-29349876008921274052017-06-18T15:58:31.851-07:002017-06-18T15:58:31.851-07:00I think this looks really interesting.
Can you al...I think this looks really interesting.<br /><br />Can you also show strong normalization of System F without fix? If you can, where are you using the extra proof-theoretic power to make that possible? Proof and Types explains, more or less, that consistency of System F implies consistency of Peano Arithmetic (PA), so by GĂ¶del's theorems you need more than PA to prove System F consistent.<br /><br />Is this model parametric? The post doesn't say much about the rule for polymorphic abstractions, but it seems you're in a sense taking the intersection of all their possible types, which I think is an existing approach but not the most common one.Paolo Giarrussohttps://www.blogger.com/profile/04485097839438234853noreply@blogger.com