Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Try using stamped syntax in syntactic typing judgment #21

Closed
4 tasks done
Blaisorblade opened this issue Feb 21, 2019 · 0 comments
Closed
4 tasks done

Try using stamped syntax in syntactic typing judgment #21

Blaisorblade opened this issue Feb 21, 2019 · 0 comments

Comments

@Blaisorblade
Copy link
Owner

Blaisorblade commented Feb 21, 2019 •
edited

Ideally, this should confirm that we can focus on stamped syntax.

Steps:

  • Make typing refer to stamped type members.
  • Prove that a typing judgment only refers to stamped expressions/subjects.
  • Prove that a typing judgment only refers to stamped types. That'll probably require extra side conditions around subtyping (EDIT: but not occurrences of TSel).
  • Check the above lemma can be used for the fundamental lemma. In fact, the fundamental lemma seems to not require explicit proofs that the syntax is stamped (or not).

I moved other items to #43; closing.
@Blaisorblade Blaisorblade mentioned this issue Feb 21, 2019
Closed
3 tasks
Blaisorblade added a commit that referenced this issue Feb 22, 2019
@Blaisorblade
Make typing depend on stampTable via typeclass (!!!)
80c89bb 
Contentious implementation:
Thread the stampTable everywhere implicitly with a typeclass.

Otherwise, we'd have to redesign the notations and thread extra boilerplate.

Part of #21.
Blaisorblade added a commit that referenced this issue Feb 28, 2019
@Blaisorblade
Dot: add definition of stampedness (#21)
6277fe8
Blaisorblade added a commit that referenced this issue Feb 28, 2019
@Blaisorblade
Prove that typed expressions are stamped (#21)
750aa33 
This found one scoping bug in typing (and, in fact, a few bugs in stampedness;
fixes already included in the previous commit).
Blaisorblade added a commit that referenced this issue Feb 28, 2019
@Blaisorblade
Prove that typing implies well-stamping (#21)
51c59eb 
We take well-stamping of context as hypothesis (following PFPL 2nd ed.'s
regularity, Lemma 16.1 for System F). We must also check well-stamping of all
types we add to the typing context.
@Blaisorblade Blaisorblade added this to the Crucial milestone Mar 1, 2019
@Blaisorblade Blaisorblade removed this from the Crucial milestone Apr 22, 2019
@Blaisorblade Blaisorblade mentioned this issue May 3, 2019
Closed
3 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@Blaisorblade