We present ENVCAP, a statically typed programming language based on environment-based semantics that supports first-class environments, capabilities, and separate compilation. Using the environment-based semantics of λE calculus, ENVCAP models capabilities as first-class modules based on first-class environments as an alternative to the object-capability model and enables separate compilation without any extra-linguistic structures. We provide an interpreter implementation and formalize the type-directed elaboration from core ENVCAP to λE calculus in Rocq.

I am a research intern at the Max Planck Institute for Security and Privacy in Bochum, Germany, and a final-year undergraduate student at the University of Hong Kong. My research interests lie in formal methods, programming languages, and quantum computing.