Commit 699b4805 authored by Amin Timany's avatar Amin Timany

Merge branch 'master' of gitlab.mpi-sws.org:iris/tutorial-popl20

parents 3ce3bb2d 5c30b5c6
......@@ -8,7 +8,7 @@ all: Makefile.coq
clean: Makefile.coq
+@make -f Makefile.coq clean
find solutions tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
rm -f Makefile.coq .lia.cache
.PHONY: clean
......
......@@ -45,7 +45,9 @@ former for the function type [A1 → A2] in traditional logical relations: it
expresses that arguments of semantic type [A1] are mapped to results of
semantic type [A2]. The definition makes two of two features of Iris:
- The weakest precondition [WP e {{ Φ }}].
- The weakest precondition [WP e {{ Φ }}]. We have already seen weakest
preconditions before (in the file [language.v]). We use them in the semantics
of functions to talk about the result of the expression [v w].
- The persistence modality [□]. Recall that semantic types are persistent Iris
predicates. However, even if both [P] and [Q] are persistent propositions,
the magic wand [P -∗ Q] is not necessarily persistent. Hence, we use the [□
......@@ -54,58 +56,53 @@ semantic type [A2]. The definition makes two of two features of Iris:
(** * Polymorphism and existentials *)
Definition sem_ty_forall `{!heapG Σ} (C : sem_ty Σ sem_ty Σ) : sem_ty Σ := SemTy (λ w,
A : sem_ty Σ, WP w #() {{ w, C A w }})%I.
A : sem_ty Σ, WP w <_> {{ w, C A w }})%I.
Definition sem_ty_exist {Σ} (C : sem_ty Σ sem_ty Σ) : sem_ty Σ := SemTy (λ w,
A : sem_ty Σ, C A w)%I.
(** The interpretations of these types are fairly straightforward.
Given a higher-order type former [C] that maps semantic types to
semantic types, we define the universal type [sem_ty_forall A]
using the universal quantification in Iris. That is, a value [w]
is considered a polymorphic value if for any semantic type [A],
when [w] is specialized to the type [A] (written as [w #()] as
(semantic) types never appear in terms in our untyped syntax)
the _resulting expression_ is an expression in the semantics of
(** The interpretations of these types are fairly straightforward. Given a
higher-order type former [C] that maps semantic types to semantic types, we
define the universal type [sem_ty_forall A] using the universal quantifier of
Iris. That is, a value [w] is considered a polymorphic value if for any semantic
type [A], when [w] is specialized to the type [A] (written as [w <_>] (see the
file [polymorphism.v]) as (semantic) types never appear in terms in our
untyped syntax) the _resulting expression_ is an expression in the semantics of
the type [C A] (defined using WP).
Similarly, given a higher-order type former [C] that maps
semantic types to semantic types, we define the existential type
[sem_ty_exist A] using the existential quantification in Iris.
Similarly, given a higher-order type former [C] that maps semantic types to
semantic types, we define the existential type [sem_ty_exist A] using the
existential quantifier of Iris.
Notice how the impredicative nature of Iris propositions and
predicates allows us to quantify over Iris predicates to define
an Iris predicate. This is crucial for giving semantics to
parametric polymorphism, i.e., universal and existential types.
Notice how the impredicative nature of Iris propositions and predicates allow
us to quantify over Iris predicates to define an Iris predicate. This is crucial
for giving semantics to parametric polymorphism, i.e., universal and existential
types.
Remark: notice that for technical reasons (related to the value
restriction problem in ML-like languages) universally quantified
expressions are not evaluated until they are applied to a
specific type. *)
Remark: notice that for technical reasons (related to the value restriction
problem in ML-like languages) universally quantified expressions are not
evaluated until they are applied to a specific type. *)
(** * References *)
Definition tyN := nroot .@ "ty".
Definition sem_ty_ref `{!heapG Σ} (A : sem_ty Σ) : sem_ty Σ := SemTy (λ w,
l : loc, w = #l inv (tyN .@ l) ( v, l v A v))%I.
(** Intuitively, values of the reference type [sem_ty_ref A] should
be locations [l] that hold a value [w] in the semantic type [A] at
all times. In order to express this intuition in a formal way, we
make use of two features of Iris:
- The points-to connective l ↦ v (from vanilla separation logic)
provides exclusive ownership of the location l with value
v. The points-to connective is an ephemeral proposition, and
necessarily not a persistent proposition.
- The invariant assertion [inv N P] expresses that a (typically
ephemeral) proposition [P] holds at all times -- i.e., [P] is
invariant. The invariant assertion is persistent.
(** Intuitively, values of the reference type [sem_ty_ref A] should be locations
[l] that hold a value [w] in the semantic type [A] at all times. In order to
express this intuition in a formal way, we make use of two features of Iris:
- The points-to connective [l ↦ v] (from vanilla separation logic) provides
exclusive ownership of the location [l] with value [v]. The points-to
connective is an ephemeral proposition, and necessarily not a persistent
proposition.
- The invariant assertion [inv N P] expresses that a (typically ephemeral)
proposition [P] holds at all times -- i.e., [P] is invariant. The invariant
assertion is persistent.
*)
(** Remark: Iris is also capable giving semantics to recursive
types. However, for the sake of simplicity we did not consider
recursive types for this tutorial. In particular, to give the
semantics of recursive types one needs to use Iris's guarded
fixpoints, which require some additional bookkeeping related to
contractiveness. *)
(** Remark: Iris is also capable giving semantics to recursive types. However,
for the sake of simplicity we did not consider recursive types for this
tutorial. In particular, to give the semantics of recursive types one needs to
use Iris's guarded fixpoints, which require some additional bookkeeping related
to contractiveness. *)
(** We introduce nicely looking notations for our semantic types. This allows
us to write lemmas, for example, the compatibility lemmas, in a readable way. *)
......
......@@ -45,7 +45,9 @@ former for the function type [A1 → A2] in traditional logical relations: it
expresses that arguments of semantic type [A1] are mapped to results of
semantic type [A2]. The definition makes two of two features of Iris:
- The weakest precondition [WP e {{ Φ }}].
- The weakest precondition [WP e {{ Φ }}]. We have already seen weakest
preconditions before (in the file [language.v]). We use them in the semantics
of functions to talk about the result of the expression [v w].
- The persistence modality [□]. Recall that semantic types are persistent Iris
predicates. However, even if both [P] and [Q] are persistent propositions,
the magic wand [P -∗ Q] is not necessarily persistent. Hence, we use the [□
......@@ -54,58 +56,53 @@ semantic type [A2]. The definition makes two of two features of Iris:
(** * Polymorphism and existentials *)
Definition sem_ty_forall `{!heapG Σ} (C : sem_ty Σ sem_ty Σ) : sem_ty Σ := SemTy (λ w,
A : sem_ty Σ, WP w #() {{ w, C A w }})%I.
A : sem_ty Σ, WP w <_> {{ w, C A w }})%I.
Definition sem_ty_exist {Σ} (C : sem_ty Σ sem_ty Σ) : sem_ty Σ := SemTy (λ w,
A : sem_ty Σ, C A w)%I.
(** The interpretations of these types are fairly straightforward.
Given a higher-order type former [C] that maps semantic types to
semantic types, we define the universal type [sem_ty_forall A]
using the universal quantification in Iris. That is, a value [w]
is considered a polymorphic value if for any semantic type [A],
when [w] is specialized to the type [A] (written as [w #()] as
(semantic) types never appear in terms in our untyped syntax)
the _resulting expression_ is an expression in the semantics of
(** The interpretations of these types are fairly straightforward. Given a
higher-order type former [C] that maps semantic types to semantic types, we
define the universal type [sem_ty_forall A] using the universal quantifier of
Iris. That is, a value [w] is considered a polymorphic value if for any semantic
type [A], when [w] is specialized to the type [A] (written as [w <_>] (see the
file [polymorphism.v]) as (semantic) types never appear in terms in our
untyped syntax) the _resulting expression_ is an expression in the semantics of
the type [C A] (defined using WP).
Similarly, given a higher-order type former [C] that maps
semantic types to semantic types, we define the existential type
[sem_ty_exist A] using the existential quantification in Iris.
Similarly, given a higher-order type former [C] that maps semantic types to
semantic types, we define the existential type [sem_ty_exist A] using the
existential quantifier of Iris.
Notice how the impredicative nature of Iris propositions and
predicates allows us to quantify over Iris predicates to define
an Iris predicate. This is crucial for giving semantics to
parametric polymorphism, i.e., universal and existential types.
Notice how the impredicative nature of Iris propositions and predicates allow
us to quantify over Iris predicates to define an Iris predicate. This is crucial
for giving semantics to parametric polymorphism, i.e., universal and existential
types.
Remark: notice that for technical reasons (related to the value
restriction problem in ML-like languages) universally quantified
expressions are not evaluated until they are applied to a
specific type. *)
Remark: notice that for technical reasons (related to the value restriction
problem in ML-like languages) universally quantified expressions are not
evaluated until they are applied to a specific type. *)
(** * References *)
Definition tyN := nroot .@ "ty".
Definition sem_ty_ref `{!heapG Σ} (A : sem_ty Σ) : sem_ty Σ := SemTy (λ w,
l : loc, w = #l inv (tyN .@ l) ( v, l v A v))%I.
(** Intuitively, values of the reference type [sem_ty_ref A] should
be locations [l] that hold a value [w] in the semantic type [A] at
all times. In order to express this intuition in a formal way, we
make use of two features of Iris:
- The points-to connective l ↦ v (from vanilla separation logic)
provides exclusive ownership of the location l with value
v. The points-to connective is an ephemeral proposition, and
necessarily not a persistent proposition.
- The invariant assertion [inv N P] expresses that a (typically
ephemeral) proposition [P] holds at all times -- i.e., [P] is
invariant. The invariant assertion is persistent.
(** Intuitively, values of the reference type [sem_ty_ref A] should be locations
[l] that hold a value [w] in the semantic type [A] at all times. In order to
express this intuition in a formal way, we make use of two features of Iris:
- The points-to connective [l ↦ v] (from vanilla separation logic) provides
exclusive ownership of the location [l] with value [v]. The points-to
connective is an ephemeral proposition, and necessarily not a persistent
proposition.
- The invariant assertion [inv N P] expresses that a (typically ephemeral)
proposition [P] holds at all times -- i.e., [P] is invariant. The invariant
assertion is persistent.
*)
(** Remark: Iris is also capable giving semantics to recursive
types. However, for the sake of simplicity we did not consider
recursive types for this tutorial. In particular, to give the
semantics of recursive types one needs to use Iris's guarded
fixpoints, which require some additional bookkeeping related to
contractiveness. *)
(** Remark: Iris is also capable giving semantics to recursive types. However,
for the sake of simplicity we did not consider recursive types for this
tutorial. In particular, to give the semantics of recursive types one needs to
use Iris's guarded fixpoints, which require some additional bookkeeping related
to contractiveness. *)
(** We introduce nicely looking notations for our semantic types. This allows
us to write lemmas, for example, the compatibility lemmas, in a readable way. *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment