Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Fengmin Zhu
Tutorial POPL20
Commits
4ae9c1c5
Commit
4ae9c1c5
authored
Jan 20, 2020
by
Robbert Krebbers
Browse files
Work.
parent
b2842b79
Changes
3
Hide whitespace changes
Inline
Sidebyside
solutions/language.v
View file @
4ae9c1c5
...
...
@@ 431,7 +431,7 @@ Lemma wp_add_two_fancy `{!heapG Σ} (x : Z) :
auto
with
f_equal
lia
.
Qed
.
(** * Reasoning about "unsafe"
function
s *)
(** * Reasoning about "unsafe"
program
s *)
(** Since HeapLang is an untyped language, we can write down arbitrary
programs, i.e. programs that are not typeable by conventional type systems, and
prove logical specifications of them. We will show this on two small examples
...
...
solutions/polymorphism.v
View file @
4ae9c1c5
From
tutorial_popl20
Require
Export
language
.
(** * Polymorphism and existential types in HeapLang *)
(** In order to define a type system for HeapLang (in the file [typed.v]) we
(** In order to define a type system for HeapLang (in the file [typed.v])
,
we
need to extend HeapLang with constructs for polymorphic functions (i.e.
typelevel lambdas and application), and for existential types (i.e. pack and
unpack). Since HeapLang is an untyped language, it does natively have these
...
...
solutions/sem_type_formers.v
View file @
4ae9c1c5
From
tutorial_popl20
Require
Export
sem_types
.
(** * The definitions of the semantic type formers
(** * Semantic type formers *)
(** For all of the type formers in the syntactic type system, we now define
corresponding semantic type formers. For example, we define the product type
formers, which given two semantic types [A] and [B], gives the semantic type of
the product [A * B], i.e., values that are pairs where the first component
belongs to [A] and the second component to [B]. *)
These type formers correspond to those of syntactic types, e.g., a
product former that given two semantic types [A] and [B], gives
the semantic type of the product [A * B], i.e., values that are
pairs where the first component belongs to [A] and the second
component to [B]. *)
Section
types
.
Context
`
{!
heapG
Σ
}.
(** * Base types *)
(** Let us start with the simplest types of our language: unit and Boolean.
The value interpretations of these types are as follows: *)
Definition
sem_ty_unit
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
⌜
w
=
#()
⌝
)%
I
.
Definition
sem_ty_bool
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
∃
b
:
bool
,
⌜
w
=
#
b
⌝
)%
I
.
The corresponding semantic types are defined as follows: *)
Definition
sem_ty_unit
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
⌜
w
=
#()
⌝
)%
I
.
Definition
sem_ty_bool
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
∃
b
:
bool
,
⌜
w
=
#
b
⌝
)%
I
.
(** These interpretations are exactly what you would expect: the only value
of the unit type is the unit value [()], the values of the Boolean type are
the elements of the Coq type [bool] (i.e. [true] and [false]). *)
(** Exercise. now define the value interpretation of the integer type. *)
(* REMOVE *)
Definition
sem_ty_int
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
∃
n
:
Z
,
⌜
w
=
#
n
⌝
)%
I
.
(** ** Exercise (sem_ty_int, easy) *)
(** Define the semantic version of the type of integers. *)
(* REMOVE *)
Definition
sem_ty_int
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
∃
n
:
Z
,
⌜
w
=
#
n
⌝
)%
I
.
(** The value interpretation for product type is as one would expect: *)
(** * Products and sums *)
(** The semantic type former for products is as follows: *)
Definition
sem_ty_prod
(
A1
A2
:
sem_ty
Σ
)
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
∃
w1
w2
,
⌜
w
=
(
w1
,
w2
)%
V
⌝
∧
A1
w1
∧
A2
w2
)%
I
.
(** Values of the product type over [A1] and [A2] should be tuples [(w1, w2)],
where [w1] and [w2] should
be
in the
interpretation of
[A1] and [A2],
where [w1] and [w2] should
values
in the
semantic type
[A1] and [A2],
respectively. *)
(** ** Exercise (sem_ty_sum, moderate) *)
(** Define the semantic type former for sums. *)
(* REMOVE *)
Definition
sem_ty_sum
(
A1
A2
:
sem_ty
Σ
)
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
(
∃
w1
,
⌜
w
=
InjLV
w1
⌝
∧
A1
w1
)
∨
(
∃
w2
,
⌜
w
=
InjRV
w2
⌝
∧
A2
w2
))%
I
.
(
∃
w1
,
⌜
w
=
InjLV
w1
⌝
∧
A1
w1
)
∨
(
∃
w2
,
⌜
w
=
InjRV
w2
⌝
∧
A2
w2
))%
I
.
(** The value interpretation for function types is as follows: *)
(** * Functions *)
(** The semantic type former for functions is as follows: *)
Definition
sem_ty_arr
(
A1
A2
:
sem_ty
Σ
)
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
□
∀
v
,
A1
v

∗
WP
App
w
v
{{
A2
}})%
I
.
(** This definition is very close to the usual way of defining the
value interpretation of the function type [A1 → A2] in ordinary
logical relations: it expresses that arguments of semantic type
[A1] are mapped to results of semantic type [A2] . The only Iris
specific feature one has to take into account is the [□]
modality. Recall that the value interpretation should be a
persistent predicate; however, even if both [P] and [Q] are
persistent propositions, the magic wand [P ∗ Q] is not
necessarily persistent. Hence, we use the [□] modality to make
the magic wand persistent. *)
(** The value interpretation for type variables, universal types,
and existential types is: *)
(** This definition is very close to the usual way of defining the type
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 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 [□
modality to make the magic wand persistent.
*)
(** * Polymorphism and existentials *)
Definition
sem_ty_forall
(
C
:
sem_ty
Σ
→
sem_ty
Σ
)
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
□
∀
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 higherorder 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 type [C A] (defined using WP).
Similarly, given a higherorder 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.
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.
Remark: notice that for technical reasons (related to the value
restriction problem in MLlike languages) universally quantified
expressions are not evaluated until they are applied to a
specific type. *)
(**
The value interpretation of reference types is as follows:
*)
Given a higherorder 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 type [C A] (defined using WP).
Similarly, given a higherorder 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.
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.
Remark: notice that for technical reasons (related to the value
restriction problem in MLlike languages) universally quantified
expressions are not evaluated until they are applied to a
specific type. *)
(**
* References
*)
Definition
tyN
:
=
nroot
.@
"ty"
.
Definition
sem_ty_ref
(
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:
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 pointsto connective l ↦ v (from vanilla separation logic)
provides exclusive ownership of the location l with value
v. The pointsto connective is an ephemeral proposition, and
necessarily not a persistent proposition.
 The pointsto connective l ↦ v (from vanilla separation logic)
provides exclusive ownership of the location l with value
v. The pointsto 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. *)
 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. *)
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. *)
End
types
.
(** We introduce nicely looking notations for our semantic types. This allows
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment