Naso Evangelou-Oost

General Purpose South 78-414

The University of Queensland

St Lucia, Qld 4067

Dr. Naso Evangelou-Oost, Senior Mathematician at Sirius-beta Labs.

Senior Mathematician — Sirius-beta Labs

At Sirius-beta Labs, I engage in mathematical research and software design across knowledge representation, formal methods, and predictive systems. My work applies abstract mathematical frameworks—valuation algebras, sheaf theory, and category theory—to build scalable, resilient, intelligent software systems bridging theory and implementation.

Research Interests:

Valuation Algebras: Abstract algebraic structures with wide-ranging applications.
Sheaf Theory: Tools for understanding local-to-global behaviours in mathematical contexts.
Formal Methods: Rigorous specification and verification of complex software systems.
Concurrent and Distributed Systems: Creating more robust and resilient technologies.

Founder — Oneironaut

I founded Oneironaut, a mathematical software consultancy where category theory, artificial intelligence, and functional programming converge to solve complex problems. This work transcends technology trends, applying mathematical insight to challenges in knowledge representation and predictive analytics.

Oneironaut embodies innovative thinking through mathematical elegance. My practice bridges abstract theory and practical application, translating mathematical concepts into client value.

Selected publications

Trace Models of Concurrent Valuation Algebras

Naso Evangelou-Oost, Larissa Meinicke, Callum Bannister, and 1 more author

In Formal Methods and Software Engineering, 2023

Abs Bib

This paper introduces Concurrent Valuation Algebras (CVAs), a novel extension of ordered valuation algebras (OVAs). CVAs include two combine operators representing parallel and sequential products, adhering to a weak exchange law. This development offers theoretical and practical benefits for the specification and modelling of concurrent and distributed systems. As a presheaf on a space of domains, CVAs enable localised specifications, supporting modularity, compositionality, and the ability to represent large and complex systems. Furthermore, CVAs align with lattice-based refinement reasoning and are compatible with established methodologies such as Hoare and Rely-Guarantee logics. The flexibility of CVAs is explored through three trace models, illustrating distinct paradigms of concurrent/distributed computing, interrelated by morphisms. The paper also highlights the potential to incorporate a powerful local computation framework from valuation algebras for model checking in concurrent and distributed systems. The foundational results presented have been verified with the proof assistant Isabelle/HOL.
@inproceedings{evangelouoost2023a, address = {Singapore}, author = {Evangelou-Oost, Naso and Meinicke, Larissa and Bannister, Callum and Hayes, Ian J.}, booktitle = {Formal Methods and Software Engineering}, editor = {Li, Yi and Tahar, Sofi{\`e}ne}, isbn = {978-981-99-7584-6}, pages = {118--136}, publisher = {Springer Nature Singapore}, title = {Trace Models of Concurrent Valuation Algebras}, year = {2023} }
Contextuality in Distributed Systems

Nasos Evangelou-Oost, Callum Bannister, and Ian J. Hayes

In Relational and Algebraic Methods in Computer Science, 2023

Abs Bib

We present a lattice of distributed program specifications, whose ordering represents implementability/refinement. Specifications are modelled by families of subsets of relative execution traces, which encode the local orderings of state transitions, rather than their absolute timing according to a global clock. This is to overcome fundamental physical difficulties with synchronisation. The lattice of specifications is assembled and analysed with several established mathematical tools. Sets of nondegenerate cells of a simplicial set are used to model relative traces, presheaves model the parametrisation of these traces by a topological space of variables, and information algebras reveal novel constraints on program correctness. The latter aspect brings the enterprise of program specification under the widening umbrella of contextual semantics introduced by Abramsky et al. In this model of program specifications, contextuality manifests as a failure of a consistency criterion comparable to Lamport’s definition of sequential consistency. The theory of information algebras also suggests efficient local computation algorithms for the verification of this criterion. The novel constructions in this paper have been verified in the proof assistant Isabelle/HOL.
@inproceedings{evangelouoost2023b, address = {Cham}, author = {Evangelou-Oost, Nasos and Bannister, Callum and Hayes, Ian J.}, booktitle = {Relational and Algebraic Methods in Computer Science}, editor = {Gl{\"u}ck, Roland and Santocanale, Luigi and Winter, Michael}, isbn = {978-3-031-28083-2}, order = {4}, pages = {52--68}, publisher = {Springer International Publishing}, title = {Contextuality in Distributed Systems}, url = {https://link.springer.com/chapter/10.1007/978-3-031-28083-2_4}, year = {2023} }