All of the articles in this proceedings volume have been presented at the Workshop on Computation: Theory and Practice (WCTP2025) during December 1st — 3rd, 2025 in Chitose Arcadia Plaza, Chitose-city, Hokkaido, Japan. These articles have been peer reviewed by the members of the Program Committee and...

In this paper, we implement a framework for verifying programs targeting source code using the theorem prover Rocq and the program logic library Iris. As programming languages become more complex, it is becoming difficult to accurately describe their semantics. As a result, it is becoming increasingly...

This paper presents a practical framework for quantum indoor localization by focusing on the implementation details of its core subroutine, the SWAP test. The work integrates three key components: formal methods, statistical analysis, and simulation. First, we demonstrate the utility of modern verification...

Coverage checking is an essential static analysis for preventing runtime errors in programming languages with pattern matching. We present a work-in-progress formalization of Maranget’s algorithm in Agda. Although the algorithm targets simple patterns and does not support complex patterns such as those...

It is a standard result in recursion theory that sets of natural numbers recognized by Turing Machines can be mapped bijectively to Δ1 sets in  HF (i.e. the hereditarily finite sets). On the other hand, there are other sets in HF ,...

We have studied the lambda calculus with first-class environments in our previous work. The lambda calculus with first-class environments was an extension of the lambda calculus, but it had no destructive operation on the environment. For example, when we receive an actual parameter as a formal parameter,...

A workflow net is a computational tool for modeling business processes. Their verification is crucial for ensuring that the processes they model follow a criteria of correctness. In this paper, we observe that workflow net constructs can be mapped to programming language features. This mapping allows...

With the discrete logarithm problem (DLP) underpinning many modern cryptographic protocols, ensuring the correctness of algorithms that solve DLP is crucial for digital security. In this work, we present a machine-checked formalization of the Pohlig–Hellman algorithm in the Coq proof assistant. We introduce...

Metrocycle is a browser-based road safety education game developed to reinforce proper driving behaviors among Filipino motorcycle and bicycle riders through a gamified education approach. However, like any application, many of its aspects, such as user interface and user experience (UI/UX), accessibility,...

We have developed a system using Mixed Reality (MR) and sensor devices to aid Basic Life Support (BLS) self-training. Our system can provide BLS trainees with the real-time feedback of training score and post-training score visualization. It combines visual information provided by a MR device and physical...

Alzheimer’s disease cases in the Philippines are expected to increase exponentially by 2040. Non-pharmacological management of this disease involves physical therapy, occupational therapy, speech therapy, art therapy, and music therapy, which can be simulated in a virtual environment through an immersive...

The push-up is an accessible, low-equipment exercise where improvement comes through changes in positioning and leverage through progressions, rather than increasing weight. To produce optimal results from performing push-ups, one requires optimal form, traditionally advised through coaching. As coaching...

Learning string instruments such as the cello is notoriously difficult for beginners due to the challenges of intonation and bowing techniques, as well as the absence of clear physical guides. While textbooks and video materials provide visual information, they lack interactivity and real-time three-dimensional...

This study designed and evaluated an emotion-driven adaptive game system that dynamically modified difficulty level and genre in real time. The system estimated players’ emotional states by combining facial expression recognition with in-game performance metrics such as stage completion time. Based on...

In this study, we introduce a parallel implementation for generating sets of maximal activities for workflows or systems modeled using the Enriched Robustness Diagram with Loop and Time Controls (ERDLT). This is inspired by literature on its predecessor multidimensional workflow known as Robustness Diagram...

This study introduces and formalizes lazy soundness in Robustness Diagrams with Loop and Time controls (RDLTs), focusing on systems with parallel activities. Lazy soundness is a relaxation of classical soundness that tolerates the non-completion of certain concurrent activities, provided that exactly...

The Robustness Diagram with Loop and Time Controls is a kind of diagram that encapsulates every workflow dimension. Classical soundness, a workflow property of RDLTs, implies proper termination and liveness in the model if its requirements are met. Other soundness notions can be realized through loosening...

