Glossary

• anonymous type: A type built from its interpretation, thus without syntax.
• associated proof: An associated constant of the proof type.
• bottom type: The type with an empty interpretation.
• permissions to use: Characteristic of a robust type.
• promised type: The type at the end of a borrow of a mutable reference.
• restrictions to use: Characteristic of an unsafe type.
• robust type: An anonymous type missing some safe values.
• safe type: A Rust type (its interpretation is exactly the safe values).
• safe value: A value satisfying the safety invariant.
• soundness: The property of type systems that only accept defined programs.
• subtyping: The inclusion relation between type interpretations.
• type interpretation: A mapping from types to their set of values.
• unsafe type: An anonymous type containing some unsafe values.
• unsafe value: A valid but not safe value.
• valid value: A value satisfying the validity invariant.
• value: A part of the execution of a program.
• variance: Type-level functions behavior regarding subtyping.