Lamda_calculus_formalizations Alternatives

Similar projects and alternatives to lamda_calculus_formalizations

elaboration-zoo

23 561 5.3 Haskell lamda_calculus_formalizations VS elaboration-zoo

Minimal implementations for dependent type checking and elaboration
lambda-calculus-hs

1 42 6.4 Haskell lamda_calculus_formalizations VS lambda-calculus-hs

Single file Lambda Calculus implementations demonstrating various type system features and interpretation techniques
WorkOS

workos.com sponsored

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.

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a better lamda_calculus_formalizations alternative or higher similarity.

Suggest an alternative to lamda_calculus_formalizations

lamda_calculus_formalizations reviews and mentions

Posts with mentions or reviews of lamda_calculus_formalizations. We have used some of these posts to build our list of alternatives and similar projects. The last one was on 2023-06-14.

How to implement dependent type theory I (2012)
3 projects | news.ycombinator.com | 14 Jun 2023

This is really cool. I've been doing something in a similar vein at https://github.com/sgodwincs/lamda_calculus_formalizations, though the difference being I'm using Lean and trying to prove certain properties of the languages (type safety, normalization, etc.). Of course, compared to unification and stuff you have, I only have very simple additions like natural numbers and binary product types (though the proofs still are hard for me!). Working on finite product types now and it's an absolute pain to even define it in a way that Lean likes.