The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning. Learn more →
Top 17 type-theory Open-Source Projects
-
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
-
write-you-a-haskell
Building a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)
-
-
-
WorkOS
The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.
-
TypeTopology
Logical manifestations of topological concepts, and other things, via the univalent point of view.
-
-
redtt
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
-
path_semantics
A research project in path semantics, a re-interpretation of functions for expressing mathematics
-
-
Category_Theory_Natural_Language_Processing_NLP
List of papers and other resources at the intersection of Category Theory and NLP.
-
SaaSHub
SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
I recall reading a comment on here at some point in the last year where someone who worked on a team that wrote compilers lamented the difficulty in hiring qualified people because the practice of compiler construction differs so wildly from what is taught in school or even most compiler books. Apparently it scarcely resembles what is taught in university courses based on the Dragon book or similar, both in the higher level architecture and the lower level techniques
I know that one difference is that compilers have adopted a more service-oriented architecture, kind of like the Roslyn compiler. This allows them to not only compile your code, but inform your text editor and linter and similar tooling of syntax issues incrementally.
What are other differences? Is llvm still relevant outside of academia?
Are there any books, papers, or open source projects one could study to learn how compilers are built in this day and age?
Also: does the more abstract "programming language theory" popular in the more formal functional programming world (e.g. denotational semantics, lambda calculus, Floyd-Hoare logic, type theory, etc: this sort of stuff[1]) have any relevance to compiler writers and language/language tooling developers in industry?
[1] https://steshaw.org/plt/
Project mention: Kind: A lambda-calculus based pure programming language | news.ycombinator.com | 2023-11-27
I highly recommend https://github.com/sdiehl/write-you-a-haskell as it is very developer friendly. It’s not complete, but it really gets the gears turning and will set you up for writing your own Hendley-Milner style type checker.
This was recently deemed inappropriate:
"Bye bye Set"
"Set and Prop are removed as keywords"
https://github.com/agda/agda/pull/4629
Project mention: What do we mean by "the foundations of mathematics"? | news.ycombinator.com | 2023-11-01https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t... :
> * Today, Zermelo–Fraenkel set theory [ZFC], with the historically controversial axiom of choice (AC) included, is the standard form of axiomatic set theory and as such is the most common* foundation of mathematics.
Foundation of mathematics: https://en.wikipedia.org/wiki/Foundations_of_mathematics
Implementation of mathematics in set theory:
> The implementation of a number of basic mathematical concepts is carried out in parallel in ZFC (the dominant set theory) and in NFU, the version of Quine's New Foundations shown to be consistent by R. B. Jensen in 1969 (here understood to include at least axioms of Infinity and Choice).
> What is said here applies also to two families of set theories: on the one hand, a range of theories including Zermelo set theory near the lower end of the scale and going up to ZFC extended with large cardinal hypotheses such as "there is a measurable cardinal"; and on the other hand a hierarchy of extensions of NFU which is surveyed in the New Foundations article. These correspond to different general views of what the set-theoretical universe is like
IEEE-754 specifies that float64s have ±infinity and specify ZeroDivisionError. Symbolic CAS with MPFR needn't be limited to float64s.
HoTT in CoQ: Coq-HoTT: https://github.com/HoTT/Coq-HoTT
leanprover-community/mathlib4//
Project mention: A Taste of Coq and Correct Code by Construction | news.ycombinator.com | 2023-09-03If you're already familiar with a functional programming language like Haskell or OCaml, you have the prerequisite knowledge to work through my Coq tutorial here: https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...
My goal with this tutorial was to introduce the core aspects of the language (dependent types, tactics, etc.) in a "straight to the point" kind of way for readers who are already motivated to learn it. If you've heard about proof assistants like Coq or Lean and you're fascinated by what they can do, and you just want the TL;DR of how they work, then this tutorial is written for you.
Any feedback is appreciated!
I just wonder if there are any irl meetups of people involved with formalizing mathematics, I thought that it would be a cool hobby to pick up (with some background in math and programming) but the existing libraries, like MathLib, TypeTopology or UniMath look a bit intimidating...
Variant
Project mention: What do we mean by "the foundations of mathematics"? | news.ycombinator.com | 2023-11-01In mathematics, the roof holds up the building, not the foundation. Since humans use mathematics a lot, we design foundations to our specific needs. It is not the building we are worried about, we just want better foundations to create better tools.
Not only are we going to treat mathematics as subjective, but also having formal theories that reason about different notions of subjectivity. https://crates.io/crates/joker_calculus
> Could our conception of paradox be itself primal, and perhaps, in some plane, could it be something ranking higher, of first-class?
Yes! Paradoxes are statements of the form `false^a` in exponential propositions. https://crates.io/crates/hooo
> Also, I’ve been thinking, recently, on the role of time in structures. There can’t possibly be any structure whatsoever without time, or, more concretely, at least the memory of events, recollecting distinctive and contrasting entropic signatures. So, mathematics manifesting as, of, and for structure, wouldn’t it require, first and foremost, a treatment from physics? Regular or meta?
Path semantical quality models this relation, where you have different "moments" in time which each are spaces for normal logical reasoning. Between these moments, there are ways to propagate quality, which is a partial equivalence. https://github.com/advancedresearch/path_semantics
Project mention: Cicada – A FOSS, Cross-Platform Version of GitHub Actions and Gitlab CI | news.ycombinator.com | 2023-11-06There is a collision in names:
Cicada, this CI tool, uses a DSL (domain specific language) to write configuration, and this DSL is referred to as "Cicada language", and blasted in marketing copy as a "real programming language" on https://cicada.sh/
However, this is a completely different language from Cicada language, a programming language and theorem prover hosted at https://cicada-lang.org/ and https://github.com/cicada-lang/cicada
This name collision is very confusing, and I wonder why Cicada the CI tool didn't just stick to python, since it is also a "real programming language"
HOAS can be very useful when we are building type systems, an example is Lura's type system, that defines two states, one state for HOAS, and another state for the Quoted types.
NOTE:
The open source projects on this list are ordered by number of github stars.
The number of mentions indicates repo mentiontions in the last 12 Months or
since we started tracking (Dec 2020).
type-theory related posts
- Kind: A lambda-calculus based pure programming language
- What do we mean by "the foundations of mathematics"?
- A Taste of Coq and Correct Code by Construction
- Will Computers Redefine the Roots of Math?
- Ask HN: Learning Modern Compilers?
- What are some evergreen articles on programming languages and computing in general?
- First (1/5) steps with HVM, A massively parallel, optimal functional runtime in Rust
-
A note from our sponsor - WorkOS
workos.com | 25 Apr 2024
Index
What are some of the best open-source type-theory projects? This list will help you:
| Project | Stars | |
|---|---|---|
| 1 | plt | 5,126 |
| 2 | Kind | 3,438 |
| 3 | write-you-a-haskell | 3,304 |
| 4 | Agda | 2,371 |
| 5 | Coq-HoTT | 1,213 |
| 6 | cubicaltt | 556 |
| 7 | datafun | 375 |
| 8 | proofs | 286 |
| 9 | TypeTopology | 211 |
| 10 | cooltt | 208 |
| 11 | redtt | 199 |
| 12 | variant | 178 |
| 13 | path_semantics | 157 |
| 14 | ttlite | 118 |
| 15 | cicada | 92 |
| 16 | Category_Theory_Natural_Language_Processing_NLP | 40 |
| 17 | lura | 31 |
Sponsored
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com