Lecture 03 - harmony
Lecture 04 - cut reduction as computation
Lecture 05 - choice and replication
Use for computing:
- I Got Plenty o' Nuttin' by Conor McBride
- Syntax and Semantics of Quantitative Type Theory by Robert Atkey
Linear Logic changes structural rules so that they do not allow Weakening Rule or Contraction Rule. This means that resources are conserved (we cannot duplicate them when we want). This maintains some sort of state.
Structural rules define how variables can be substituted, reordered, and ignored in appropriate ways.
Hypotheses may be extended with additional members
Two equal (or unifiable) members on the same side of a sequent may be replaced by a single member.
Hypotheses contains two proofs of of A that is x:A y:A which we can replace with one proof z:A .
Also known as:
variables in the context can be reordered. (for dependent types B cannot depend on a.)
This has a different status in sequent calculus since it is a primative built into the mechinism.
Information about type theories/logics which do not have some of these rules:
Girard's linear logic does not allow the copying and destruction of terms so they must be used once. However they are still transferable. (transferring a resource from one owner to another can be done even when the resource cannot be copied.)
|ordered||once in order|
|we change from meaning of sequent from:||assumptionsproof|
Quantitative Type Theory
QTT = Linear types + Dependent types
Represents interactions between independent processes as communication (message-passing), rather than as modification of shared variables.
Describes concurrent communication language in which we can describe communicating processes which interact.
Each channel can operate in parallel and both the channels (different endpoints) and the state of the channels can change during the computation.
In π calculus we have:
- channels have a state (what event are they expecting)
we pass around names of channels. Names of channels can be passed along other channels.
channels names may be used only once but new instances of names (that is, reuse existing name) may be created for changes in state of the channel.