Commit 20ba9d4c by Ralf Jung

### update exercises

parent 697ba6c8
 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,23 +22,27 @@ Section parametricity. ... @@ -20,23 +22,27 @@ 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, σ') → False. False. Proof. (* FILL IN YOUR PROOF *) Qed. Proof. (* FILL IN YOUR PROOF *) 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. Proof. (* FILL IN YOUR PROOF *) Qed. Proof. (* FILL IN YOUR PROOF *) 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, σ) (of_val w :: es, σ') → ∃ n : nat, w = #n. (of_val w :: es, σ') → ∃ n : nat, w = #n. Proof. (* FILL IN YOUR PROOF *) Qed. Proof. (* FILL IN YOUR PROOF *) 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 ... @@ -89,7 +89,7 @@ Section types. ... @@ -89,7 +89,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!