ConcurrentProgramming)in) Linear)Type)Theory)
[Pages:41]Concurrent
Programming
in
Linear
Type
Theory
Frank
Pfenning
Carnegie
Mellon
University
Joint
work
with
Lu?s
Caires,
Bernardo
Toninho,
Jorge
Per?z,
Dennis
Griffith,
Elsa
Gunter,
et
al.
1/9/2014
ABCD
Project
MeeQng
1
1/9/2014
ABCD
Project
MeeQng
2
Outline
? A
new
foundaQon
for
session
types
? SILL
by
example
? Prime
sieve
? Bit
strings
? Language
highlights
? Types
and
programs
? ImplementaQon
? Ongoing
research
1/9/2014
ABCD
Project
MeeQng
3
Session
Types
? Prescribe
communicaQon
behavior
between
message--passing
concurrent
processes
? May
be
synchronous
or
asynchronous
? Linear
channels
with
two
endpoints
? Shared
channels
with
mulQple
endpoints
? Messages
exchanged
can
be
? data
values
(including
process
expressions)
? channels
(as
in
the
--calculus)
? labels
(to
indicate
choice)
1/9/2014
ABCD
Project
MeeQng
4
Curry--Howard
Isomorphisms
? Logical
origins
of
computaQonal
phenomena
? IntuiQonisQc
logic
funcQonal
programming
? S4
modal
logic
quote/eval
staging
? S5
modal
logic
distributed
programming
? Temporal
logic
parQal
evaluaQon
? Linear
logic
session--typed
concurrency
? More
than
an
analogy!
1/9/2014
ABCD
Project
MeeQng
5
Linear
Logic:
A
New
FoundaQon
? Linear
proposiQons
session
types
? Sequent
proofs
process
expressions
? Cut
process
composiQon
? IdenQty
message
forwarding
? Proof
reducQon
communicaQon
? Linear
type
theory
generalizes
linear
logic
? Logic:
proposiQons
do
not
menQon
proofs
? Type
theory:
proofs
are
internalized
as
terms
1/9/2014
ABCD
Project
MeeQng
6
Benefits
of
Curry--Howard
Design
? Integrated
development
of
programming
constructs
and
reasoning
principles
? Correct
programs
via
simple
reasoning
principles
? Even
if
they
are
not
formalized
in
the
language!
? Elegant
and
expressive
language
primiQves
? Orthogonality
and
compaQbility
of
constructs
? Programming
language
theory
as
proof
theory
1/9/2014
ABCD
Project
MeeQng
7
Some
Choices
for
SILL
? SILL
=
Sessions
in
IntuiQonisQc
Linear
Logic
? ConservaQvely
extend
funcQonal
language
? Process
expressions
form
a
(contextual)
monad
? CommunicaQon
may
be
observable
? Manifest
noQon
of
process
? Offer
vs.
use
of
a
service
? Process
channel
along
which
service
is
offered
? Later:
CILL,
sessions
in
a
C--like
language
1/9/2014
ABCD
Project
MeeQng
8
................
................
In order to avoid copyright disputes, this page is only a partial summary.
To fulfill the demand for quickly locating and searching documents.
It is intelligent file search solution for home and business.
Related download
Related searches
- coefficient in linear regression
- how find r in linear correlation coefficient
- correlation coefficient in a linear equation
- linear correlation in statistics examples
- linear correlation in statistics
- interpret coefficients in linear regression
- correlation coefficient in linear regression
- linear systems in 3 variables calculator
- how many square feet in linear foot
- linear inequalities in one variable
- linear inequalities in one unknown
- linear inequalities in two variables