Commit 8602ad8c authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

README tweaking.

parent 4ae9c1c5
......@@ -58,10 +58,10 @@ Semantic typing:
- [sem_operators.v](solutions/sem_operators.v): The judgment for semantic
operator typing and proofs of the corresponding semantic rules.
- [compatibility.v](solutions/compatibility.v): The semantic typing rules, i.e.,
the compatibility lemmas.
the *compatibility lemmas*.
- [interp.v](solutions/interp.v): The interpretation of syntactic types in terms
of semantic types.
- [fundamental.v](solutions/fundamental.v): The *fundamental theorem**, which
- [fundamental.v](solutions/fundamental.v): The *fundamental theorem*, which
states that any syntactically typed program is semantically typed..
- [safety.v](solutions/safety.v): Proofs of semantic and syntactic type safety.
- [unsafe.v](solutions/unsafe.v): Proofs of "unsafe" programs, i.e. programs
Supports Markdown
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