Formalization

Paper on Integrated Technologies of Care published in Nature Scientific Reports

Our paper titled “Integrated technologies of care: proof-of-concept study on an integrated physiological and activity monitoring system to enhance independence and care” has just been published by Nature Scientific Reports. You can access it here. The showcases work done as part of the Advanced Care Research Centre (ACRC).

Abstract

This study presents a multi-sensor activity monitoring system designed to verify daily behaviours and detect physiological anomalies within a controlled home environment. Seven subjects participated in a scripted routine of Activities of Daily Living carried out in a home-like environment. The proposed system is designed for single-occupancy environments (e.g. individuals living alone). Accordingly, this proof-of-concept evaluation was conducted under controlled, single-participant conditions using sequential, non-concurrent activities and excluding overlapping sensor changes. Within the routine, different sensors capture physiological hydration levels and breathing rates of the participant as sensor events, to check whether the measurements were within normal levels. In addition, camera, contact, motion and pressure sensors are used to capture action triggered events within the routine. Sensor data is processed and translated into a time-ordered trace of events. A model is constructed to capture the layout of the controlled environment and the trace of events. Expected behaviours are specified as properties encoded in Linear Temporal Logic and model checking is used to assess whether the sensor-captured events align with these expectations. Through model checking, the captured behaviour can be verified against a set of logical formulae representing properties. The identified deviations from expected behaviours demonstrate the viable application of model checking in the verification of Activities of Daily Living. Cross-sensor data aggregation compensates for occasional sensor inaccuracy, ensuring reliability. The initial results support the system’s potential for use in behaviour and physiological monitoring of people living independently, where accurate and unobtrusive monitoring is crucial.

Reconstruction of Euler’s proof published in the AFP

Our development of “Euler’s Exponential Series as an Infinite Polynomial” has been accepted and published by the Archive of Formal Proofs.

Abstract:
In this formalisation, we reconstruct Euler’s derivation of the power series for the exponential function as expounded in his famous Introductio in analysin infinitorum, first published in 1748. Using nonstandard analysis, we mechanize his mixture of infinitesimal and infinite ‘algebraic’ reasoning in the proof assistant Isabelle. In so doing, we demonstrate that the gist of his arguments can be reconstructed formally, with Isabelle and nonstandard analysis shoring up crucial aspects of his reasoning that some historians have qualified as being “more a matter of faith than science”.

The full formalization is available here:

IsaGrad paper accepted at LogicNN 2026

Our paper “IsaGrad: Verified Automatic Differentiation over Computational Graphs in Imperative HOL” has been accepted and will be presented at LogicNN, FLOC 2026.

The Gelfand–Naimark–Segal Construction published in the AFP

Our development of the “The Gelfand–Naimark–Segal Construction” has been accepted and published by the AFP.

Abstract

This entry formalises complete normed algebras equipped with an involution, so-called C*-algebras. We provide both a class definition, and a locale for C*-algebras on carrier sets in the spirit of existing developments of linear algebra and smooth manifolds. Bounded operators on a complex Hilbert space, with the operator norm and adjoints, form such an algebra. The main theorem of this entry is a result in the converse direction: the Gelfand–Naimark–Segal (GNS) construction, which starts with a single suitable functional on a C*-algebra in order to obtain both a Hilbert space and a representation of the algebra in terms of bounded operators on that space. This is implemented as a type construction in Isabelle/HOL, taking advantage of existing mechanisms for quotient types, and integrating with existing type classes for Hilbert spaces and Cauchy completions.

The full formalisation is available here.

Our paper on differentiable Signal Temporal Logic for neurosymbolic AI has been published by LIPIcs

GradSTL: Comprehensive Signal Temporal Logic for Neurosymbolic Reasoning and Learning

Authors Mark Chevallier , Filip Smola , Richard Schmoetten , Jacques D. Fleuriot

Part of: Volume: 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Symposium on Temporal Representation and Reasoning (TIME)

Our pre-print on differentiable Signal Temporal Logic for neural learning is out on arXiv

Abstract:

We present GradSTL, the first fully comprehensive implementation of signal temporal logic (STL) suitable for integration with neurosymbolic learning. In particular, GradSTL can successfully evaluate any STL constraint over any signal, regardless of how it is sampled. Our formally verified approach specifies smooth STL semantics over tensors, with formal proofs of soundness and of correctness of its derivative function. Our implementation is generated automatically from this formalisation, without manual coding, guaranteeing correctness by construction. We show via a case study that using our implementation, a neurosymbolic process learns to satisfy a pre-specified STL constraint. Our approach offers a highly rigorous foundation for integrating signal temporal logic and learning by gradient descent.

Paper: https://www.arxiv.org/abs/2508.04438

This work has been accepted as a long paper at TIME 2025 and will be presented at the conference at the end of August 2025.

Our formalisation of Linear Resources and Process Compositions has been published in the Archive of Formal Proof

Abstract

In this entry we formalise a framework for process composition based on actions that are specified by their input and output resources. We verify their correctness by translating compositions of process into deductions of intuitionistic linear logic. As part of the verification we derive simple conditions on the compositions which ensure well-formedness of the corresponding deduction.

We describe an earlier version of this formalisation in our article Linear Resources in Isabelle/HOL, which also includes a formalisation of manufacturing processes in the simulation game Factorio.

Our formalisation of Lie Groups and Algebras has been published in the Archive of Formal Proof

Abstract

Lie Groups are formalised as locales, building on the AFP theory of Smooth Manifolds. We formalise the diffeomorphism group of a manifold, and the action of a Lie group on a manifold. The general linear group is shown to be a Lie group by proving properties of the determinant, and matrix inverses. We also develop a theory of smooth vector fields on a manifold , defined as smooth maps from the manifold to its tangent bundle . We employ a shortcut that avoids difficulties in defining the tangent bundle as a manifold, but which still leads to vector fields with the properties one would expect. We then construct the Lie algebra of a Lie group as an algebra of left-invariant smooth vector fields.

Schmoetten R. and Fleuriot J. D. (2024). Lie Groups and Algebras. Archive of Formal Proofs. ISSN: 2150-914x.