Par (⅋) is an experimental concurrent programming language. It's an attempt to bring the expressive power of linear logic into practice.
See the code💬 Join our Discord, or use the Discussions as a forum to ask questions and share ideas!
🫶 If you'd like to support my effort to bring the power of linear logic into practical programming, you can do it via GitHub Sponsors.
Duality gives two sides to every concept, leading to rich composability. Whichever angle you take to tackle a problem, there will likely be ways to express it. Par comes with these first-class, structural types:
(Dual types are on the same line.)
These orthogonal concepts combine to give rise to a rich world of types and semantics.
Automatically concurrent execution. Everything that can run concurrently, does! Sequential execution is
only enforced by data dependencies. It's as if everything was async, but nothing needs await.
Par compiles to interaction combinators, which is the basis for the famous HVM, and the Bend programming language.
Structured concurrency with session types. Session types describe concurrent protocols, almost like finite-state machines, and make sure these are upheld in code. Par needs no special library for these. Linear types are session types, at least in their full version, which embraces duality.
No crashes. Runtime exceptions are not supported, except for running out of memory.
No deadlocks. Structured concurrency of Par makes deadlocks impossible.
(Almost) no infinite loops.* By default, recursion using begin/loop is checked for well-foundedness.
Iterative (corecursive) types are distinguished from recursive types, and enable constructing potentially unbounded objects, such as infinite sequences, with no danger of infinite loops, or a need to opt-out of totality.
*There is an escape hatch. Some algorithms, especially divide-and-conquer, are difficult or impossible
to implement using easy-to-check well-founded strategies. For those, unfounded turns this check
off. Vast majority of code doesn't need to opt-out of totality checking, it naturally fits its requirements.
Those few parts that need to opt-out are clearly marked with unfounded. They are the only places
that can potentially cause infinite loops.
Par is fully based on linear logic. It's an attempt to bring its expressive power into practice, by interpreting linear logic as session types.
In fact, the language itself is based on a little process language, called CP, from a paper called "Propositions as Sessions" by the famous Phil Wadler.
While programming in Par feels just like a programming language, even if an unusual one, its programs still correspond one-to-one with linear logic proofs.
There's still so much to be done! If this project speaks to you, join us on Discord.
Par is currently funded by motivation alone. Only your support can make it viable long-term. Consider sponsoring.
(top 24 of 71)
536 followers · starred Sep 2025
6,707 followers · starred Apr 2025
376 followers · starred Oct 2026
1,375 followers · starred Apr 2025
Par (⅋) is an experimental concurrent programming language. It's an attempt to bring the expressive power of linear logic into practice.
See the code💬 Join our Discord, or use the Discussions as a forum to ask questions and share ideas!
🫶 If you'd like to support my effort to bring the power of linear logic into practical programming, you can do it via GitHub Sponsors.
Duality gives two sides to every concept, leading to rich composability. Whichever angle you take to tackle a problem, there will likely be ways to express it. Par comes with these first-class, structural types:
(Dual types are on the same line.)
These orthogonal concepts combine to give rise to a rich world of types and semantics.
Automatically concurrent execution. Everything that can run concurrently, does! Sequential execution is
only enforced by data dependencies. It's as if everything was async, but nothing needs await.
Par compiles to interaction combinators, which is the basis for the famous HVM, and the Bend programming language.
Structured concurrency with session types. Session types describe concurrent protocols, almost like finite-state machines, and make sure these are upheld in code. Par needs no special library for these. Linear types are session types, at least in their full version, which embraces duality.
No crashes. Runtime exceptions are not supported, except for running out of memory.
No deadlocks. Structured concurrency of Par makes deadlocks impossible.
(Almost) no infinite loops.* By default, recursion using begin/loop is checked for well-foundedness.
Iterative (corecursive) types are distinguished from recursive types, and enable constructing potentially unbounded objects, such as infinite sequences, with no danger of infinite loops, or a need to opt-out of totality.
*There is an escape hatch. Some algorithms, especially divide-and-conquer, are difficult or impossible
to implement using easy-to-check well-founded strategies. For those, unfounded turns this check
off. Vast majority of code doesn't need to opt-out of totality checking, it naturally fits its requirements.
Those few parts that need to opt-out are clearly marked with unfounded. They are the only places
that can potentially cause infinite loops.
Par is fully based on linear logic. It's an attempt to bring its expressive power into practice, by interpreting linear logic as session types.
In fact, the language itself is based on a little process language, called CP, from a paper called "Propositions as Sessions" by the famous Phil Wadler.
While programming in Par feels just like a programming language, even if an unusual one, its programs still correspond one-to-one with linear logic proofs.
There's still so much to be done! If this project speaks to you, join us on Discord.
Par is currently funded by motivation alone. Only your support can make it viable long-term. Consider sponsoring.
(top 24 of 71)
536 followers · starred Sep 2025
6,707 followers · starred Apr 2025
376 followers · starred Oct 2026
1,375 followers · starred Apr 2025
