# crosslang

Monorepo gathering language-implementation projects whose shared shape
makes cross-language theorems possible. Each subdirectory remains a
self-contained Lake package; `common-lean` is the apex that consumes
the other three through Lake path-deps and exposes a typeclass-level
abstraction over them.

## Layout

| Path | Role |
| --- | --- |
| `golang-lean/` | **TGC** — Go subset; big-step over `Heap × Env`. |
| `octive-lean/` | **TOC** — GNU Octave; big-step over `Env`. |
| `tsm-lean/`    | **TSM** — Tiny Stack Machine; small-step, positional operands. Also hosts a source-to-bytecode `Compile/` layer. |
| `common-lean/` | Apex: `BigStepLang` and `SmallStepLang` typeclasses; TGC/TOC/TSM as instances; generic theorems that fire on every instance. |

## Why a monorepo

The three kernels share a `Core/` skeleton (`Syntax · Semantics · Types
· Eval · Determinism · Preservation · TypeSoundness`). Anything *truly*
language-invariant has to be statable in terms common to all three.
Living together in one repo means:

- a generic theorem proved in `common-lean` is a single edit away from
  applying to every kernel,
- new kernels are added by writing a `BigStepLang` (or `SmallStepLang`)
  instance — no path-dep restructuring,
- the factoring is post-hoc: abstractions land only after a third
  concrete point demands them.

## Build

Each package builds independently with `lake build`. The apex:

```sh
cd common-lean && lake build
```

resolves path-deps to the three sibling kernels.

## History

Subprojects were imported with `git subtree add` so per-file `git log`
continues to work across the move.