Commit ca93fdb
feat: Initial Ephapax language implementation (#2)
Ephapax is a linear type system for safe memory management
targeting WebAssembly.
This commit includes:
Core Implementation:
- ephapax-syntax: AST definitions with linear type annotations
- ephapax-typing: Linear type checker with region support
- ephapax-wasm: WASM code generator with bump allocation
- ephapax-runtime: no_std WASM runtime with region management
Formal Semantics (Coq):
- Syntax.v: Core type and expression definitions
- Typing.v: Linear typing rules with context tracking
- Semantics.v: Operational semantics and safety theorems
Documentation:
- Language specification (spec/SPEC.md)
- Comprehensive wiki documentation
- ROADMAP.md with detailed development plan
- CONTRIBUTING.adoc guide
Infrastructure:
- Cargo workspace with 4 crates
- CI/CD workflow for Rust and Coq
- EUPL-1.2 license
Key features:
- Linear types prevent use-after-free and memory leaks
- Region-based memory management for bulk deallocation
- Second-class borrows for temporary access
- Formal proofs in Coq for type safety
Co-authored-by: Claude <noreply@anthropic.com>1 parent 9350b2b commit ca93fdb
0 file changed
0 commit comments