New Spaces for Denotational Semantics
Abstract
There are many possible degrees and dimensions of correctness for software programs, e.g. safety, functional correctness, computational complexity, and security. Grappling with the diversity of verification requirements, programming language theorists have developed many different mathematical models of program behavior that expose different aspects of program execution at different levels of detail or abstraction. Each of these models corresponds to a notion of computational space or domain , and the act of interpreting a program as a function on such a space is called denotational semantics. The objective of this project is to develop the axiomatic foundations of a generalized denotational semantics that brings the practical benefits of modular verification to realistic programming languages supporting difficult combinations of concurrency and higher-order computational effects, such as state.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Mar 14, 2024
- Source ID
- FA95502310728
Entities
People
- Jonathan Sterling
Organizations
- Air Force Office of Scientific Research
- United States Air Force
- University of Cambridge