-
Notifications
You must be signed in to change notification settings - Fork 0
/
SimonPaperQs
52 lines (42 loc) · 2.12 KB
/
SimonPaperQs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
Hi Simon,
I have a draft of the paper (attached) to give you some context for the
following questions I have:
* I have been thinking about including the typing judgements for CP and GV,
and the reduction rules for CP but using the *locally nameless cofinite
quantification* form to obtain figures closer to the mechanised
proofs. What do you think? Otherwise (and with the second bullet in mind)
I'm not clear what I can really show to the reader and say, ``Look! This
is what I've done!''. I'm reluctant to put too much Coq code in the paper
since it usually winds up unreadable even to people well-versed in the
system.
* I'm not sure to what extent I should be regurgitating the work of Wadler
in my paper. Do I include relevant figures e.g. GV/CP types and terms and
also the CPS translation as relevant background? As it stands my draft is
already hovering around 14 pages and I've not finalised the main
contribution section (Section 3, Formalisation).
* What can I assume of the reader's knowledge? Should I have a section
explaining aspects of Coq? Its features for theorem proving, underlying
type theory, etc? I have looked at one other MSci project which used
Isabelle and there were some simple examples of how the prover worked (a
student of John's two years ago, no less)
Regards,
Craig
------------
Hi Simon,
I have attached another draft of the paper. I don't think I have any specific
questions to ask. I'm a little concerned my terminology is confusing; I use
"well-typed" and "typed in environment X" when referring to CP processes but I
can't think of any other when to say it, "communicates using environment X" is
a bit unwieldy.
Regarding the talk, should I be going into a similar depth as in the paper? Or
should I curtail the amount of Coq code I show. I think a slide full of typing
rules tends to strain the attention of the audience.
Regards,
Craig
------------
Hi Simon,
Since I sent the last draft I've only made minor changes/typo fixes. Do you
any other comments/suggestions to make on the draft I sent? Otherwise, I think
I will just leave it as is.
Regards,
Craig