<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body>
<p>Hi,</p>
<p>I know that this is probably not the correct place to ask as my
question is not directly related to GHC itself, but I thought here
are the people that can most likely answer this.</p>
<p>To better understand PL papers, especially those involving System
Fc and its extensions, I started to write a formal proof of type
safety including alpha-equivalence. Currently I have <a
moz-do-not-send="true"
href="https://github.com/jvanbruegge/isabelle-lambda-calculus">a
complete proof for System F</a> (without coercions and data
types yet). I mainly used the <a moz-do-not-send="true"
href="https://www.microsoft.com/en-us/research/wp-content/uploads/2007/01/tldi22-sulzmann-with-appendix.pdf">System
Fc paper</a> as reference, ignoring all the parts about
coercions.</p>
<p>1. In the Fc paper, the rule `AppT` has a judgement delta as
assumption, which does not exist. I assumed the `ty` judgement was
meant there by looking at the arguments. Is this correct?</p>
<p>2. In the `Abs` rule, the type of the variable is required to be
valid and of kind star by the judgement `ty`. In the `Let` rule,
this assumption is missing. I tried it like that, but was not able
to complete the proofs. Is such an assumption missing there or
should I be able to proof it without?</p>
<p>3. In the Fc paper, the types and kinds of datatype declarations
are added to the context with a separate judgement that interprets
the datatype declarations. In the <a moz-do-not-send="true"
href="https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/p53-yorgey.pdf?from=http%3A%2F%2Fresearch.microsoft.com%2Fen-us%2Fum%2Fpeople%2Fsimonpj%2Fpapers%2Fext-f%2Fpromotion.pdf">System
Fc pro paper</a> (from what I can tell) those types and kinds
are assumed to be already part of the initial context. At the
moment I prove progress against the empty context, so I guess I
would have to relax that to an initial context that only contains
types and kinds of type constants and nothing else. Is that
correct? What is here the "best practice" in terms of PL research?</p>
<p>Thank you all<br>
Jan<br>
</p>
</body>
</html>