Commit graph

  • 4bf2dd38cd Add 'common-lean/' from commit 'a0b719e170f66a736093d0d1c51b9d5883471db2' master Maximus Gorog 2026-05-12 02:59:14 -06:00
  • bd2e14214d Add 'tsm-lean/' from commit '2e9061abead6f2daa464b39a79c17a949db30785' Maximus Gorog 2026-05-12 02:59:14 -06:00
  • 6592cd058d Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' Maximus Gorog 2026-05-12 02:59:14 -06:00
  • fd3d42ae33 Add 'golang-lean/' from commit 'f5f17019224c6a6c319387214ceb8e29d09251c6' Maximus Gorog 2026-05-12 02:59:14 -06:00
  • 6487c7046f Initial commit: crosslang monorepo skeleton. Maximus Gorog 2026-05-12 02:59:08 -06:00
  • 4b6fcec565 Add SymPy bridge and migrate DSL to brace-block syntax. Maximus Gorog 2026-05-12 02:58:50 -06:00
  • a0b719e170 Initial commit: Common — cross-language abstraction over TGC, TOC, TSM. Maximus Gorog 2026-05-10 06:52:25 -06:00
  • f5f1701922 Add RosettaStone.lean — Go ↔ Lean translation reference. Maximus Gorog 2026-05-10 06:49:22 -06:00
  • 2e9061abea Refactor compile to be offset-aware (v0.4). Maximus Gorog 2026-05-10 06:12:03 -06:00
  • f9ed9ec4c7 Extend compiler with bool literals + sub + mul (v0.3). Maximus Gorog 2026-05-10 06:01:44 -06:00
  • ec65229050 Extend source-to-TSM compiler with addition (v0.2). Maximus Gorog 2026-05-10 05:53:39 -06:00
  • fff0091f89 Add source-to-TSM compiler with proven correctness (v0.1). Maximus Gorog 2026-05-10 05:38:01 -06:00
  • 987f205ce5 Initial commit: Tiny Stack Machine (TSM) in Lean 4. Maximus Gorog 2026-05-10 05:12:10 -06:00
  • d86d500b4f Prove preservation theorem for TOC big-step semantics. Maximus Gorog 2026-05-10 04:32:52 -06:00
  • 567d3d1902 Add Tiny Octave Core (TOC) parallel to golang-lean's TGC. Maximus Gorog 2026-05-10 04:26:12 -06:00
  • ed636a1aa2 Prove preservation theorem for TGC big-step semantics. Maximus Gorog 2026-05-10 04:05:08 -06:00
  • 3174918193 Add executable evaluator (Phase A) and type system + soundness infra (Phase B). Maximus Gorog 2026-05-10 03:51:14 -06:00
  • 878a84e072 Add Tiny Go Core (TGC): kernel calculus with proven determinism. Maximus Gorog 2026-05-10 02:23:58 -06:00
  • 2173e196fe Initial scaffold: Lean 4 reimplementation of Go. Maximus Gorog 2026-05-10 02:12:19 -06:00
  • 23162fb93a Add README, CONTRIBUTING, editorconfig, gitattributes, justfile Maximus Gorog 2026-04-29 09:44:24 -06:00
  • db79eb3fde Initial commit: Lean 4 reimplementation of GNU Octave Maximus Gorog 2026-04-29 09:40:46 -06:00