First-Class Environments and Environment Calculi
In ordinary programming languages, an environment, which associates variables with values, is usually hidden inside the implementation. This research develops a theory of first-class environments, where environments themselves can be created, passed, and composed as program values. By extending the lambda calculus, the work gives explicit reduction rules for variable lookup, environment update, and function application, and studies type safety, type inference, confluence, and evaluation strategies. These ideas also provide a common foundation for understanding dynamic software evolution, modules, records, and explicit substitutions.
Related Research
Continuations, Linear Logic, and Object Calculi
A continuation represents the rest of a computation from a particular point and treats it as a value. This concept provides a unified way to describe exception handling, coroutines, non-local exits, and backtracking. This research designs lambda calculi and object calculi in which continuations are first-class values, and studies their relationships with linear logic, evaluation order, type inference, and computational effects. In particular, it clarifies the relationship between linearity, where a resource is used exactly once, and continuations, which may duplicate computations, thereby providing foundations for type systems that safely handle advanced control mechanisms.
Related Research
Type Systems, Semantics, and Program Analysis
This research aims to verify mathematically, before execution, that programs behave as intended. Type systems can express not only ordinary data types, but also how functions may be used, how control flows, and which conditions must hold at run time. The work investigates polymorphic types, linear types, gradual typing, refinement types, and effect systems as methods for statically guaranteeing program safety and other properties. It also studies the relationships among big-step semantics, small-step semantics, abstract machines, and program transformations, connecting theoretical models with practical implementations.
Related Research
Model Checking for Safety, Reliability, and DoS Resistance
Model checking automatically explores the possible states of a system to determine whether undesirable behavior can occur. This research represents communication protocols, Web servers, e-mail systems, and load balancers as formal models, and verifies safety, reliability, policy compliance, and real-time properties. A particular focus is resistance to denial-of-service attacks. Process calculi that include time and computational cost are used to compare the workload imposed by an attacker with the processing capacity of a server. The work demonstrates how formal methods can be applied to the practical design and analysis of networked systems.
Related Research
Applications to Intelligent Systems, Distributed Computing, and Computing Education
This theme applies theoretical computer science to intelligent systems, education, and practical software. In artificial intelligence, the research combines knowledge representation with numerical computation to simulate complex biological regulation in an explainable form. In distributed computing, it explores methods that use existing Web infrastructure, such as blogs, as computational resources, as well as online proof and decision systems. It also develops project-based computing education that begins with real user needs and integrates requirements analysis, team building, international collaboration, and system development.
Related Research