Jeff

• BA hons (first class), Pure Mathematics, Monash University. 

• PhD, Harmonic Analysis, Australian National University.

1976 Monash University sabbatical replacement lecturer. 

1977-1981 UNSW lecturer in Pure Mathematics.

1982-1984 UTS lecturer in the Computing Methods Unit.

1985-2007 Oxford, Programming Research Group, Research Assistant 

        then university lecturer and tutorial fellow at Lady Margaret Hall (now emeritus).

2007-2012 International Institute for Software Technology, United Nations University, Macao, Principal Research Fellow.

2012-2024 African Institute for Mathematical Sciences, South Africa, Academic Director then Resident Senior Researcher.

2024-2027 Zijiang Chair Professor, DISEI, ECNU.

0. Selected publications:

   From over a hundred publications:

• JH Loxton & JW Sanders. On an Inversion Theorem of Mobius. Journal of the Australian Mathematical Society (series A), 30:15–32, 1980.

  The well-known M ̈obius inversion formula from Combinatorics is extended to infinite series and applied to a range of problems in numerical integration. The fundamental result is one of a family studied by Hardy and Littlewood, who simply seem to have missed this result.

• CAR Hoare, He Jifeng & JW Sanders. Prespecification in data refinement. IPL 25(2):71–76, 1987.

  Shows how the method of data representation can be used to derive the specification of a design from its specification using a data representation, entirely in the relational calculus. It is the topic of at least two books (by other authors) and the basis for several more.

• JW Sanders & P Zuliani. Quantum Programming. Mathematics of Pro- gram Construction, ed. JN Oliviera & R Backhouse, Springer LNCS 1837:80– 99, 2000.

  The first presentation of a formal language with laws and semantics for quantum computation; it is used to give a formal derivation of the Deutsch- Josza algorithm.

• Chen Yifeng & JW Sanders. Logic of global synchrony. ACM ToPLaS, 26(2):221–262, 2004.

  One of its referees said this paper could be the paper of the year. It provides, and validates using the bench-mark example of the dining philosophers, a method for deriving reactive programs from their specifications.

• Graeme Smith & JW Sanders. Refining emergent properties. Refine 2009, Electronic Notes in Theoretical Computer Science, 259:207–233, Elsevier, 2009.

                       It is shown how the emergent behaviour of a complex multi-agent system (in this case the glider in Conway’s Game of Life) can be formally 

                       specified and accounted for by top-down incremental refinement, something which has been claimed by several authors to be impossible. 

                       This paper is repre- sentative of work in complex systems.

• CC Morgan, AK McIver, K Seidel & JW Sanders. Refinement-oriented probability for CSP. Formal Aspects of Computing, 8(6):617–647, 1996.

  Provides a denotational model for the process algebra CSP extended to include probability. It reveals the subleties of reasoning about (demonic) nondeterminism and probabilism.

• MN Kamkuemah & JW Sanders. NFT formalised. Submitted, 2024.

  Ownership by Non-FungibleToken, NFT, is peculiar because it confers no rights over the asset. This paper gives a formal specification of NFT and proves that its standard existence on a blockchain implements it.

• Chen Yifeng & JW Sanders. Consciousness of agents in terms of modal logic.

  This series of papers published one or two annually since 2022 considers the consciousness of agents (not necessarily human): as awareness of awareness; in a social setting; by degree; and under evolution.

Professor Sanders’s research involves applying pure mathematics to formalise and reason about computations.

He began with Scott’s work on domain theory then moved to Computer Science and Oxford’s Programming Research Group, 

where he worked on Formal Methods both state-based (Z) and process algebraic (CSP).

Since those days he has shifted with the emphasis of Theoretical Computer Science to: specific distributed systems 

(cryptocurrency & blockchain, and multi-agent systems); specific forms of AI (Machine Learning); and quantum computing.

He currently uses various forms of logic to describe and reason about consciousness of agents and inter-agent trust, 

and is about to embark at ECNU on a new topic: Social Systems, which are agent-based, hierarchical with agents behaving 

differently at different levels in the hierarchy depending on what they believe. It is thus based on doxastic logic and incorporates 

inconsistent reasoning.

• Writing and Communication [Autumn semester 2024] 

• Data Science [Spring semester 2025]

• Quantum Computing [Spring semester 2025]

Staying under the radar of public scrutiny.

0. Competitive grants held:

1. Australian Research Council Travel grants, ×2.

2. Oxford University Oppenheimer Fund, travel grants, ×2.

3. Macao Science and Technology Development Fund: Engineering Accountable Ensembles for 3 years
    (1 postdoc, 1 Phd, 3 fellows, travel and visitors).

4. Macao Science and Technology Development Fund:
    Process Expansion: Action Refinement in the Large for 3 years (1 postdoc, 1 Phd, 3 fellows and equipment).

5. European Union Marie Curie International Postdoctoral Fellowship: 3-year postdoc held by Zuliani (at Princeton and Oxford).

6. U.K. Engineering and Physical Sciences Research Council: Specification and rigorous development of probabilistic systems. GR/J46647, held for 3.5 years (2 postdocs, 1 DPhil and travel).

7. U.K. Engineering and Physical Sciences Research Council:
    A probabilistic formal method.
    Gr/L23260, held for 3.5 years (1 postdoc, 1 DPhil and travel).

         Projects (6) and (7) were evaluated as being 5*, the highest level, by the Engineering and Physical Sciences Research Council.

 U.K. Engineering and Physical Sciences Research Council: 2-year postdoc.

 U.K. Engineering and Physical Sciences Research Council:

funding to support Lengauer’s Oxford visit, travel and accommodation.

Invited international addresses:


       1. Unified Theories of Programming (UTP) 2006.

       2. Relational Methods in Computer Science (RelMiCS) 2006.        

       3. Unified Theories of Programming (UTP) 2010.

       4. Workshop on Mathematical Structures, Stellenbosch, 2013.