Formal Logic and Computational Models

Report on Current Developments in the Research Area

General Direction of the Field

The recent developments in the research area indicate a significant shift towards more abstract and foundational approaches, with a strong emphasis on formalizing and axiomatizing various logical and computational structures. The field is witnessing a convergence of ideas from different domains, such as temporal logic, probabilistic programming, and algebraic computation, leading to innovative frameworks that bridge traditional boundaries.

One of the key trends is the exploration of new logical systems that extend beyond classical models, incorporating temporal, probabilistic, and algebraic elements. These systems are being developed to address specific challenges in areas like biomedicine, clinical research, and computational indistinguishability, where existing frameworks are either too restrictive or too permissive. The introduction of novel logics, such as Temporal Ensemble Logic (TEL), reflects a need for more nuanced temporal reasoning that can capture complex sequential properties in these domains.

Another notable direction is the focus on compositional theories and the development of comprehensive calculi for module interaction and composition. This approach seeks to provide a unified framework for understanding and formalizing the behavior of interacting modules, which is increasingly recognized as a fundamental aspect of computation. The proposed composition calculus aims to be a foundational theory that can encompass a wide range of settings, from digital systems to more abstract computational models.

Probabilistic programming is also gaining traction, with researchers introducing sound and complete equational theories for discrete probabilistic programs. These developments not only advance the theoretical understanding of probabilistic computation but also have practical implications for the formalization of probability theory in Markov categories.

The field is also seeing a renewed interest in the foundational aspects of computational models, such as the Weihrauch lattice and intuitionistic propositional logic. These studies are contributing to a deeper understanding of the equational theories underlying these models, with implications for decidability and complexity.

Noteworthy Developments

  • Temporal Ensemble Logic (TEL): Introduces a novel temporal logic tailored for biomedicine, addressing the limitations of existing frameworks.
  • Composition Calculus: Proposes a foundational theory for module interaction and composition, with broad applicability across computational settings.
  • Equational Theory for Discrete Probabilistic Programming: Provides a complete axiomatization for probabilistic programs, advancing the formalization of probability theory.
  • Weihrauch Lattice with Iterated Composition: Offers a complete axiomatization and game-theoretic characterization, contributing to the understanding of computational models.
  • Parallel and Algebraic Lambda-Calculi: Introduces a novel interpretation of parallel operators within propositional logic, challenging conventional approaches.
  • Weak Distributive Laws between Monads: Demonstrates weak distributive laws between various monads, with applications in probabilistic and topological settings.
  • Collapsing Constructive and Intuitionistic Modal Logics: Proves the equivalence of constructive and intuitionistic variants of modal logic KB, contrasting with previous results on modal logic K.
  • Computational Indistinguishability and Logical Relations: Introduces a λ-calculus for probabilistic polynomial time evaluation, with implications for cryptographic security proofs.

Sources

Model-checking positive equality free logic on a fixed structure (direttissima)

Temporal Ensemble Logic

Once and for all: how to compose modules -- The composition calculus

A Complete Axiomatisation of Equivalence for Discrete Probabilistic Programming

The equational theory of the Weihrauch lattice with (iterated) composition

Parallel and algebraic lambda-calculi in intuitionistic propositional logic

Weak Distributive Laws between Monads of Continuous Valuations and of Non-Deterministic Choice

Collapsing Constructive and Intuitionistic Modal Logics

On Computational Indistinguishability and Logical Relations