This project exploits recent advances in the use of sophisticated mathematical methodologies to address related fundamental questions in the foundations of computation theory and programming language semantics. Many important questions arise out of a desire and need to capture in a semantic setting both minor and major variations in computational strategies. The significance in investigating such variations lies in the fact that they can both provide a means of interpreting increasingly sophisticated programming language constructs, and also isolate fundamental mathematical processes at work that help define and distinguish between different notions of computation. The main focus of the research entails the utilization of new approaches in the use of algebras, monads and comonads, categories, logic and sheaves to provide a systematic and conceptual approach to the interpretation and solution of these questions. Questions to be addressed include: finding an algebraically robust interpretation for partial data types and partial maps; generating an intrinsic characterization of fixed point constructions, including the generation of recursive data types, and isolating the special role of invariance in this process; defining a categorical foundation for semantics in general and describing a synthetic domain theory in particular; and identifying and utilizing in a semantic setting logical properties resident in sheaf-theoretic structures. General areas of investigation include partial data types and computation, fixed point semantics, monadic and comonadic computation, invariance and algebras, and partial sheaf semantics. Technical tools include functorial liftings on categories of algebras, refined partial map classifiers, algebraic uniformity, induction and coinduction principles, natural and dinatural transformations, monadic and comonadic strength, domain theory and extensional PERs.
