Formalization of the labelled sequent calculus for intuitionistic modal logic (LabIK) in the Coq proof assistant. We discuss different approaches and design choices made, precisely when it comes to representing the different contexts and the labels necessary for the system. We also discuss the challenges faced during the formalization and the limitations of our implementation.

Implementation was done in OCaml while making use of the 'Logical' tool for the proof search of BV, specifically. Proof search in Pomset was implemented as the search of cycles on graphs: restricted to balanced formulas. The implementation in Pomset was used as a benchmark for testing the proof search on BV.

Research on the link between equational and graphical structures. Transforming the categorical definition of a terminal object to an equational definition using the work done by Albert Burroni. Defined the relevant type system and its rules for terms, contexts and equalities.

Implemented a domain-informed module in ProgLog to guide the reward shaping of a Reinforcement Learning (RL) module. Independently gathered related work to better identify the problem of reward shaping in RL and investigate possible solutions. Adapted a deep-learning architecture to include a logic module, the model was formalized accordingly.

Provided a logical framework for distributed evidential transactions. Compiled relevant related work and proved cut-elimination for the logic (interesting proof found in annex of the paper).

Formalized and implemented a survival game scenario based on predators and preys. Action is determined by behavior and decision in the environment. Experimenting on outcomes of behavioral modulations and its learned effects on decisions.