Commit 697ba6c8 authored by Ralf Jung's avatar Ralf Jung
Browse files
parents a47f9e2d 4c7e479e
-Q solutions tutorial_popl20 -Q solutions solutions
# non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9. # non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
-arg -w -arg -redundant-canonical-projection -arg -w -arg -redundant-canonical-projection
# change_no_check does not exist yet in 8.9. # change_no_check does not exist yet in 8.9.
......
From tutorial_popl20 Require Export sem_typed sem_operators. From solutions Require Export sem_typed sem_operators.
(** * Compatibility lemmas *) (** * Compatibility lemmas *)
(** We prove that the logical relations, i.e., the semantic typing judgment, (** We prove that the logical relations, i.e., the semantic typing judgment,
......
From tutorial_popl20 Require Import language. From solutions Require Import language.
From iris.base_logic.lib Require Import invariants. From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import adequacy. From iris.heap_lang Require Import adequacy.
......
From tutorial_popl20 Require Export typed compatibility interp. From solutions Require Export typed compatibility interp.
(** * The fundamental theorem of logical relations *) (** * The fundamental theorem of logical relations *)
(** The fundamental theorem of logical relations says that any syntactically (** The fundamental theorem of logical relations says that any syntactically
......
From tutorial_popl20 Require Export sem_typed sem_type_formers types. From solutions Require Export sem_typed sem_type_formers types.
(** * Interpretation of syntactic types *) (** * Interpretation of syntactic types *)
(** We use semantic type formers to define the interpretation [⟦ τ ⟧ : sem_ty] (** We use semantic type formers to define the interpretation [⟦ τ ⟧ : sem_ty]
of syntactic types [τ : ty]. The interpretation is defined recursively on the of syntactic types [τ : ty]. The interpretation is defined recursively on the
structure of syntactic types. *) structure of syntactic types. To account for type variables (that appear freely
in [τ]), we need to keep track of their corresponding semantic types. We
represent these semantic types as a list, since de use De Bruijn indices for
type variables. *)
Reserved Notation "⟦ τ ⟧". Reserved Notation "⟦ τ ⟧".
Fixpoint interp `{!heapG Σ} (τ : ty) (ρ : list (sem_ty Σ)) : sem_ty Σ := Fixpoint interp `{!heapG Σ} (τ : ty) (ρ : list (sem_ty Σ)) : sem_ty Σ :=
match τ return _ with match τ return _ with
...@@ -20,16 +22,10 @@ Fixpoint interp `{!heapG Σ} (τ : ty) (ρ : list (sem_ty Σ)) : sem_ty Σ := ...@@ -20,16 +22,10 @@ Fixpoint interp `{!heapG Σ} (τ : ty) (ρ : list (sem_ty Σ)) : sem_ty Σ :=
| TRef τ => ref ( τ ρ) | TRef τ => ref ( τ ρ)
end%sem_ty end%sem_ty
where "⟦ τ ⟧" := (interp τ). where "⟦ τ ⟧" := (interp τ).
Instance: Params (@interp) 2 := {}. Instance: Params (@interp) 2 := {}.
(** Given a syntactic typing context [Γ : gmap string ty] (a mapping from (** We now lift the interpretation of types to typing contexts. This is done in
variables [string] to syntactic types [ty]) together with a mapping a pointwise fashion using the [<$> : (A → B) → gmap K A → gmap K B] operator. *)
[ρ : list (sem_ty Σ)] from type variables (that appear freely in [Γ]) to
their corresponding semantic types (represented as a list, since de use De
Bruijn indices for type variables), we define a semantic typing context
[interp_env Γ ρ : gmap string (sem_ty Σ)], i.e., a mapping from variables
(strings) to semantic types. *)
Definition interp_env `{!heapG Σ} (Γ : gmap string ty) Definition interp_env `{!heapG Σ} (Γ : gmap string ty)
(ρ : list (sem_ty Σ)) : gmap string (sem_ty Σ) := flip interp ρ <$> Γ. (ρ : list (sem_ty Σ)) : gmap string (sem_ty Σ) := flip interp ρ <$> Γ.
Instance: Params (@interp_env) 3 := {}. Instance: Params (@interp_env) 3 := {}.
......
From tutorial_popl20 Require Export safety. From solutions Require Export safety.
(** * Parametricity *)
Section parametricity. Section parametricity.
Context `{!heapG Σ}. Context `{!heapG Σ}.
(** * The polymorphic identity function *)
Lemma identity_param `{!heapPreG Σ} e (v : val) σ w es σ' : Lemma identity_param `{!heapPreG Σ} e (v : val) σ w es σ' :
( `{!heapG Σ}, ( e : A, A A)%I) ( `{!heapG Σ}, ( e : A, A A)%I)
rtc erased_step ([e <_> v]%E, σ) (of_val w :: es, σ') w = v. rtc erased_step ([e <_> v]%E, σ) (of_val w :: es, σ') w = v.
...@@ -20,6 +22,7 @@ Section parametricity. ...@@ -20,6 +22,7 @@ Section parametricity.
wp_apply (wp_wand with "Hu"). iIntros (w') "Hw'". by iApply "Hw'". wp_apply (wp_wand with "Hu"). iIntros (w') "Hw'". by iApply "Hw'".
Qed. Qed.
(** * Exercise (empty_type_param, easy) *)
Lemma empty_type_param `{!heapPreG Σ} e (v : val) σ w es σ' : Lemma empty_type_param `{!heapPreG Σ} e (v : val) σ w es σ' :
( `{!heapG Σ}, ( e : A, A)%I) ( `{!heapG Σ}, ( e : A, A)%I)
rtc erased_step ([e <_>]%E, σ) (of_val w :: es, σ') rtc erased_step ([e <_>]%E, σ) (of_val w :: es, σ')
...@@ -38,6 +41,7 @@ Section parametricity. ...@@ -38,6 +41,7 @@ Section parametricity.
iApply ("Hu" $! T). iApply ("Hu" $! T).
Qed. Qed.
(** * Exercise (boolean_param, moderate) *)
Lemma boolean_param `{!heapPreG Σ} e (v1 v2 : val) σ w es σ' : Lemma boolean_param `{!heapPreG Σ} e (v1 v2 : val) σ w es σ' :
( `{!heapG Σ}, ( e : A, A A A)%I) ( `{!heapG Σ}, ( e : A, A A A)%I)
rtc erased_step ([e <_> v1 v2]%E, σ) (of_val w :: es, σ') w = v1 w = v2. rtc erased_step ([e <_> v1 v2]%E, σ) (of_val w :: es, σ') w = v1 w = v2.
...@@ -59,6 +63,7 @@ Section parametricity. ...@@ -59,6 +63,7 @@ Section parametricity.
iApply ("Hw''" $! v2). by iRight. iApply ("Hw''" $! v2). by iRight.
Qed. Qed.
(** * Exercise (nat_param, hard) *)
Lemma nat_param `{!heapPreG Σ} e σ w es σ' : Lemma nat_param `{!heapPreG Σ} e σ w es σ' :
( `{!heapG Σ}, ( e : A, (A A) A A)%I) ( `{!heapG Σ}, ( e : A, (A A) A A)%I)
rtc erased_step ([e <_> (λ: "n", "n" + #1)%V #0]%E, σ) rtc erased_step ([e <_> (λ: "n", "n" + #1)%V #0]%E, σ)
...@@ -85,6 +90,7 @@ Section parametricity. ...@@ -85,6 +90,7 @@ Section parametricity.
by iExists 0%nat. by iExists 0%nat.
Qed. Qed.
(** * Exercise (strong_nat_param, hard) *)
Lemma strong_nat_param `{!heapPreG Σ} e σ w es σ' (vf vz : val) φ : Lemma strong_nat_param `{!heapPreG Σ} e σ w es σ' (vf vz : val) φ :
( `{!heapG Σ}, Φ : sem_ty Σ, ( `{!heapG Σ}, Φ : sem_ty Σ,
( e : A, (A A) A A)%I ( e : A, (A A) A A)%I
......
From tutorial_popl20 Require Export language. From solutions Require Export language.
(** * Polymorphism and existential types in HeapLang *) (** * 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
......
From iris.heap_lang Require Export adequacy. From iris.heap_lang Require Export adequacy.
From tutorial_popl20 Require Export fundamental. From solutions Require Export fundamental.
(** * Semantic and syntactic type safety *) (** * Semantic and syntactic type safety *)
(** We prove *semantic type safety*, which says that any _closed_ expression (** We prove *semantic type safety*, which says that any _closed_ expression
......
From tutorial_popl20 Require Export sem_typed. From solutions Require Export sem_typed.
(** Semantic operator typing *) (** Semantic operator typing *)
Class SemTyUnboxed `{!heapG Σ} (A : sem_ty Σ) := Class SemTyUnboxed `{!heapG Σ} (A : sem_ty Σ) :=
......
From tutorial_popl20 Require Export sem_types. From solutions Require Export sem_types.
(** * Semantic type formers *) (** * Semantic type formers *)
(** For all of the type formers in the syntactic type system, we now define (** For all of the type formers in the syntactic type system, we now define
...@@ -92,7 +92,7 @@ Section types. ...@@ -92,7 +92,7 @@ Section types.
Definition sem_ty_ref (A : sem_ty Σ) : sem_ty Σ := SemTy (λ w, Definition sem_ty_ref (A : sem_ty Σ) : sem_ty Σ := SemTy (λ w,
l : loc, w = #l inv (tyN .@ l) ( v, l v A v))%I. l : loc, w = #l inv (tyN .@ l) ( v, l v A v))%I.
(** Intuitively, values of the reference type [sem_ty_ref A] should (** 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 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 all times. In order to express this intuition in a formal way, we
make use of two features of Iris: make use of two features of Iris:
......
From tutorial_popl20 Require Export sem_type_formers. From solutions Require Export sem_type_formers.
(** * The semantic typing judgment *) (** * The semantic typing judgment *)
......
From tutorial_popl20 Require Export polymorphism. From solutions Require Export polymorphism.
From iris.heap_lang Require Export proofmode. From iris.heap_lang Require Export proofmode.
From iris.base_logic.lib Require Export invariants. From iris.base_logic.lib Require Export invariants.
......
From tutorial_popl20 Require Export types polymorphism. From solutions Require Export types polymorphism.
(** * Syntactic typing for HeapLang *) (** * Syntactic typing for HeapLang *)
(** In this file, we define a syntactic type system for HeapLang. We do this (** In this file, we define a syntactic type system for HeapLang. We do this
......
From tutorial_popl20 Require Export language. From solutions Require Export language.
(** * Syntactic types for HeapLang *) (** * Syntactic types for HeapLang *)
(** The inductive type [ty] defines the syntactic types for HeapLang. We make (** The inductive type [ty] defines the syntactic types for HeapLang. We make
......
From tutorial_popl20 Require Export sem_typed. From solutions Require Export sem_typed.
From tutorial_popl20 Require Import symbol_ghost two_state_ghost. From solutions Require Import symbol_ghost two_state_ghost.
Section unsafe. Section unsafe.
Context `{!heapG Σ}. Context `{!heapG Σ}.
......
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