Cortex

Research wiki

Cortex
Glossary
Map
Style
Taxonomy

01. Quickstart
02. First Wire workflow
03. Running Pulse
04. Deploying Pulse
05. Integrating from Haskell
06. Troubleshooting

01. Overview active
02. Ownership and boundaries active
03. Algebraic foundations active
04. Graph and Circuit active
05. Wire language active
06. Pulse runtime active
07. Rewrites and materialization active
08. Artifacts and provenance active

Wire
Proof status active
Development
Pulse accepted
Rewrites accepted
Cortex Terminology accepted

0001. Structured Document IR superseded
0002. Ownership boundary accepted
0003. Pulse boundary accepted
0004. Graph-native execution accepted
0005. Rewrite admission accepted
0006. Workflow artifact accepted
0007. Conditional lowering accepted
0008. Operator visibility accepted
0009. Graph integrity accepted
0010. Wire authority accepted
0011. Compatibility barriers accepted
0012. Topological memory accepted
0013. Artifact provenance accepted
0014. Model vs external call proposed
0015. Logos archetypes proposed
0016. Cortex roots proposed
0017. Executor and ports proposed
0018. Haskell tree proposed
0019. Executor binding proposed
0020. Pure output equations accepted
0021. Source elaboration proposed
0022. Node clause grammar proposed
0023. CorePure surface proposed
0024. Typed executors proposed
0025. Configured executors proposed
0026. Wire failures proposed
0027. Typed LLM output proposed
0028. Topology composition proposed
0029. CorePure serialization proposed
0030. Node implementation forms proposed
0031. Binding forms and where proposed
0032. Boundary resources proposed
0033. Guarded collapse proposed
0034. Pure select authority proposed
0035. Rewrite forms proposed
0036. Latent branch budget proposed
0037. Latent control proposed
0038. Proof ledger proposed
0039. Node boundary normal form proposed
0040. Logos reasoning surfaces accepted
0041. Wire CLI command proposed
0042. Standard effect executors proposed
0043. Pulse in-memory runner proposed
0044. Namespace use imports proposed
0045. Node-body kinds proposed
0046. Graph forms proposed
0047. Frontier linearity and precedence proposed
0048. Make proposed
0049. Fan phantom adapter proposed
0050. CorePure residue proposed
0051. Source includes proposed
0052. Indexed products proposed
0053. Executor catalog bindings proposed
0054. Wire packages and host bindings proposed

Logos
Portman
Quantum draft
- Reasoning library active

Paper 1 draft
Roadmap active
Paper 2 draft
Paper 3 draft
Paper 4 draft
Paper 6 draft
Publication Notes research
- Deterministic Multi-Rewrite Admission draft
- Ideas
- Causal Programming: Temporal Honesty as a Foundation for Verified Distributed Systems draft

Epics
Plans
Completed
Archive
- Substrate soundness active
- Lean mechanization proposed
- Rewrite materialization proposed

Foundation
Runtime
Wire
Applications
- Topological Memory — Iteration Synthesis

Module Index
Cortex
Cortex.Graph.Core
Cortex.Graph.Laws proofs
Cortex.Graph.Quotient proofs
Cortex.Graph.Relation proofs
Cortex.Graph.Safety proofs
Cortex.Pulse.Classify proofs
Cortex.Pulse.Closure proofs
Cortex.Pulse.DAG proofs
Cortex.Pulse.Fact proofs
Cortex.Pulse.Frontier proofs
Cortex.Pulse.Recovery proofs
Cortex.Pulse.RunSafety proofs
Cortex.Pulse.State proofs
Cortex.Pulse.Validity proofs
Cortex.Wire.ActualizedBridge proofs
Cortex.Wire.Admission proofs
Cortex.Wire.AdmissionArtifact
Cortex.Wire.AdmissionArtifact.Boundary proofs
Cortex.Wire.AdmissionArtifact.Check proofs
Cortex.Wire.AdmissionArtifact.Generated proofs
Cortex.Wire.AdmissionArtifact.GeneratedReconstruction proofs
Cortex.Wire.AdmissionArtifact.Phantom proofs
Cortex.Wire.AdmissionArtifact.PhantomReconstruction proofs
Cortex.Wire.AdmissionArtifact.Primitive proofs
Cortex.Wire.AdmissionArtifact.PrimitiveReconstruction proofs
Cortex.Wire.AdmissionArtifact.PrimitiveTraceCheck proofs
Cortex.Wire.AdmissionArtifact.ReadyGeneral proofs
Cortex.Wire.AdmissionArtifact.ReadyGenerated proofs
Cortex.Wire.AdmissionArtifact.ReadyPhantom proofs
Cortex.Wire.AdmissionArtifact.ReadyPhantomBridge proofs
Cortex.Wire.AdmissionArtifact.ReadyPrimitive
Cortex.Wire.AdmissionArtifact.ReadyPrimitiveRows proofs
Cortex.Wire.AdmissionArtifact.ReadySelect proofs
Cortex.Wire.AdmissionArtifact.ReadySelectBridge proofs
Cortex.Wire.AdmissionArtifact.ReadySummary proofs
Cortex.Wire.AdmissionArtifact.Select proofs
Cortex.Wire.AdmissionArtifact.SelectReconstruction proofs
Cortex.Wire.AdmissionArtifact.Sound proofs
Cortex.Wire.AdmissionArtifact.StaticValue proofs
Cortex.Wire.AdmissionArtifact.Validator
Cortex.Wire.AdmissionArtifact.ValidatorCore proofs
Cortex.Wire.AdmissionArtifact.ValidatorCoreCheck proofs
Cortex.Wire.BoundaryResource proofs
Cortex.Wire.ElaborationIR proofs
Cortex.Wire.FrontierReclaim proofs
Cortex.Wire.GeneratedForms proofs
Cortex.Wire.GraphElaboration proofs
Cortex.Wire.Make proofs
Cortex.Wire.NodeBoundary proofs
Cortex.Wire.PhantomAdapter proofs
Cortex.Wire.Planner proofs
Cortex.Wire.Planner.Chain proofs
Cortex.Wire.Planner.Construction proofs
Cortex.Wire.PortLinearity proofs
Cortex.Wire.PulseSafety proofs
Cortex.Wire.Pure proofs
Cortex.Wire.Registry proofs
Cortex.Wire.Rewrite proofs
Cortex.Wire.RunTrace proofs
Cortex.Wire.Select proofs
Cortex.Wire.SelectAdmission proofs
Cortex.Wire.SelectRecovery proofs

github.com/Digimuoto/cortex

© 2026 Cortex

Publications /Paper 3 Graph Substitution Semantics /Typeset Manuscript

Paper 3 - Graph Substitution Semantics

First-pass Typst PDF rendering of the graph substitution semantics manuscript.

Manuscript Loading PDF…

This page embeds a PDF manuscript. Your browser can't display it inline. Download the PDF or open it in a new tab.