2nd Workshop on Logic, Algebra and Category Theory: LAC 2025

Fukuoka, September 29 – October 3, 2025

Co-organized by the Institute of Mathematics for Industry at Kyushu University and Universitat Politècnica de València

Aims and Scope

Modern specification languages are based on logic. For any such language there exists a specific logical system underlying the language's features and constructions. The logic-based approach has great advantages for formal software verification, since it guarantees precision and clarity in the process of software development. On the other hand, it resulted in a proliferation of logical systems in specification theory, each tailor-made for a particular language. Essentially the same arguments and results had to be used for each of these systems, just to fit a different language. To avoid such redundancies, a unifying framework is clearly needed. One could then prove logical results in an abstract way and then apply them to concrete specification languages. Such a framework would also contribute to a deeper understanding of the causality relations between logic properties which are often hindered by the unnecessary details of concrete logics.

Category theory suggests itself as a general supporting structure, since it focuses on relations between objects rather than the precise way the objects are built. On the other hand, universal algebra plays an important role in defining the semantics of algebraic specification languages. Therefore, there exists a strong connection between logic, category theory and algebraic structures, especially in the context of formal methods, where mathematically grounded techniques are developed for modeling and verifying complex systems in various fields of computing science.

Poster

Speakers from the Industrial Sector

Academic Speakers

Early Career Research Speakers

Programme

Monday (Chair: Daniel Găină)

10:00–10:10
Opening
10:10–11:10
Hung Q. Ngo, Optimization techniques for a Datalog-inspired query language
11:10–11:40
Guillermo Badia, Containment of Conjunctive Queries with Equations and Disequations for Databases over Semiring
11:40–14:30
Lunch break
14:30–15:00
Sasha Rubin (online), Tight inference and real-valued logic
15:00–15:30
Krzysztof Krawczyk (online), Structural completeness among finitary extensions of R-mingle

Tuesday (Chair: Ionut Tutu)

10:00–10:30
Hiroakira Ono, A glance at extensions of bi-intuitionistic logic
10:30–11:00
Zbyszek Krol, On some forms of logical connections between theories
11:00–12:00
Mark Reynolds, A tree-shaped tableau for Linear Time Temporal Logic
12:00–14:00
Lunch break
14:00–15:00
Kazuhiro Ogata, Formal Specification and Verification of Post-quantum Cryptographic Protocols with Proof Scores
15:00–16:00
Kokichi Futatsugi, Constructing proof scores in CafeOBJ
18:00–20:00
Dinner party

Wednesday (Chair: Guillermo Badia)

10:00–11:00
Jonathan Lenchner, On Some Relatives of the Ehrenfeucht-Fraïssé Game and Software for Helping with the Analysis of these Games
11:00–12:00
Tomasz Kowalski, Hybrid-Dynamic Ehrenfeucht-Fraïssé Games
12:00–14:30
Lunch break
14:30–15:00
Diamant Pireva (online), Many-Sorted First-Order Logic with Quantification over Inter-Sort Functions
15:00–15:30
Carles Noguera (online), Fagin’s Theorem for Semiring Turing Machines

Thursday (Chair: Adrian Riesco)

10:00–11:00
Santiago Escobar, Unification and Narrowing in Maude 3.5
11:00–12:00
Francisco Durán, NuITP: An Inductive Theorem Prover for Maude
12:00–14:00
Lunch break
14:00–15:00
Marcel Jackson (online), Minimal signatures for undecidability of representability for relation algebras
15:00–16:00
Narciso Martí Oliet (online) and Ruben Rubio, Strategies, qualitative and quantitative model checking in Maude
16:00–16:30
Beatriz Alcaide García (online), MongoDB specification in Maude

Friday (Chair: Tomasz Kowalski)

10:00–11:00
Ionuț Țuțu, Forcing, Transition Algebras, and Calculi
11:00–12:00
Adrián Riesco Rodríguez, Executable Specifications in Transition Algebra
12:00–14:00
Lunch break
14:00–14:30
Go Hashimoto, Model-theoretic Forcing in Transition Algebra
15:00–15:10
Closing

Registration

We are now accepting registrations!

To register for LAC 2025, please fill in the following form.

Zoom broadcast details will be sent to all registered participants!

Venue

The workshop will be held at Ito Campus, IMI Auditorium (W1 - D 413).

Maps and details about the location can be found here.

If you're using public transportation, we recommend taking the train to Kyudai-Gakkentoshi Station, followed by a bus to the Ito Campus. Please refer to the link above for more details.

Accommodation

Accommodation options nearby include:

  • Ito Glocal Hotel
    Location: 15 min by bus to Kyushu University Ito Campus
    Highlights: Popular among university visitors, often offers special rates for Kyushu University affiliates
    Note: Booking may require Japanese language or browser translation tools

  • Nishijin Plaza (Kyushu University Facility)
    Address: 2-16-23 Nishijin, Sawara-ku, Fukuoka 814-0002
    Phone: +81-92-802-2322
    Highlights: University-affiliated lodging, ideal for academic visitors

  • The Residential Suites Fukuoka
    Address: 1‑3‑70 Momochihama, Sawara‑ku, Fukuoka‑shi, Fukuoka 814‑0001, Japan
    Phone: +81-92-846-8585

Organizers

Contact

If you have any questions or inquiries about LAC 2025 you can contact us via e-mail at lac2025 [at] imi.kyushu-u.ac.jp