Facial recognition technology has advanced rapidly, but existing emotion recognition tools assume natural expressions and may not function accurately in strategic situations such as bluffing. This study analyzed facial expressions and physiological responses during a card game involving psychological...

Methods for inferring phylogenetic trees such as maximum likelihood-based methods face scalability challenges due to the computational cost of evaluating candidate trees. To address this, the study evaluates the potential of integrating machine learning models with branchswapping heuristics for guiding...

Zhang’s six-frame Alignment algorithm is a type of sequence alignment used to identify similarities between DNA and protein sequences and has a wide range of applications in bioinformatics. Zhang’s six-frame translates the DNA sequence across all six possible reading frames to specifically account for...

Minimizing edge crossings in graph drawings is crucial for improving readability. One variant, the k-layered hierarchical crossing minimization problem, seeks optimal vertex orderings across all layers of a k-layered graph to reduce crossings. We explore a hybrid layer-bylayer approach that combines...

In this study, the Online Facility Location Problem is examined using historical data on 911 EMS calls in Montgomery County. K-means clustering and the offline solution to a past year’s data are both explored as solutions to the online facility location problem and compared to existing online solutions...

Sequence alignment is the process of aligning two genomic sequences. It is the first step in various bioinformatics processes and is essential in many fields of genomics and bionformatics, such as de novo genome assembly and variant detection. One such sequence alignment algorithm is the Bi-Directional...

One major problem faced by quantum computing is how vulnerable qubits are to noise. Given this, the importance of quantum error correction in the field of quantum computing cannot be understated. Much research has been done on this topic, and many models of quantum error correction codes (QECCs) have...

This study integrates niche construction theory and cultural evolution theory to model emotional dynamics using Generative Adversarial Networks (GANs). Based on empirical data from 155 participants across five hypothetical cultural evolution stages, we developed a Research Based Emotion Evaluator and...

Studies that conduct sentiment analysis on Filipino or a mix of Filipino and English text data suffer from a lack of readily available language resources. Many studies result in losing linguistic information when translating to a high-resource language or undergo the painstaking and expensive process...

Teaching evaluations provide essential feedback for improving educational quality, yet institutions struggle to efficiently utilize unstructured student comments. This study implements ordinal logistic regression to analyze 4,410 bilingual (English-Filipino) student comments, creating a probabilistic...

Short Message Service (SMS) phishing, or smishing, is an escalating cybersecurity threat in the Philippines, where widespread mobile usage intersects with informal language and frequent code-switching between Filipino and English. While prior studies have primarily focused on English-language datasets,...

With the rise of consumer-centric genomic testing services, there is an increased risk of data breaches and privacy concerns regarding sensitive genomic data. Paternity testing, one of the most common genetic tests, is no exception to this risk. To address this privacy risk, Fully Homomorphic Encryption...

This study investigates the performance impact of concurrent queries on encrypted DNS protocols. We conducted experiments on a virtual machine, measuring query response times under several conditions. We compared single versus concurrent queries for individual protocols (Do53, DoT, DoH, DoH3, and DoQ),...

As vehicles become more connected and autonomous, intrusion detection systems must adapt to emerging threats while preserving user privacy. This paper presents a privacy-preserving vehicle IDS that integrates federated learning (FL) and homomorphic encryption (HE) to detect denial-of-service, fuzzy,...

Public transportation in the Philippines is multimodal and demand-responsive, yet commuters lack access to real-time, reliable route information. Existing navigation apps like Google Maps and Waze cater primarily to private vehicles, while local alternatives such as Sakay.ph and Moovit suffer from outdated...

This research presents adapted implementations of Breadth-First Search (BFS) and Dijkstra’s algorithm for real-time flood prediction and evacuation routing. The work shows how government sensor data can be transformed into accessible disaster information for communities. The BANTAY system uses optimized...

JeePS, a real-time transportation tracking system, is a web and mobile application designed to improve passenger satisfaction with Public Utility Vehicles (PUVs). This paper introduces JeePS 2.0, an improved version designed to overcome the limitations of the original system through new features, including...