Formal typing rules and presentation materials for Swift 6.2's concurrency type system, focusing on Capability (where code runs) and Region (where data lives).
Presented at try! Swift Tokyo 2026.
- Video: https://youtu.be/Vs_hytYk3HU
- Slide (HTML): https://inamiy.github.io/swift-concurrency-type-system/slide.html
- Slide (PDF): https://speakerdeck.com/inamiy/swift-concurrency-type-system
| Format | File | Description |
|---|---|---|
| Slide (PDF) | swift-concurrency-type-system-slide.pdf | Marp slide deck |
| Paper (PDF) | swift-concurrency-type-system-paper.pdf | LaTeX paper (ACM sigplan format) |
| Beginner Guide (JA) | docs/beginner-guide-ja.md | Gentle introduction to basic logic / typed lambda calculus notation |
| Beginner Guide (EN) | docs/beginner-guide-en.md | English translation of the beginner guide |
| Typing Rules (JA) | docs/typing-rules-ja.md | Source of truth (Japanese) |
| Typing Rules (EN) | docs/typing-rules-en.md | English translation |
The judgment form central to the type system:
Γ; @κ; α ⊢ e : T at ρ ⊣ Γ'
| Symbol | Role | Examples |
|---|---|---|
@κ (Capability) |
Where code runs | @nonisolated, @MainActor |
ρ (Region) |
Where data lives | disconnected, isolated(a), task |
Γ → Γ' |
Affine discipline | Region merge refines, transfer shrinks |
Covers function conversion rules, sending as affine transfer, region merge as context refinement, and closure isolation inference.
| Proposal | Title |
|---|---|
| SE-0414 | Region-based Isolation |
| SE-0430 | sending parameter and result values |
| SE-0431 | @isolated(any) function types |
| SE-0461 | Nonisolated nonsending by default |
./
├── docs/ # Formal typing rules, beginner guide & conversion diagrams
│ ├── beginner-guide-ja.md # Gentle introduction to logic / typed lambda calculus notation
│ ├── beginner-guide-en.md # English translation of the beginner guide
│ ├── typing-rules-ja.md # Source of truth (Japanese)
│ ├── typing-rules-en.md # English translation (must be kept in sync with -ja)
│ ├── scripts/ # Helper scripts (markdown-toc, Mermaid splitter)
│ └── diagrams/ # Mermaid diagram sources
├── swift/ # SwiftPM package (swift-tools-version: 6.2, Swift 6 mode)
│ ├── Sources/
│ │ └── concurrency-type-check/ # Isolation/region/sending experiments
│ └── Tests/
│ └── concurrency-type-checkTests/
├── swift-sil/ # SIL dump analysis (Swift source + emitted SIL pairs)
│ └── docs/ # SIL reading guides
├── slide/ # Marp-based presentation (md -> html via marp-cli)
│ ├── src/ # Slide source (md, themes, assets)
│ └── scripts/ # Build scripts (mermaid splitter, TTS)
├── paper/ # LaTeX paper (ACM sigplan format via tectonic)
└── swiftlang/ # Git submodules (read-only reference, git-ignored)
├── swift/ # Official Swift compiler source
└── swift-evolution/ # Swift Evolution proposals
| Command | Description |
|---|---|
make setup |
Install npm deps and generate Mermaid diagrams |
make -C slide html |
Build slide HTML into slide/dist/ |
make -C slide pdf |
Build slide PDF into slide/dist/ |
make -C paper pdf |
Build paper PDF via tectonic |
make markdown-toc |
Regenerate table of contents in typing rules docs |
make diagrams |
Regenerate Mermaid diagrams only |
make clean |
Remove all build artifacts |
cd swift && swift build |
Build Swift package |
cd swift && swift test |
Run Swift tests |
- Typing Rules Workflow — Rules for creating/modifying typing rules and verification
- For Swift internals, type checker behavior, SIL, or language evolution, consult the
swiftlang/directory. - Use English as a default language for any file output except filenames suffixed with
-{lang}.{ext}. - Avoid section-number cross-references (e.g. "(§3.8.1)") in documentation; prefer heading titles or rule names.
- Use ASCII parentheses
()instead of full-width parentheses（）in all documentation files. - In
docsmarkdown files, DO NOT manually edit "Table of Contents" sections unless explicitly requested, which is auto-generated.