This file indicates how some standard intuitionistic connectives
can be defined in terms of their linear counterparts, using the
type constructor TyBang.
Require Import Types.
Require Import TypeEquality.
Require Import Coercions.
Require Import Programs.
Require Import Multiplicity.
Require Import Environments.
Require Import Subtyping.
Require Import Typing.
Require Import PreliminaryLemmas.
Require Import Resources.
Require Import ResourcesContinued.
-------------------------------------------------------------------------
The capability-calculus arrow. This is the type of a DUPLICABLE function
that accepts a LINEAR argument. This corresponds to the functions found in
our ICFP 2008 paper.
Incidentally, this seems to be the known call-by-value translation of
intuitionistic logic into linear logic. See Benton and Wadler, LICS 1996.
Definition ccArrow T1 T2 :=
TyBang (
TyArrow T1 T2).
Abstraction. There is not much to be said about application; in an encoding
of the ICFP 2008 system into the present system, variables of duplicable
type would be re-bound via TLetBang as soon as they are introduced, so
they would appear in the non-linear part of the context. Thus, an arrow
becomes a standard arrow again, and application is just application.
Definition ccAbs t :=
VBang (
VAbs t).
Derived typing rules.
Lemma jv_ccAbs:
forall R M E t T1 T2,
jt (
neutral R) (
neutral M;;
MOne) (
E;;
T1)
t T2 ->
wf T1 ->
jv R M E (
ccAbs t) (
ccArrow T1 T2).
Proof.
intros. constructor; eauto.
Qed.
Derived subtyping rules.
Definition co_ccArrow c1 c2 :=
CoBang (
CoArrow c1 c2).
Lemma jco_ccArrow:
forall C c1 c2 T1 T2 U1 U2,
jco C c1 (
U1 -->
T1) ->
jco C c2 (
T2 -->
U2) ->
jco C (
co_ccArrow c1 c2) (
ccArrow T1 T2 -->
ccArrow U1 U2).
Proof.
intros. constructor; eauto.
Qed.