Pick a query, hit Run. The whole evaluator below is F*-extracted OCaml compiled to JavaScript or WebAssembly — no server, no network call. Each card below is a separate dataset with its own query dropdown. For a multi-file, multi-named-graph demo against real Wikidata data, see the life-sciences demo.
People & friendships (~60 triples, Turtle)
PREFIX foaf: <http://xmlns.com/foaf/0.1/>
SELECT ?person ?name ?age
WHERE {
?person a foaf:Person ;
foaf:name ?name ;
foaf:age ?age .
}
ORDER BY ?name
PREFIX foaf: <http://xmlns.com/foaf/0.1/>
SELECT ?name ?age
WHERE {
?p foaf:name ?name ;
foaf:age ?age .
FILTER (?age > 30)
}
ORDER BY DESC(?age)
PREFIX foaf: <http://xmlns.com/foaf/0.1/>
SELECT ?name ?mbox
WHERE {
?p foaf:name ?name .
OPTIONAL { ?p foaf:mbox ?mbox }
}
ORDER BY ?name
PREFIX foaf: <http://xmlns.com/foaf/0.1/>
PREFIX ex: <http://example.org/>
SELECT ?friend ?friendName
WHERE {
ex:alice foaf:knows ?friend .
?friend foaf:name ?friendName .
}
ORDER BY ?friendName
PREFIX foaf: <http://xmlns.com/foaf/0.1/>
SELECT DISTINCT ?a ?b
WHERE {
?a foaf:knows ?b .
?b foaf:knows ?a .
FILTER (STR(?a) < STR(?b))
}
ORDER BY ?a ?b
PREFIX foaf: <http://xmlns.com/foaf/0.1/>
SELECT ?name (COUNT(?friend) AS ?nFriends)
WHERE {
?p foaf:name ?name ;
foaf:knows ?friend .
}
GROUP BY ?p ?name
ORDER BY DESC(?nFriends)
PREFIX foaf: <http://xmlns.com/foaf/0.1/>
PREFIX ex: <http://example.org/>
ASK {
ex:alice foaf:knows ?mid .
?mid foaf:knows ex:eve .
}
PREFIX foaf: <http://xmlns.com/foaf/0.1/>
SELECT ?name
WHERE {
?p foaf:name ?name .
FILTER (LANG(?name) = "de")
}
PREFIX foaf: <http://xmlns.com/foaf/0.1/>
SELECT ?name ?upper ?initial
WHERE {
?p foaf:name ?name .
BIND (UCASE(STR(?name)) AS ?upper)
BIND (SUBSTR(STR(?name),1,1) AS ?initial)
}
ORDER BY ?name
Product catalogue (~80 triples, Turtle)
PREFIX sch: <http://schema.org/>
PREFIX ex: <http://example.org/>
SELECT ?name ?category ?price
WHERE {
?p sch:name ?name ;
sch:category ?category ;
ex:price ?price .
}
ORDER BY DESC(?price)
PREFIX sch: <http://schema.org/>
PREFIX ex: <http://example.org/>
SELECT ?category (COUNT(?p) AS ?n) (AVG(?price) AS ?avgPrice)
WHERE {
?p sch:category ?category ;
ex:price ?price .
}
GROUP BY ?category
ORDER BY DESC(?n)
PREFIX sch: <http://schema.org/>
PREFIX ex: <http://example.org/>
SELECT ?name ?category
WHERE {
?p sch:name ?name ;
sch:category ?category ;
ex:stock 0 .
}
ORDER BY ?category ?name
PREFIX sch: <http://schema.org/>
PREFIX ex: <http://example.org/>
SELECT ?category (MAX(?price) AS ?topPrice)
WHERE {
?p sch:category ?category ;
ex:price ?price .
}
GROUP BY ?category
HAVING (MAX(?price) > 50)
ORDER BY DESC(?topPrice)
Music — bands, members, albums (~70 triples, Turtle)
PREFIX ex: <http://example.org/music/>
PREFIX dc: <http://purl.org/dc/terms/>
SELECT ?album ?year ?band
WHERE {
?a a <http://purl.org/ontology/mo/Album> ;
dc:title ?album ;
ex:year ?year ;
ex:by ?b .
?b dc:title ?band .
}
ORDER BY ?year
PREFIX ex: <http://example.org/music/>
PREFIX dc: <http://purl.org/dc/terms/>
SELECT ?band (COUNT(?m) AS ?nMembers)
WHERE {
?g a <http://purl.org/ontology/mo/MusicGroup> ;
dc:title ?band ;
ex:member ?m .
}
GROUP BY ?g ?band
ORDER BY DESC(?nMembers)
PREFIX ex: <http://example.org/music/>
PREFIX dc: <http://purl.org/dc/terms/>
SELECT ?band (GROUP_CONCAT(?album; SEPARATOR=", ") AS ?albums)
WHERE {
?a a <http://purl.org/ontology/mo/Album> ;
dc:title ?album ;
ex:by ?b .
?b dc:title ?band .
}
GROUP BY ?b ?band
ORDER BY ?band
PREFIX ex: <http://example.org/music/>
PREFIX dc: <http://purl.org/dc/terms/>
SELECT ?album ?year
WHERE {
?a dc:title ?album ;
ex:year ?year .
FILTER (?year >= 1970 && ?year < 1980)
}
ORDER BY ?year
PREFIX ex: <http://example.org/music/>
PREFIX dc: <http://purl.org/dc/terms/>
# Compound property path: album -> band (ex:by) -> musician (ex:member).
# "?a ex:by/ex:member ?m" reads as one property path that walks two
# edges without an intermediate variable for the band. The engine
# does the join for you.
SELECT ?album ?musician
WHERE {
?a a <http://purl.org/ontology/mo/Album> ;
dc:title ?album ;
ex:by/ex:member ?m .
?m dc:title ?musician .
}
ORDER BY ?album ?musician
PREFIX ex: <http://example.org/music/>
PREFIX dc: <http://purl.org/dc/terms/>
# "^ex:member" is the inverse path (band-of-this-musician), then
# "/ex:member" forward again gets all members of that band. The
# result is everyone who shares a band with Thom, Thom included —
# FILTER strips him out.
SELECT ?colleague
WHERE {
ex:thom ^ex:member/ex:member ?m .
?m dc:title ?colleague .
FILTER (?m != ex:thom)
}
ORDER BY ?colleague
Places, countries, populations (~50 triples, Turtle)
PREFIX ex: <http://example.org/geo/>
PREFIX rdfs: <http://www.w3.org/2000/01/rdf-schema#>
SELECT ?country ?capital ?population
WHERE {
?c a ex:Country ;
rdfs:label ?country ;
ex:capital ?cap ;
ex:population ?population .
?cap rdfs:label ?capital .
}
ORDER BY DESC(?population)
PREFIX ex: <http://example.org/geo/>
PREFIX rdfs: <http://www.w3.org/2000/01/rdf-schema#>
SELECT ?continent (SUM(?pop) AS ?total)
WHERE {
?c a ex:Country ;
ex:inContinent ?k ;
ex:population ?pop .
?k rdfs:label ?continent .
}
GROUP BY ?k ?continent
ORDER BY DESC(?total)
PREFIX ex: <http://example.org/geo/>
PREFIX rdfs: <http://www.w3.org/2000/01/rdf-schema#>
SELECT ?country ?capital
WHERE {
?c a ex:Country ;
rdfs:label ?country ;
ex:inContinent ex:europe ;
ex:population ?pop ;
ex:capital ?cap .
?cap rdfs:label ?capital .
FILTER (?pop > 50000000)
}
ORDER BY ?country
Named graphs — three libraries (~45 quads, TriG)
PREFIX ex: <http://example.org/lib/>
PREFIX schema: <http://schema.org/>
SELECT ?library ?book ?title
WHERE {
GRAPH ?library {
?book a schema:Book ; schema:name ?title .
}
}
ORDER BY ?library ?title
PREFIX ex: <http://example.org/lib/>
PREFIX schema: <http://schema.org/>
SELECT ?title (COUNT(DISTINCT ?g) AS ?nCopies)
WHERE {
GRAPH ?g { ?b a schema:Book ; schema:name ?title }
}
GROUP BY ?title
HAVING (COUNT(DISTINCT ?g) > 1)
ORDER BY DESC(?nCopies) ?title
PREFIX dc: <http://purl.org/dc/terms/>
PREFIX ex: <http://example.org/lib/>
SELECT ?library ?name
WHERE {
?library dc:title ?name .
}
ORDER BY ?library
PREFIX ex: <http://example.org/lib/>
PREFIX schema: <http://schema.org/>
SELECT ?title ?author
WHERE {
GRAPH ex:central { ?b schema:name ?title ; schema:author ?author }
}
ORDER BY ?title
schema.org class hierarchy (entailment demo, Turtle)
The Logic: radio in the toolbar (None / RDFS /
OWL-RL) switches entailment regime per run. Try "None" then
"RDFS" on the "All Places" query to see sub-class inference
kick in.
PREFIX schema: <http://schema.org/>
SELECT ?s ?name
WHERE {
?s a schema:Place ;
schema:name ?name .
}
ORDER BY ?name
PREFIX rdfs: <http://www.w3.org/2000/01/rdf-schema#>
PREFIX schema: <http://schema.org/>
# Classic SPARQL 1.1 pattern: "a/rdfs:subClassOf*" reads as
# "rdf:type, then zero or more subClassOf hops". This finds every
# instance that transitively is-a schema:Place without turning on
# RDFS entailment at all — the engine walks the class chain on
# the fly per the property path. Contrast with "?s a schema:Place"
# (needs RDFS entailment to find hotels).
SELECT ?instance ?name
WHERE {
?instance a/rdfs:subClassOf* schema:Place ;
schema:name ?name .
}
ORDER BY ?name
PREFIX schema: <http://schema.org/>
SELECT ?s ?name
WHERE {
?s a schema:LodgingBusiness ;
schema:name ?name .
}
ORDER BY ?name
PREFIX schema: <http://schema.org/>
SELECT ?s ?name
WHERE {
?s a schema:Restaurant ;
schema:name ?name .
}
ORDER BY ?name
PREFIX schema: <http://schema.org/>
# schema:legalName rdfs:subPropertyOf schema:name, so with RDFS on
# ex:hotelZ (which only has a legalName) shows up here too.
SELECT ?s ?name
WHERE {
?s schema:name ?name .
}
ORDER BY ?s
PREFIX schema: <http://schema.org/>
# The data only has ex:downtown schema:containsPlace ?x, so without
# OWL-RL this returns nothing. With OWL-RL, prp-inv1 flips the arrow.
SELECT ?sub ?container
WHERE {
?sub schema:containedInPlace ?container .
}
ORDER BY ?sub
PREFIX schema: <http://schema.org/>
# ex:hotelZincLLC owl:sameAs ex:hotelZ, and both carry name triples.
# With OWL-RL, eq-rep-s collapses them so ex:hotelZ has both names.
SELECT ?s ?name
WHERE {
?s a schema:Hotel ; schema:name ?name .
}
ORDER BY ?s ?name
What is Factoidal?
Factoidal is an RDF 1.1 and SPARQL 1.1 implementation where the specification is the product. The semantics are written in F*, a dependently-typed language with an SMT solver. The executable code you're running was obtained by extraction — not hand-written to "mirror" the spec.
What can it do?
Query any RDF data in Turtle, N-Triples, N-Quads, TriG, or RDF/XML. Supports the standard SPARQL 1.1 query language: SELECT, ASK, CONSTRUCT, FILTER, OPTIONAL, UNION, MINUS, BIND, VALUES, EXISTS/NOT EXISTS, DISTINCT, ORDER BY, LIMIT, OFFSET, GROUP BY, HAVING, aggregates (COUNT, SUM, AVG, MIN, MAX, GROUP_CONCAT, SAMPLE), subqueries, property paths, and 30+ built-in functions.
How close is it to a reference implementation?
Against the W3C conformance test suites (2026-04-25; live results): SPARQL 1.1 ~622 pass / ~5 fail across SELECT/ASK/CONSTRUCT, full UPDATE grammar (INSERT DATA / DELETE DATA / DELETE WHERE / DELETE-INSERT WHERE, plus CLEAR/DROP/CREATE/ADD/MOVE/COPY graph management), federated SERVICE (in-process), LOAD SILENT, SPARQL Protocol (in-process), Graph Store HTTP Protocol (in-process), service description, and a verified property-path engine; RDF 1.1 1031/1031 parser tests pass across N-Triples, Turtle, N-Quads, TriG, RDF/XML, plus the rdf-mt model-theory suite. Entailment: RDFS + OWL 2 RL Datalog (13/30 PositiveEntailmentTests, the remaining 17 require negation-as-failure / contrapositive reasoning that OWL-RL cannot derive monotonically). RDF Dataset Canonicalization 1.0 (RDFC-1.0) is wired with HFDQ + 2-level neighbour-hash, F*-verified clean. Remaining headline gaps: 3 entailment tests under SPARQL-DL tableau (paper-Q3, parent4, parent7), 1 GSP test that requires Turtle-body parsing for mismatched-payload detection.
Why does it exist?
The intent is to have a SPARQL evaluator whose correctness argument is mechanically checked rather than "we wrote lots of tests". Each W3C test that passes is one more sanity check on the F* spec; the proofs are what justify the implementation.
Source on GitHub →
Build pipeline
F* .fst ──fstar.exe --codegen OCaml──► ocaml-output/*.ml
│
├──ocamlfind ocamlc──► bin/<platform>/factoidal (native)
│
├──js_of_ocaml──────► docs/fstar-extracted/factoidal.js
│
└──wasm_of_ocaml────► docs/fstar-extracted/w3c-runner.wasm.{js,assets/}
See formal/fstar/build-ocaml.sh for the exact invocation. The demo above is driven by the js_of_ocaml output — the bytecode runs under js_of_ocaml's runtime, which provides an in-memory fake filesystem (MlFakeDevice) so the OCaml code can "open" files that only exist as JavaScript strings.
Browser artifacts
factoidal.js — SPARQL + RDF parsing CLI, js_of_ocaml. What the demo above loads. Works in any modern browser or Node. The demo runs it with -o json and renders the SPARQL Results JSON as an HTML table.
w3c-runner.js — the W3C conformance runner, js_of_ocaml. Same engine as factoidal; run it from Node with node w3c-runner.js bind.
w3c-runner.wasm.js (loader) + w3c-runner.wasm.assets/ — WebAssembly build via wasm_of_ocaml. 400 KB .wasm + 45 KB loader. Needs Wasm-GC (Chrome ≥ 119, Node ≥ 22; Firefox not yet). Node CLI only — no browser UI wired up to it yet.
factoidal.wasm.js (loader) + factoidal.wasm.assets/ — WebAssembly build of the query CLI. 372 KB .wasm + 38 KB loader. Smoke-tested under Node (node factoidal.wasm.js -d data.ttl -e 'SELECT * WHERE { ?s ?p ?o }' -o json). The demo above still uses factoidal.js (js_of_ocaml, synchronous) — a JS/wasm toggle is queued; the wasm loader is async and needs a small handler refactor.
Wasm coverage vs native
Per-suite totals match the native runner almost everywhere. One crash (functions, SHA/digestif C primitives with no proper wasm binding yet) and an unexplained 4-test gap in property-path.
| Suite | native | wasm |
|---|
| bind / bindings / exists / grouping / project-expression / csv-tsv-res / json-res / syntax-fed / syntax-query / aggregates / subquery / negation / construct / delete-insert / entailment / cast | identical | identical |
| property-path | 33/33 | 29/33 |
| functions | 74/75 | crash |
Vendored wasm runtime (zarith)
wasm_of_ocaml emits throwing stubs for any external C primitive it can't link. fstar.lib transitively pulls in zarith, stdint, sha, and digestif — about 150 such primitives. js_of_ocaml's JS stubs don't auto-link under wasm_of_ocaml: you need a companion .wat that imports JS functions and re-exports them under OCaml-facing names. zarith_stubs_js v0.17+ ships exactly that, so we vendor its runtime.wat + runtime_wasm.js under formal/fstar/ocaml-output/wasm_runtime/ (the installed opam zarith_stubs_js v0.16.1 predates the wasm files).
The remaining stdint/sha/digestif primitives get identity pass-through shims from wasm_stub_shims.py. See js_of_ocaml#2190 if your distro's binaryen package is missing wasm-merge.
Running the CLI from Node
git clone --recurse-submodules https://github.com/danbri/factoidal.git
cd factoidal/docs/fstar-extracted
# SPARQL CLI:
node factoidal.js -d data.ttl -e 'SELECT * WHERE { ?s ?p ?o }' -o json
# W3C conformance runner (Node):
node w3c-runner.js bind
node w3c-runner.wasm.js bind
Known browser limitations
The demo's engine is js_of_ocaml (pure JavaScript). The wasm build
is not yet plugged into the UI — it's a Node CLI only. Hash built-ins
(MD5, SHA1, SHA256, SHA384,
SHA512) use Node's crypto module under
Node but return empty strings in the browser. Everything else runs
identically.