-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathMsciProjectIdeasEmail
180 lines (157 loc) · 8.4 KB
/
MsciProjectIdeasEmail
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
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
formalise correspondence between GV (Wadler, 2012) and
(Gay and Vasconcelos, 2010)
- possibility for extending GV to handle subtyping
+ check the subtyping for session types by (Gay and Hole, 2005).
and
presenting a formal proof of the deadlock-free property
of GV (whether this is of research interest, is debatable).
- could also handle buffered communication in GV formalisation.
- what is the research contribution of this work
- a formally proved implementation of session types in
multi-threaded functional programming language (with
linear types) with
guarantees of deadlock-freedom via its translation from
a process calculus.
- it's not clear whether GV handles asynchronous communication?
- are the formal proofs of research interest?
- significance of the relationship to process calculus, CP
- could we marry the two systems to support recursion that
terminates a la Coq's FixPoint construct?
- support for type polymorphism/type abstraction(inference?)?
+ neither system has support for these (formally).
alias control without the use of linear types
- affine types? look this up...
object-oriented session types
+ formal semantics/ownership types for sending/receiving.
+ why is this so difficult to formulate, or hasn't this been
done already?
+ motivated by prevalent usage of OOP languages.
+ deadlock? correctness? strong normalisation?
- translation to process calculus in Wadler's paper?
Email body follows:
--------------------
Hi Simon,
I have read the papers you suggested along with:
Wadler, Philip. Propositions as Sessions, 2012.
I'll refer to them using the numbers below:
Propositions as Sessions [1]
"Linear Type Theory for Asynchronous Session Types" [2]
TR-2003-133.pdf [3].
From the works, and the sections on future work I see a
number of things we can work on:
We could formalise the implementation of a multi-threaded
functional language with session types in Coq. We could
marry GV, the language discussed in [1], and the language
in [2], to provide a formal proof of:
(1) deadlock-freedom,
(2) bounded-buffer assurances,
(3) type preservation (possibly the most straightforward).
This would also entail translation to the process
calculus discussed in [1]. It is not yet clear to me how
significant the development would be, and whether it is
amenable to the timeline of an MSci project; it's just
a seed of idea so far but I'd like to know your thoughts
on it? e.g. whether you think formalising these proofs
(albeit proof sketches in [1]) has research value?
Also, [1], [2] both mention the desire for
type polymorphism and inference, and these could be
separate directions to go on. Alternatively, we could look to
focus on just one language defined in the literature and extend
it with formal semantics for type inference/polymorphism/etc.
My work last year involved adding an annotation to an
actor-based language to support a variant of ownership
types over the channel-based communication mechanism
between the actors. The static analysis I developed
allowed unrestricted aliasing of "owned" types within
a single actor while still guaranteeing that only one
actor held all the aliases at any one time. I understand
your work on object-oriented session types looks to
control aliasing (currently with linear typing,
from "Modular Session Types for Distributed Object-Oriented
Programming"), and perhaps we could explore extending
or enhancing this feature of the object-oriented
setting, although at this time I am not sure how to
incorporate the use of interactive theorem proving.
If you have any other projects or ideas you think
I should consider, let me know.
Regards,
Craig
-----
Response:
Dear Craig,
Another paper that might be relevant is this one:
http://fpl.cs.depaul.edu/cpitcher/research/2013-an-extensible-approach-to-
session-polymorphism.pdf
It's about polymorphism in session types, and the system they describe
has been formalized in Coq.
Indeed I am interested in alias control. All the work I have done on
session types so far has used strict linearity, which is too restrictive
for practical programming. Exploring other forms of alias control would
be interesting. You could look at it in a functional setting or an
object-oriented setting (but in that case we would probably want
something simpler than my "modular session types" paper, which has a
very complicated type system). There is some work by Robert DeLine and
Manuel Fahndrich based on the Vault and Fugue systems, with a particular
form of alias control that many people find attractive. One of their
papers is called "Practical linear types for imperative programming". I
would like to understand their system better and maybe formalising it
would be a way of doing that.
I think an important aspect of working with Coq, in the area of
semantics and type systems, is to not just formalize a particular system
but to set things up in a way that makes it easy to produce formalized
proofs about a range of related languages. In that way the formalization
can become a tool for checking the properties of new type systems.
Simon
------
My Response:
Hi Simon,
Apologies for the late reply. I require to send a project outline to Gethin
by Friday next week and I'm looking to confirm a project with you as
supervisor. Based on our previous discussions I have written a short outline
below. Let me know what you think/have any suggestions for amendments.
Project Title: Formalisation of Lambda Calculus Session-based Type Systems
Project Outline:
The aim of this project is to develop a framework for formalising lambda
calculus type systems involving session types using interactive theorem
proving (in particular, the system Coq). The motivation for the framework is
that it will enable a whole class of related languages and type systems to be
formalised with little extra proof effort. Inspired by previous work on a
mechanised framework of pi calculus type systems [1], we shift to the lambda
calculus to provide a basis on which session types for mainstream programming
languages can be studied whilst taking advantage of previous proof effort and
specialising only for those parts unique to the particular system.
From the generic framework, a number of directions can be explored including
session polymorphism, session subtyping, and permitting different forms of
aliasing within the type system. The majority of previous session type systems
for mainstream programming languages has focussed exclusively on linear type
systems. One disadvantage of a linear type system is the need to re-bind
objects after each operation [2]. Principally, we intend to instantiate the
framework with a type system that provides the benefits of aliasing with the
guarantees of linearity, termed ``adoption and focus''. The ``adoption and
focus'' type system is non-trivial requiring special language features, e.g.
to manage capabilities which can be thought as a form of object liveness
mechanism, so the framework design must support such flexibility by, e.g
allowing the typing judgements to be extended such that the capabilities can
be included in soundness results. The instantiation will demonstrate that the
framework supports a wide range of languages and type systems providing
researchers the ability to harness the power of formal verification in the
design, implementation and documentation of session-based type systems.
[1] Simon J. Gay. 2001. A Framework for the Formalisation of Pi Calculus Type
Systems in Isabelle/HOL. In Proceedings of the 14th International Conference
on Theorem Proving in Higher Order Logics (TPHOLs '01), Richard J. Boulton and
Paul B. Jackson (Eds.). Springer-Verlag, London, UK, UK, 217-232.
[2] Simon j. Gay and Vasco t. Vasconcelos. 2010. Linear type theory for
asynchronous session types. J. Funct. Program. 20, 1 (January 2010), 19-50.
DOI=10.1017/S0956796809990268 http://dx.doi.org/10.1017/S0956796809990268
----
Or a formalisation based on the pi-calculus (which would provide deadlock
freedom guarantees).
A project aimed at developing a generic framework for reasoning about type
systems (similar to your paper in 2001). Instantiating the framework for
the type system found in the adoption and focus paper.
Perhaps looking into creating some translation layer between a process
calculus and a lambda caculus (metalanguage)?
From there we could formalise a number of extensions if time permits, e.g.
subtyping and a correspondence between GV process calculus.
Adopt and focus/GV/ some translation of a functional language to GV
(process calculus)