Appendix

• Embedding
  • Types
  • Booleans
  • Exceptions and Errors
  • Pre- and Post-Conditions
  • Store
  • Modules
  • Module Instances
  • Functions
  • Tables
  • Memories
  • Tags
  • Exceptions
  • Globals
  • Values
  • Matching
• Implementation Limitations
  • Syntactic Limits
  • Validation
  • Execution
• Type Soundness
  • Contexts
  • Types
  • Subtyping
  • Results
  • Store Validity
  • Configuration Validity
  • Administrative Instructions
  • Store Extension
  • Theorems
• Type System Properties
  • Principal Types
  • Type Lattice
  • Compositionality
• Validation Algorithm
  • Data Structures
  • Validation of Opcode Sequences
• Custom Sections and Annotations
  • Name Section
  • Name Annotations
  • Custom Annotations
• Change History
  • Release 2.0
  • Release 3.0
• Index of Types
• Index of Instructions
• Index of Semantic Rules
  • Well-formedness of Types
  • Typing of Static Constructs
  • Typing of Runtime Constructs
  • Defaultability
  • Constantness
  • Matching
  • Store Extension
  • Execution