Commit 4c7e479e authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Change project name in _CoqProject.

parent 14ee8d5f
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]
......
From tutorial_popl20 Require Export safety. From solutions Require Export safety.
(** * Parametricity *) (** * Parametricity *)
Section parametricity. Section parametricity.
......
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
......
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