2023 -- A Correct-by-Construction Approach to Approximate Computation

Project funded by the Engineering and Physical Sciences Research Council (EPSRC), UK Research and Inovation (UKRI)
Budget - GBP 865,000 (FEC)
Principal investigator Prof. Radu Mardare
Co-investigators
Prof. Neil Ghani (Strathclyde)
Dr. Fredrik Nordvall Forsberg (Strathclyde)
Collaborators
Prof. Gordon Plotkin (Edinburgh)
Prof. Prakash Panangaden (McGill, Canada)
Prof. Luca Cardelli (Oxford)
Prof. Thorsten Altenkirch (Nottingham)
Dr. Edwin Brady (St Andrews)
National Physics Laboratory (NPL)
Abstract:
Correct-by-construction program development uses advanced type systems to describe both the data manipulated by computation, and the correctness of those computations. Embedding correctness within software has many advantages, as certified by several decades of pioneering work in the UK and elsewhere, which have culminated in systems such as Agda, Idris, Coq, Lean, HOL, Isabelle, etc., which are powerful enough to implement this vision and which are now having significant impact in both academia and industry.
The main question that motivates this research is: can correct-by-construction programming be extended to computation with approximate values, e.g. in: i) stochastic systems where one needs to handle inherent/simulated randomness; ii) resource limited environments, where exact computation is prohibitively expensive; iii) systems with imperfect/partial recall, where one only has limited information about what has happened or the intentions/trustworthiness of each agent; and iv) non-exact computation where primitive data (e.g. from sensors) is inexact and supplied with error bars. These scenarios arise in e.g. cyber-physical systems, machine learning, robotics, automotive engineering, aerospace, and energy systems. Measuring how close measurements might be from their true values naturally leads to the use of metrics but, despite some successes, their use suffers from a number of drawbacks, e.g. i) metrics defined in one problem domain often do not carry over to others; ii) metrics based upon system structure often do not reflect behavioural similarity and vice-versa; and iii) increasingly accurate models of a system's structure are not guaranteed to have increasingly accurate behaviours to that of the modelled system. We conjecture that these problems are manifestations of the deeper problem that all of the mathematics underpinning computation takes exact equality as primitive, so approximation is built over an exact meta-theory. However, in a recent breakthrough, Mardare and his collaborators introduced Quantitative Algebra (QA) which generalises one of the central pillars of modern mathematics, namely universal algebra (UA), to allow approximate equations in formal reasoning. The generality of this new idea - replacing classical reasoning with a more refined approximate reasoning in the very fabric of mathematics - gives us a new paradigm which supports a rigorous logical framework for a proper approximation theory, where bounds can be handled, convergences proven and limits approximated.
This project will transform the theory and applications of approximate computation by designing, implementing and deploying a new language for trusted approximate computation. It involves: i) Mathematical Research: We replicate the shift from UA to QA with a similarly revolutionary one from exact computation to approximate computation by developing new quantitative generalisations of the common mathematical structures underpinning exact computation. Approximate computation will then be driven by these new approximate versions of the key structures that drive exact computation. ii) Type Theory & Programming Languages Research: We develop a core dependent type theory incorporating equality-up-to-approximation and type checking to ensure approximation bounds are adhered to; and we convert our type theory into a usable programming language by developing high level features. iii) Applications and Impact Generation: We create case studies in systems biology and digital twins to validate our research and create impact with academic/industrial collaborators who have co-created this proposal. This involves the development of approximate game theory as both these case studies involve autonomous agents that need to make optimal decisions in the presence of uncertainty.

===============================================================================

2022 -- Theory of approximation in experimental biochemical protocols

Collaboration with Prof. Luca Cardelli (Oxford University), project supported by The Royal Society.
Recruitment link - postdoc position
Abstract:
Biochemical laboratories are moving towards more precise and reproduceable experiments via laboratory protocols supported by full automation, and towards higher throughput investigation via automated hypothesis generation supported by data analysis and model inference. To achieve these goals, we need to integrate lab protocols, which define the steps carried out during an experiment, with mathematical models that describe physical processes and guide future experiments. This integration has not yet been achieved to the levels of rigour needed, and in particular it requires accounting for approximations that arise in experimental procedures, and approximations that arise from uncertain knowledge of model parameters. In a recent paper we have proposed a language for modelling and optimizing biological protocols, which has been implemented in the Kaemika chemical simulator app. Significant challenges remain in characterizing the reliability of these formalized protocols in terms of uncertainty in their outcomes, in model refinement driven by data, and in the attribution of fault to either the model or the equipment when an experiment fails. Mardare’s quantitative Barycentric algebra naturally handles the core operation of the proportionate mixing of reagents during experiments, and formally models tolerances in model parameters, equipment operations, and data collection, including handling iterative and recursive protocols and other high-level features necessary for a fully expressive protocol language. We aim to extend our understanding of the interactions between models and protocols, to support a fully automated scientific discovery cycle. The proposed research is interdisciplinary, aiming to apply Logic and Computer Science to Biology and Physics, with concrete foundations in Nanotechnology that helps miniaturize and automate laboratory procedures.

===============================================================================

2020 -- Towards a Non-Standard Semantics for Computational Systems

NPF grant awarded by University of Strathclyde.
Budget - GBP 25,000
Collaborators
Prof. Dana Scott (Carnagie Mellon, USA)
Prof. Gordon Plotkin (Edinburgh)
Prof. Prakash Panangaden (McGill, Canada)
Prof. Dexter Kozen (Cornell, USA)
Dr. Robert Furber (AAU)

===============================================================================

2018 -- AAU Digital Hub Denmark

Fellowship supported by the Danish national program "Strategy for Denmark's Digital Growth" awarded by Digital Hub Denmark.
Budget - DKK 200,000 = GBP 30,000

===============================================================================

2015 -- Approximate Reasoning for Stochastic Markovian Systems

Project 4181-00360 awarded in June 2015 by The Danish Council for Independent Research.
Starting date - August 2015
Budget - DKK 5,574,000 = EUR 750,000
Collaborators
Prof. Kim Larsen (AAU)
Prof. Prakash Panangaden (McGill, Canada)
Prof. Dexter Kozen (Cornell, USA)
Prof. Luca Cardelli (Microsoft Research Cambridge, UK)
Dr. Robert Furber (AAU)

===============================================================================

2010 -- Sapere Aude: DFF-Young Reserchers

Sapere Aude: DFF-Young Researchers Grant awarded in December 2010 by The Danish Council for Independent Research.
Budget - DKK 950,000 = EUR 128,000
Collaborators
Prof. Kim Larsen (AAU)
Dr. Giorgio Bacci (AAU)
Dr. Giovanni Bacci (AAU)
Elite Research Conference 2011 (EliteForsk Konference) ############################################# My link on Sapere Aude EliteForsk website

 

===============================================================================

2010 -- Modular Markovian Logics for Analysis of Stochastic Concurrent Systems

Individual Research Grant (Project 10-085054) awarded in May 2010 by The Danish Council for Independent Research.
Starting date - October 2010
Budget - DKK 1,728,000 = EUR 233,000
Collaborators
Prof. Kim Larsen (AAU),
Prof. Arne Skou (AAU)
Prof. Luca Cardelli (Microsoft Research Cambridge, UK).

Related Tools:
On-the-fly Exact Computation of Bisimilarity Distances.