The Journal of Logical and Algebraic Methods in Programming is an international journal whose aim is to publish high quality, original research papers, survey and review articles, tutorial expositions, and historical studies in the areas of logical and algebraic methods and techniques for guaranteeing correctness and performability of programs and in general of computing systems. All aspects will be covered, especially theory and foundations, implementation issues, and applications involving novel ideas.

Topics of interest to the journal include:
• Applications of algebras, co-algebra and categories to programming
• Applications of proof theory and model theory to programming
• Constraint programming
• Foundations of Programming Paradigms
• Logic programming
• Logical Foundations of Program Security
• Models and Analytical Models for Cyber-Physical Systems
• Process Calculi
• Programming Models
• Quantitative Methods for System Analysis
• Specification and verification of systems

The Journal of Logical and Algebraic Methods in Programming complements Elsevier's Science of Computer Programming and Theoretical Computer Science by its focus on the foundations and the application of logical, algebraic and categorical methods to programming and to the development of trustworthy computing systems.

Special Issue on Foundations for Effective and Correct Runtime Monitoring
Submission Date: 2023-11-30

Guest editors:
Adrian Francalanza
Email: adrian.francalanza@um.edu.mt
Special issue information:
Runtime monitoring is an increasingly popular technique for improving software reliability, correctness and performance. It can be broadly construed as the runtime analysis of systems in order to infer aspects of their behaviour to potentially affect their current execution. Runtime monitoring brings about various advantages, from the convenience of dynamically generating a system model from its own execution, to the opportunities afforded to conduct fault containment and error recovery. Example applications of the technique include telemetry, log aggregation, threshold alerting, performance monitoring and runtime verification/enforcement; aspects of monitoring also manifest themselves as part of established software techniques such as testing.
The scope of this theme covers the various challenges of devising formal approaches and theories underpinning the specification, analysis, and realisation of effective monitored systems. These include (but are not limited to) aspects such as:
+ system instrumentation and event extraction;
+ execution recording and replaying;
+ fault localization, recovery and resilience;
+ automated monitor synthesis and program repair;
+ programming language support for runtime analysis and verification;
+ the connections between specification logics and correct runtime analysis; and
+ the integration of monitoring with other verification techniques.
Manuscript submission information:
Submission deadline: 30th November 2023
Learn more about the benefits of publishing in a special issue: https://www.elsevier.com/authors/submit-your-paper/special-issues
Interested in becoming a guest editor? Discover the benefits of guest editing a special issue and the valuable contribution that you can make to your field: https://www.elsevier.com/editors/role-of-an-editor/guest-editors
------------
Guest editors:
------------
Adrian Francalanza
------------
Email: adrian.francalanza@um.edu.mt 

Special Issue on Logic and Type Theoretic Foundations of Concurrent and Distributed Systems
Submission Date: 2023-11-30

The continuous development of networks and communicating systems at the heart of the digital revolution raises new challenges to logic and formal methods in Computer Science. The need for new methods for designing and verifying software and hardware systems has fostered both the introduction of new logics and the adaptation and extensions of preexisting logical systems.

In the literature, there are many different models of concurrency, such as transition systems and automata, domain-theoretic models, game-theoretic models, process algebras, Petri nets, mobile and collaborative systems, etc. On the one hand, several logics were introduced to reason about them, formalising basic properties like deadlock freedom, behavioural equivalence, safety and liveness, security and scalability. These formalisations underpin the analysis, synthesis and verification of concurrent programs and systems. On the other hand, type systems were devised to structure programs and systems in such a way that the same properties are guaranteed. To assess essential issues such that soundness and expressivity of type systems, it is essential to study their connections with logic.

With respect to the theme, topics of interest include (but are not limited to):

- logics for concurrency such as modal logics, probabilistic and stochastic logics
- resource-aware logics and type systems, such as linear logic, temporal and spatial logics
- logic-based techniques for specification and verification of concurrent programs and systems, including automata and model checking
- formalisms and type systems for process coordination and protocol specification, such as choreographies and session types
- language-based security and proof-carrying code
- game theoretic models of logic and computation