Prezi

Present Remotely

Send the link below via email or IM

Copy

Present to your audience

Start remote presentation

  • Invited audience members will follow you as you navigate and present
  • People invited to a presentation do not need a Prezi account
  • This link expires 10 minutes after you close the presentation
  • A maximum of 30 users can follow your presentation
  • Learn more about this feature in the manual

Do you really want to delete this prezi?

Neither you, nor the coeditors you shared it with will be able to recover it again.

DeleteCancel

Make your likes visible on Facebook?

Connect your Facebook account to Prezi and let your likes appear on your timeline.
You can change this under Settings & Account at any time.

No, thanks

Linear logic

No description
by James Koppel on 15 July 2014

Comments (0)

Please log in to add your comment.

Report abuse

Transcript of Linear logic

foo.close();
foo.read();
int x = 1;
int y = 2;
return x;
int x = 1;
return plus(x, x);
int x = 1;
int y = 2;
foo(x);
bar(y);
when do traditional types not help?
stateful code
functional updates
effect interference
memory management
replaced
with

persistence
change
memory leak?
use after free?
what do these have in common?
control of aliasing
stateful code
effect interference
memory management
functional updates
linear types
linearity analysis
ownership types

regions
permissions
typestate
why can't traditional types help us?
our notion of truth
W,C,E
IPC/STLC
W,E
C,E
E
affine
strict
linear
ordered
Substructural Logics
towards practical typecheckers
Checker Framework
Java type annotations for
locks
units
thread locality
tainting
immutability
format strings
regexes
nullness
Further Reading
Basic
Frank Pfenning's lecture notes. http://www.cs.cmu.edu/~fp/courses/15816-s12/schedule.html
P. Wadler. "Linear Types Can Change the World"
J. Aldrich, J. Sunshine, D. Saini, Z. Sparks: "Typestate-Oriented Programming"
M. Fähndrich and K. R. M. Leino: "Declaring and Checking Non-null Types in an Object-Oriented Language"

Advanced
J. Boyland, J. Noble, and W. Retert. "Capabilities for sharing: A generalisation of uniqueness and read-only."
J. Foster, T. Terauchi, and A. Aiken. "Flow-sensitive Type Qualifiers"
R. Garcia, R. Wolff, É. Tanter, and J. Aldrich. "Featherweight Typestate"

this.nameUtils : @Nullable NameUtils
this.nameUtils : @Initialized @NonNull NameUtils
this : @UnderInitialization({}) NameUtils, nameDelimiter : @Uninitialized String
this : @UnderInitialization({nameDelimiter}) NameUtils, nameDelimiter : @Initialized String
@Initialized = @UnderInitialization({nameDelimiter})
lastName : @Initialized @Nullable String
lastName : @Initialized @NonNull String
attendeeList.nameUtils : @Nullable NameUtils
attendeeList.nameUtils : @NonNull NameUtils
See the full transcript