Programming Languages
Implementation of a Programming Language with Capabilities as First-Class Modules with λE as the Core Calculus.
Jam Kabeer Ali Khan (3035918749)
Supervisor: Bruno C. d. S. Oliveira
Introduction
Most common programming languages do not restrict access to system resources across different sections of the codebase. An increase in codebase with no authority division between its components can lead to security vulnerabilities as insecure code can exploit system resources even if it does not require access to specific system resources to execute its tasks. Capabilities provide a mechanism to restrict access to system resources which are traditionally modeled as objects, recent advancements in λE calculus allows using first-class environments as an alternative representation for capabilities. This research project will design and implement a programming language that incorporates capabilities as first-class modules and supports separate compilation, utilizing λE as the core calculus.
Main Features
Environment-Based Semantics
Reducing the gap between theory and implementation.
Capabilities
Capabilities to write secure code based on the Principle of Least Authority.
Core Calculus λE
Enable formal reasoning for the implementation for correctness.
Types
Implementation of type checker to avoid run-time errors.
Separate Compilation
Enabling compilation with header files and modular type checking.
Design and Elaboration
Design of syntax of the surface language elaborated to the core semantics.