Associate Lecturer, The Open University | NEC Member, National Union of Journalists (UK) MSc Cognitive & Decision Sciences (UCL) | MRes Art Theory & Philosophy (UAL)
My research investigates the foundations of computation when systems are organized around transformation equivalence rather than raw value representation. By treating equivalence as identity, we unlock language–store co-designs where data individuation, memory reclamation, and computational continuity survive state transitions and federation boundaries.
-
Foundational Type & Category Theory:
-
Absolute Zero: Polyglot formalization (Coq, Lean 4, Agda, Isabelle, Mizar, Z3) of Certified Null Operations (CNO) and Observational Null Disclosure (OND).
-
Substructural Residues & Tropical Typing: Dependency-free Lean 4 formalization of max-plus resource typing (
$0$ axioms,$0$ sorry), establishing exact dynamic worst-case cost bounds. -
Epistemic & Echo Modalities: Constructive Agda developments formalizing standpoint-indexed warrants, semantic proof transport, and preimage homotopy fibers (
$\Sigma (x : A), f(x) \equiv y$ ).
-
-
Language & Systems Co-Design:
-
Ephapax (ἐφάπαξ): A memory-safe systems language targeting WebAssembly (
wasm32) via dyadic linear/affine modalities and region capabilities—eliminating runtime GC pauses and allocator overhead. Complete 17-crate Rust compiler workspace with 4-layer Coq/Idris2 soundness formalizations. -
Oblíbený & Valence Shell (vsh): A dual-form, Turing-incomplete language and verified shell implementing the Mutually Assured Accountability (MAA) framework, featuring first-class linear echo residues and post-quantum cryptographic primitives.
-
VeriSimDB & VCL-UT: An 8-modal identity-consonance database driven by an 11-level type-safe consonance language.
-
-
Cognitive Interfaces & Public-Interest Governance:
-
PanLL eNSAID: A synchronous 4-pane interface (Ambient, Symbolic, Neural, World) designed to minimize cognitive load in human-AI neurosymbolic collaboration.
-
Solidarity & Accountability Infrastructure: Translating formal verification guarantees into collective social accountability: provable GDPR erasure (RMO), cryptographic provenance, and verifiable AI governance.
-
-
Proof Engineering: Coq (8.18+), Lean 4 (4.13+), Agda (2.6.4+), Idris 2 (0.8.0), Z3 SMT.
-
Systems Programming: Rust (Production workspaces, CLI, WASM codegen), Zig (C-ABI FFI, Zero-copy buffers), OCaml.
-
Reproducibility: GNU Guix reproducible environments, formal FFI boundaries, and strict property-based testing suites.
I am actively open to research collaborations, grants, and high-assurance engineering partnerships at the intersection of formal methods, programming languages, and democratic/collective accountability.
-
Academic & Research: j.d.a.jewell@open.ac.uk
-
ORCID: [0000-0002-3078-6652](https://orcid.org/0000-0002-3078-6652)
-
LinkedIn: [jonathan-jewell](https://www.linkedin.com/in/jonathan-jewell/)
-
Project Specifications & Proof Censuses: Available in repository root
EXPLAINME.adocandSTATUS.adocfiles.