A collection of maintained, runnable RDF/SPARQL notebooks. Each post
shows a real Factoidal capability rather than a screenshot: parse and
query RDF, follow property paths, validate data, transform it, or
inspect a storage experiment.
The RDF/JS API — DataFactory, Quad terms, .equals() vs === (foaf)
The API tour — npm/factoidal's full function surface + a live capabilities probe (foaf)
Verifiable Credentials and CSVW — VC structural validation + eddsa-rdfc-2022 Data Integrity signatures (Ed25519/SHA-256 via HACL*, browser + Node via wasm) + CSVW csv2rdf live (schema.org)
How fast: the performance story — dated, commit-linked throughput and on-disk reader numbers, one live in-browser timing illustration (wikidata)
The verified-in-F* story — why F*, the standing verification qualifier, the skimmable RDF.Term.fsti core, one source to four extraction targets
The durable log, live: update, persist, reload, corrupt — the full durable-UPDATE lifecycle running in your browser via IndexedDB across a real page reload, a live checksum-rejection demo, and the same delta-log module proven running natively, as KaRaMeL C, and as wasm (foaf)
Correlated joins: LATERAL — LATERAL evaluates its right side once per left row with that row's bindings substituted in, making top-N-per-group expressible (SPARQL 1.2-track / Jena-compatible)
Full-text search: text:query — the jena-text magic predicate that searches literals instead of matching triples, conjunctive token matching, no relevance ranking
GeoSPARQL: geometry, topology, and exact-rational arithmetic — geo:wktLiteral geometries and the geof: Simple Features predicates (sfWithin/sfIntersects/sfDisjoint/sfTouches), geof:distance and geof:envelope, with a point-exactly-on-a-polygon-edge case decided by pure exact-rational F* — no floating-point epsilon (geosparql)
Reaching out to other data: the SPARQL client, SERVICE tool-wrapping, and virtual RML — answering SPARQL over data factoidal doesn't hold locally, three ways: query --endpoint against a remote SPARQL 1.1 Protocol server, SERVICE <wrap+http://...> triplifying a REST/CSV/Turtle source (SPARQL-Anything-adjacent), and --data-rml answering through an RML mapping non-materialized (D2RQ/Ontop-style pushdown). A CLI-transcript-and-architecture page — network/native features, no live cell (none)
Decentralized Identifiers: did:key — resolving a did:key:z6Mk… Ed25519 identifier to its DID Document as pure, offline, F*-verified function application, rendered live as triples and a node-graph (did)
HDT: querying a compressed binary RDF file — SPARQL run straight over the RML-Core ontology's Header-Dictionary-Triples binary via --data-hdt, with a live triple count, class table, and predicate histogram; no prior decompression to text (hdt)
XML well-formedness and XPath — the generic F* XML parser deciding well-formed vs malformed live, plus XPath 1.0 evaluation returning node-sets, strings, numbers, and booleans over a sample document (xml)
Reactive cells: declare once, use everywhere — the hub's cells reference each other ObservableHQ-style: ttl = `…` in one cell, graph = parse(ttl) in the next, then a query, then a chart, each its own cell; the vendored runtime orders them by dependency and re-runs dependents on edit (foaf)
Transforming and checking XML: XSLT and Schematron — an XSLT 1.0 stylesheet reshaping a document with xsl:for-each/xsl:value-of, and a Schematron rule firing on a document that violates it and clearing on one that doesn't (none)
Verified math, rendered: MathML, TOAN, and linear algebra — MathML evaluation to an exact rational (and a clean undef on division by zero, never NaN), an exact-arithmetic CAS emitting Content MathML for a summation with a small honest Content-to-Presentation converter so the browser can typeset it, and matrix determinants over exact rationals including a fractional result (none)
Validating data: JSON Schema and XForms recalculation — a draft-07 JSON Schema accepting one instance and rejecting another missing a required property, and an XForms bind's calculate MIP deriving one leaf from two others on a live recalculation pass (none)
OWL reasoning by model construction: the tableau — a model-construction reasoner classifying individuals into owl:someValuesFrom and owl:hasValue class expressions the Datalog closure cannot reach, an unsatisfiable ∃hasChild.owl:Nothing restriction caught as a DL inconsistency RL leaves consistent, a clash-detecting refutation sibling (Tableau.Refute, 2026-07-10) scoring the W3C inconsistency catalogs, and a measured account of what the tableau does not cover (none)
RDF 1.2: triple terms, reifiers & directional text — statements as first-class terms (<<( s p o )>>) parsed live from Turtle 1.2, queried with SPARQL 1.2 triple-term patterns and the isTRIPLE/TRIPLE builtins, plus ~ reifier + {| |} annotation provenance and directional literals — with an honest account of what 1.2 still lacks (none)
This answer is a theorem: the certified core-RDFS closure — SPARQL answers over the six-rule core-RDFS (ρdf) closure are machine-checked equivalent to entailment; run the certified engine live and watch the checker refuse false claims (none)
Correlated federation: LATERAL meets SERVICE — SERVICE endpoints bound to local graph snapshots, then driven one row at a time by LATERAL: per-row remote lookups, per-row endpoint SELECTION with SERVICE ?endpoint proved by deliberately conflicting endpoint data, and SILENT's keep-the-row semantics (none)
Extension functions: your code inside the verified engine — SPARQL 1.1 §17.6 custom functions registered by IRI (the Comunica model): sync and async JavaScript bodies, a WebAssembly-bodied function, and a function whose body is itself F*-verified (Math.Sigmoid.fst), with a precise account of which links in that pipeline are proved (none)
Wikifunctions inside the query: two F* engines, one SPARQL seam — real Wikifunctions (the wikifn-fstar corpus, translated to F*, checked, extracted to JavaScript) registered as §17.6 extension functions by ZID: palindrome canals via Z10052∘Z10096, ROT13, an honest compiled-vs-interpreter distinction, and what it would take to make two proofs into one (none)
Installed, not vendored — loads the actual @factoidal/core@0.1.0 package published to npmjs.com, live, from a public CDN that serves npm packages verbatim, and cross-checks it against this site's own same-origin copy: version comparison, parse/SELECT/ASK/canonicalize/extension-function calls run through the fetched registry module, and a row-for-row agreement check against the same-origin engine — this post's CSP alone allows the two npm CDN hosts (none)
Lean 4 in the browser: a second engine on the page — the Lean 4 port compiled Lean → C → wasm32 (Lean's runtime and core library rebuilt for the target, GMP-free, one module for browser + Node + Deno) parsing the same Turtle text and answering the same SPARQL SELECT and typed-literal ASK as the F*-derived engine, with the row-set agreement computed on the page (none)
One triple at a time — the Lean 4 engine's dispatch surface climbed step by step through fn.l4Call: parse one N-Triples line, ASK, SELECT, a join, Turtle in with byte-identical N-Quads out, INSERT DATA, CONSTRUCT, RDFS and OWL-RL closures queried live, RDFC-1.0 canonicalization deciding graph sameness — and the F* engine answering the final join over the same bytes, the agreement computed on the page (none)
A dataset that stays open — the Lean 4 engine's dataset-handle graph API worked as one session: fn.l4Parse opens a three-department TriG corpus into one handle, a GRAPH ?g query joins across the named graphs, fn.l4Update mutates the same handle in place with no re-parse, rdfsPlusClosure derives a triple from the handle's own serialized data, and owlIsConsistent's three-valued verdict flips from consistent to inconsistent — with a reason — once a disjoint-class pair is inserted (none)
A walkthrough of the IKL GUIDE — worked examples straight from Pat Hayes and Chris Menzel's IKL GUIDE, parsed live section by section: ground predication, restricted quantifier binders, proposition names and the cancelling-parentheses assertion form, quantifying-in, and the GUIDE's own stated =p boundary on propositional identity — with the reader's fragment limits stated where a GUIDE example goes beyond them (none)
COTTAS: a store, not just a format — a 4,000-triple, four-graph corpus loaded into the browser's in-memory COTTAS bytes store and queried three ways (point lookup, star join, cross-graph GRAPH join), each timed against the same queries over a plain parsed dataset — store answers in milliseconds where the re-parsing path takes hundreds, rows equal in both, part of the persistence program (none)
One model theory under all of it — the LBase programme of 2003 carried out in Lean 4 and proved instead of sketched: RDF, RDFS, ρdf, OWL 2 RL, OWL 2 DL and SPARQL BGPs translated into one Common Logic/IKL interpretation with per-language axiom schemas, each stage's adequacy against the native formalization stated at its exact strength — with the ρdf closure, Finding C-1's separating pair and an OWL 2 RL row computed live next to the theorems that cover them, and the defects the proof attempts found in shipping code (issue 598) (none)
A little IKL walkthrough — one squirrel story written down twice in short question-and-answer steps: a witness’s words held as a CLIF quoted string, the rule that (that S) is a term and cannot be that’s own argument, three-layer that-nesting through a predication, factivity as an axiom you write rather than one the logic assumes, quantifying into a that-term — and, because IKL is referentially transparent, a misunderstanding that has to be stated about the string rather than inside a belief (none)
Life sciences: named graphs, on demand — the established 43,103-triple Wikidata/KGX browser workload recast as a click-to-run named-graph notebook, retaining its chromosome/sequence-variant cross-graph join without making every documentation visit parse the corpus (wikidata)
Bring a block: browser artifact inspection — choose an IBK1 block, inspect its versioned header, calculate SHA-256, and optionally cache the exact bytes in OPFS; browser-side block query execution is named as the pending Lean-WASM ABI increment, not implied (none)
Writing Hub notebooks — the Observable-style cell model, Factoidal's browser API, and the pinned-test contract (none)
JSON-LD playground — paste JSON-LD and inspect RDF plus canonical N-Quads locally in the browser (schema.org)
AI beside a local knowledge graph — an optional browser-AI proposal over the life-sciences graph profile: check availability, ask a question, inspect read-only SPARQL, then choose whether to run it in Shardborough (sparql)
Shardborough: compose a local graph neighbourhood — query 43,103 Wikidata life-sciences triples from twelve committed IBK3 blocks: each query fetches only the predicate blocks it names, verifies their SHA-256, decodes them with the Lean WebAssembly block worker, and runs cross-graph SPARQL in the browser (wikidata)
Three blocks, one SPARQL query — fetch three current IBK3 artifacts, verify their published identities, inspect their actual byte layout, then run either an editable join or a query over all 13 decoded triples through the Lean WebAssembly runtime (sparql)
The persisted store on your laptop: what a query costs — recorded 2026-09-02: 888,949 and 1,290,077 Wikidata life-sciences triples packed into IBK3 generations and queried through the Lean native harness in under a second per query, with the theorems and checks each number rests on
A store in a bucket: SPARQL over plain HTTP — open a Shardborough generation that lives in an object store, ask the engine which artifacts a query needs, fetch only those, check their digests and answer in the browser: nine SKOS query shapes with the keys, the bytes and the time each one costs (skos)
XMPP, verified: JIDs, stream negotiation, and stanzas — the start of a fresh, GC3-targeting XMPP implementation in Lean 4: RFC 7622 JID parsing, RFC 6120 stream negotiation with a proved TLS-then-SASL-then-bind ordering, and stanza parsing, tested against a live ejabberd instance and reusing the existing XML parser rather than duplicating it (none)
See also: the performance hub — measured
runtime-vs-runtime comparisons across the four extraction targets
(native OCaml, js_of_ocaml, wasm_of_ocaml, KaRaMeL C), including the
C-to-wasm question.