Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
T
Tutorial POPL20
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Arthur Azevedo de Amorim
Tutorial POPL20
Commits
810f6a9f
Commit
810f6a9f
authored
Jan 20, 2020
by
Ralf Jung
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
also fix imports
parent
20ba9d4c
Changes
15
Hide whitespace changes
Inline
Side-by-side
Showing
15 changed files
with
18 additions
and
16 deletions
+18
-16
exercises/compatibility.v
exercises/compatibility.v
+1
-1
exercises/demo.v
exercises/demo.v
+1
-1
exercises/fundamental.v
exercises/fundamental.v
+1
-1
exercises/interp.v
exercises/interp.v
+1
-1
exercises/parametricity.v
exercises/parametricity.v
+1
-1
exercises/polymorphism.v
exercises/polymorphism.v
+1
-1
exercises/safety.v
exercises/safety.v
+1
-1
exercises/sem_operators.v
exercises/sem_operators.v
+1
-1
exercises/sem_type_formers.v
exercises/sem_type_formers.v
+1
-1
exercises/sem_typed.v
exercises/sem_typed.v
+1
-1
exercises/sem_types.v
exercises/sem_types.v
+1
-1
exercises/typed.v
exercises/typed.v
+1
-1
exercises/types.v
exercises/types.v
+1
-1
exercises/unsafe.v
exercises/unsafe.v
+2
-2
mk-exercises.sh
mk-exercises.sh
+3
-1
No files found.
exercises/compatibility.v
View file @
810f6a9f
From
solution
s
Require
Export
sem_typed
sem_operators
.
From
exercise
s
Require
Export
sem_typed
sem_operators
.
(** * Compatibility lemmas *)
(** We prove that the logical relations, i.e., the semantic typing judgment,
...
...
exercises/demo.v
View file @
810f6a9f
From
solution
s
Require
Import
language
.
From
exercise
s
Require
Import
language
.
From
iris
.
base_logic
.
lib
Require
Import
invariants
.
From
iris
.
heap_lang
Require
Import
adequacy
.
...
...
exercises/fundamental.v
View file @
810f6a9f
From
solution
s
Require
Export
typed
compatibility
interp
.
From
exercise
s
Require
Export
typed
compatibility
interp
.
(** * The fundamental theorem of logical relations *)
(** The fundamental theorem of logical relations says that any syntactically
...
...
exercises/interp.v
View file @
810f6a9f
From
solution
s
Require
Export
sem_typed
sem_type_formers
types
.
From
exercise
s
Require
Export
sem_typed
sem_type_formers
types
.
(** * Interpretation of syntactic types *)
(** We use semantic type formers to define the interpretation [⟦ τ ⟧ : sem_ty]
...
...
exercises/parametricity.v
View file @
810f6a9f
From
solution
s
Require
Export
safety
.
From
exercise
s
Require
Export
safety
.
(** * Parametricity *)
Section
parametricity
.
...
...
exercises/polymorphism.v
View file @
810f6a9f
From
solution
s
Require
Export
language
.
From
exercise
s
Require
Export
language
.
(** * Polymorphism and existential types in HeapLang *)
(** In order to define a type system for HeapLang (in the file [typed.v]), we
...
...
exercises/safety.v
View file @
810f6a9f
From
iris
.
heap_lang
Require
Export
adequacy
.
From
solution
s
Require
Export
fundamental
.
From
exercise
s
Require
Export
fundamental
.
(** * Semantic and syntactic type safety *)
(** We prove *semantic type safety*, which says that any _closed_ expression
...
...
exercises/sem_operators.v
View file @
810f6a9f
From
solution
s
Require
Export
sem_typed
.
From
exercise
s
Require
Export
sem_typed
.
(** Semantic operator typing *)
Class
SemTyUnboxed
`
{!
heapG
Σ
}
(
A
:
sem_ty
Σ
)
:
=
...
...
exercises/sem_type_formers.v
View file @
810f6a9f
From
solution
s
Require
Export
sem_types
.
From
exercise
s
Require
Export
sem_types
.
(** * Semantic type formers *)
(** For all of the type formers in the syntactic type system, we now define
...
...
exercises/sem_typed.v
View file @
810f6a9f
From
solution
s
Require
Export
sem_type_formers
.
From
exercise
s
Require
Export
sem_type_formers
.
(** * The semantic typing judgment *)
...
...
exercises/sem_types.v
View file @
810f6a9f
From
solution
s
Require
Export
polymorphism
.
From
exercise
s
Require
Export
polymorphism
.
From
iris
.
heap_lang
Require
Export
proofmode
.
From
iris
.
base_logic
.
lib
Require
Export
invariants
.
...
...
exercises/typed.v
View file @
810f6a9f
From
solution
s
Require
Export
types
polymorphism
.
From
exercise
s
Require
Export
types
polymorphism
.
(** * Syntactic typing for HeapLang *)
(** In this file, we define a syntactic type system for HeapLang. We do this
...
...
exercises/types.v
View file @
810f6a9f
From
solution
s
Require
Export
language
.
From
exercise
s
Require
Export
language
.
(** * Syntactic types for HeapLang *)
(** The inductive type [ty] defines the syntactic types for HeapLang. We make
...
...
exercises/unsafe.v
View file @
810f6a9f
From
solution
s
Require
Export
sem_typed
.
From
solution
s
Require
Import
symbol_ghost
two_state_ghost
.
From
exercise
s
Require
Export
sem_typed
.
From
exercise
s
Require
Import
symbol_ghost
two_state_ghost
.
Section
unsafe
.
Context
`
{!
heapG
Σ
}.
...
...
mk-exercises.sh
View file @
810f6a9f
...
...
@@ -7,6 +7,7 @@ REMOVEPRF_RE='s/\(\*\s*REMOVE\s*\*\)\s*Proof.\s*.*?\s*Qed\.\R/Proof. (* FILL IN
REMOVE_RE
=
's/\(\*\s*REMOVE\s*\*\)\s*(.*?)\s*:=.*?\.\R/\1. (* FILL IN HERE *) Admitted.\n/gms'
STRONGHIDE_RE
=
's/\(\*\s*STRONGHIDE\s*\*\)\s*(.*?)\(\*\s*ENDSTRONGHIDE\s*\*\)\R?//gms'
HIDE_RE
=
's/\(\*\s*HIDE\s*\*\)\s*(.*?)\(\*\s*ENDHIDE\s*\*\)/Definition hole := remove_this_line.\n(* ANSWER THE QUESTION AND REMOVE THE LINE ABOVE *)/gms'
IMPORT_RE
=
's/^From solutions/From exercises/gms'
# run replacement on all source files
mkdir
-p
exercises
...
...
@@ -16,5 +17,6 @@ for FILE in solutions/*.v; do
|
$REPLACE
"
$REMOVEPRF_RE
"
\
|
$REPLACE
"
$REMOVE_RE
"
\
|
$REPLACE
"
$STRONGHIDE_RE
"
\
|
$REPLACE
"
$HIDE_RE
"
>
"
$DST
"
|
$REPLACE
"
$HIDE_RE
"
\
|
$REPLACE
"
$IMPORT_RE
"
>
"
$DST
"
done
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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