Intrinsically Typed Compilation with Nameless Labels
summary
Claims a compositional way to intrinsically type bytecode by replacing global names with nameless labels and a co-contextual interface algebra, implemented as a linear, dependently typed shallow embedding in Agda. It builds a compiler monad (writer-style) that needs no state for fresh labels, uses an ownership predicate and proof-relevant separation logic to ensure each label is defined exactly once and every jump is well-bound, and delivers a working Agda implementation plus pipeline (SNOB elimination, assembly) with no separate type-correctness proof.
AI-written summary · about
chapters (4)
related talks
16mAn Intrinsically Typed Compiler for Algebraic Effect Handlers
41mThe Dialectics of Type-Level Programming
01h 07mBuilding a Dependently Typed Language in Haskell Part 1
18mBlame-aware Recomposition for Formally Secure Low-level Compiler Backends
31mDependent tagless final
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
19mIll-Typed Programs Don't Evaluate
21mSyntax with Shifted Names