<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>