Appendix

• Embedding
  • Types
  • Errors
  • Pre- and Post-Conditions
  • Store
  • Modules
  • Module Instances
  • Functions
  • Tables
  • Memories
  • Globals
  • References
• Implementation Limitations
  • Syntactic Limits
  • Validation
  • Execution
• Type Soundness
  • 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
  • Name Section
• Change History
  • Release 2.0
  • Release 2.?