https://github.com/engboris/transcendental-syntax Skip to content Navigation Menu Toggle navigation Sign in * Product + GitHub Copilot Write better code with AI + Security Find and fix vulnerabilities + Actions Automate any workflow + Codespaces Instant dev environments + Issues Plan and track work + Code Review Manage code changes + Discussions Collaborate outside of code + Code Search Find more, search less Explore + All features + Documentation + GitHub Skills + Blog * Solutions By company size + Enterprises + Small and medium teams + Startups By use case + DevSecOps + DevOps + CI/CD + View all use cases By industry + Healthcare + Financial services + Manufacturing + Government + View all industries View all solutions * Resources Topics + AI + DevOps + Security + Software Development + View all Explore + Learning Pathways + White papers, Ebooks, Webinars + Customer Stories + Partners + Executive Insights * Open Source + GitHub Sponsors Fund open source developers + The ReadME Project GitHub community articles Repositories + Topics + Trending + Collections * Enterprise + Enterprise platform AI-powered developer platform Available add-ons + Advanced Security Enterprise-grade security features + GitHub Copilot Enterprise-grade AI features + Premium Support Enterprise-grade 24/7 support * Pricing Search or jump to... Search code, repositories, users, issues, pull requests... Search [ ] Clear Search syntax tips Provide feedback We read every piece of feedback, and take your input very seriously. [ ] [ ] Include my email address so I can be contacted Cancel Submit feedback Saved searches Use saved searches to filter your results more quickly Name [ ] Query [ ] To see all available qualifiers, see our documentation. Cancel Create saved search Sign in Sign up Reseting focus You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session. Dismiss alert {{ message }} engboris / transcendental-syntax Public * Notifications You must be signed in to change notification settings * Fork 4 * Star 42 Technical (but still naive) interpretation of Girard's transcendental syntax tsguide.refl.fr/ License GPL-3.0 license 42 stars 4 forks Branches Tags Activity Star Notifications You must be signed in to change notification settings * Code * Issues 17 * Pull requests 0 * Actions * Projects 0 * Security * Insights Additional navigation options * Code * Issues * Pull requests * Actions * Projects * Security * Insights engboris/transcendental-syntax master BranchesTags [ ] Go to file Code Folders and files Name Name Last commit message Last commit date Latest commit History 105 Commits bin bin examples examples guide guide src src test test .gitignore .gitignore LICENSE LICENSE README.md README.md dune-project dune-project tsyntax.opam tsyntax.opam View all files Repository files navigation * README * GPL-3.0 license Transcendental Syntax The transcendental syntax is a method of constructing logical abstractions from a low-level elementary and "logic-agnostic" language. This elementary language we use to build abstractions is called "stellar resolution" and its elementary objects corresponding to programs are called "constellations". Those constellations are used in a higher-level language called "Stellogen" in which notions such as proofs and formulas are defined (this is basically a metaprogramming language for constellations). By the proof-as-program correspondence, this can be extended to programs and types. Stellar resolution The stellar resolution (RS) is a model of computation introduced by Jean-Yves Girard [1] in his transcendental syntax project as a basis for the study of the computational foundations of logic. It has been mainly developed by Eng later in his PhD thesis [2]. It can be understood from several points of view: * it is a logic-agnostic, asynchronous and very general version of Robinson's first-order resolution with disjunctive clauses, which is used in logic programming; * it is a very elementary logic-agnostic constraint programming language; * it is a non-planar generalization of Wang tiles (or LEGO bricks) using terms instead of colours and term unification instead of colour matching; * it is a model of interactive agents behaving like molecules which interact with each other. It can be seen as a generalization of Jonoska's flexible tiles used in DNA computing; * it is an assembly language for meaning. Stellar resolution is very elementary and an interpreter for it can be written in a very concise way since it mostly relies on a unification algorithm. Learn This project is still in development, hence the syntax and features are still changing. Go to https://tsguide.refl.fr/ (guide currently in French only) to learn more about how to play with the current implementation of transcendental syntax. Use You can either download a released binary (or ask for a binary) or build the program from sources. Build from sources Install opam and OCaml from opam : https://ocaml.org/docs/ installing-ocaml Install dune: opam install dune Install dependencies opam install . --deps-only Build the project dune build Executables are in _build/default/bin/. Commands Assume the executable is named sgen.exe. Interpreter Stellogen programs with: ./sgen.exe or if you use Dune: dune exec sgen -- Examples Some example files with the .sg extension in /examples are ready to be executed. In Eng's thesis, ways to work with other models of computation are described (Turing machines, pushdown automata, transducers, alternating automata etc). References * [1] Transcendental syntax I: deterministic case, Jean-Yves Girard. * [2] An exegesis of transcendental syntax, Boris Eng. * [3] Term Rewriting and All That, Franz Baader & Tobias Nipkow. About Technical (but still naive) interpretation of Girard's transcendental syntax tsguide.refl.fr/ Topics logic verification reactive-programming proof-assistant formal-methods logic-programming object-oriented-programming transcendental-syntax Resources Readme License GPL-3.0 license Activity Stars 42 stars Watchers 4 watching Forks 4 forks Report repository Releases 6 tags Packages 0 No packages published Contributors 2 * @engboris engboris Boris Eng * @Champitoad Champitoad Pablo Donato Languages * OCaml 97.5% * Dune 2.5% Footer (c) 2025 GitHub, Inc. Footer navigation * Terms * Privacy * Security * Status * Docs * Contact * Manage cookies * Do not share my personal information You can't perform that action at this time.